feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (#18087)

feat(combinatorics/simple_graph): More clique lemmas (#19203)

feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976)

move old README.md to OLD_README.md

doc: Add a warning mentioning Lean 4 to the readme (#19243)

feat(topology/metric_space): diameter of pointwise zero and addition (#19028)

feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (#18629)

feat(probability/independence): Independence of singletons (#18506)

feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612)

feat(data/finset/lattice): `sup'`/`inf'` lemmas (#18989)

chore(order/liminf_limsup): Generalise and move lemmas (#18628)

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (#17926)

feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (#11352)

feat(analysis/convex/proj_Icc): Extending convex functions (#18797)

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (#17925)