* fix-lint: (463 commits)
  chore: lint-style.py was calling str.replace incorrectly
  chore: module doc for #find_home, #minimize_imports, import early (#7095)
  chore: reduce imports to Data.Rat.Cast.CharZero (#7091)
  chore: cleanup imports of Data/Rat/Cast/Defs (#7092)
  chore: linarith only needs ring1 (#7090)
  refactor(Data/Int/Bitwise): use `<<<` and `>>>` notation (#6789)
  chore: delete redundant commented-out positivity test (#7085)
  chore: fix docstrings, names and aligns about paracompacity of emetric spaces (#7064)
  feat(Data/Finsupp): add notation (#6367)
  refactor: re-home some meta code (#6921)
  fix: don't use `False` as a bool, use `false` (#7059)
  chore: fix reference to `compactCovering` in docstring (#7065)
  fix: fix link in docstring of IsWellFounded (#7063)
  chore: tidy various files (#7041)
  feat: roots in an algebra (#6740)
  chore: revert ProofWidgets bump in #7044 and #7056 (#7069)
  feat: super factorial (#6768)
  feat(LinearAlgebra/Matrix/Trace): add Matrix.trace_diagonal (#7061)
  chore: complete ProofWidgets bump (#7056)
  feat: More `Finset.sup'` lemmas (#7021)
  feat: self_lt_pow (#7058)
  chore: move some files to `MeasureTheory/MeasurableSpace/` (#7045)
  chore(RingTheory/Nilpotent): untwine two universes (#7057)
  feat: von Neumann Mean Ergodic Theorem (#6053)
  feat: (sSup, Iic) and (Ici, sInf) are Galois connections (#6951)
  feat: derivative along a vector (#7038)
  feat: check for some common git problems in CI (#7043)
  chore: bump ProofWidgets (#7044)
  feat(Topology/Algebra): add `DiscreteTopology Mˣ` (#7028)
  chore: simplify `by rfl` (#7039)
  chore: tidy various files (#7035)
  refactor(LinearAlgebra/CliffordAlgebra/Conjugation): expose implementation details of 'reverse' (#6783)
  feat: add `DiscreteTopology.of_continuous_injective` (#7029)
  feat: restore the module docstring code snippet (#7030)
  feat: flesh out the API for `realPart` and `imaginaryPart` (#7023)
  chore: missing simps lemmas for `Multiplicative` defs (#7016)
  feat: characterize isLittleO on principal filters (#7008)
  doc: cleanup documentation on Basis.constr (#7007)
  feat: cleanup API around differentiable functions (#7004)
  feat: add Nat.digits_append_digits (#6999)
  feat: definition of the homology of a short complex (#6994)
  chore: implement porting notes about Polish spaces (#6991)
  feat(Algebra/Category/ModuleCat): composition of restriction of scalar functors (#6915)
  feat: compute the integral of sqrt (1 - x ^ 2) (#6905)
  chore(*/TensorProduct): missing functorial lemmas (#6781)
  feat: a functor from a small category to a filtered category factors through a small filtered category (#6212)
  feat: expand API on locally integrable functions (#7006)
  chore: split Tactic.NormNum.Basic (#7002)
  feat: a few lemmas on continuous functions (#7005)
  feat: ZMod.castHom_self (#7013)
  ...

The cache is broken after #7044 and #7056, so I am reverting them. (And merging directly, rather than via bors.)