Commit 2024-10-17 19:56 e355e86a

View on Github →

chore: fix "proof was" porting notes (#17836) Go through all porting notes that contain the string "proof was" and try to fix them. The following steps were used:

Golf the new proof.
If the current proof is nicer, delete the note.
Try to restore the old proof.
Classify some of the old failing proofs.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Subobject.lean

Modified Mathlib/Algebra/Order/Group/Units.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Algebra/Star/Subalgebra.lean

modified def StarAlgHom.equalizer

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/Tree/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/SymplecticGroup.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/Order/Hom/Lattice.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean