Commit 2026-03-05 11:23 f0fb0d6c

View on Github →

chore(Geometry/Manifold/MFDeriv): golf using custom elaborators (#36010)

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

modified theorem ModelWithCorners.mdifferentiableOn_symm

modified theorem OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot

modified theorem OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt_symm

modified theorem OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective

modified theorem OpenPartialHomeomorph.MDifferentiable.mfderiv_injective

modified theorem OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective

modified theorem OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top

modified theorem OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ

modified theorem mdifferentiableAt_atlas

modified theorem mdifferentiableOn_atlas

modified theorem mdifferentiableOn_atlas_symm

modified theorem mdifferentiableOn_extChartAt

Modified Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean

modified theorem mdifferentiable_iff_differentiable

modified theorem mfderiv_eq_fderiv

Modified Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean