Commit 2026-03-06 14:49 1921cdab

View on Github →

chore: golf using custom elaborators (#36235) The final pieces from #30357.

Estimated changes

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Geometry/Manifold/Complex.lean

modified theorem MDifferentiable.exists_eq_const_of_compactSpace

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

Modified Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMap.lean

modified theorem ContMDiffMap.coeFn_mk

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/Geometry/Manifold/GroupLieAlgebra.lean

Modified Mathlib/Geometry/Manifold/Instances/Icc.lean

modified theorem contMDiffOn_projIcc

modified theorem contMDiff_subtype_coe_Icc

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

modified theorem contMDiff_circleExp

Modified Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean

Modified Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

modified theorem IsLocalDiffeomorph.contMDiff

Modified Mathlib/Geometry/Manifold/Notation.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

modified theorem BumpCovering.coe_toSmoothPartitionOfUnity

modified def BumpCovering.toSmoothPartitionOfUnity

modified theorem SmoothPartitionOfUnity.contMDiff_smul

modified theorem SmoothPartitionOfUnity.contMDiff_sum

Modified Mathlib/Geometry/Manifold/Riemannian/Basic.lean

Modified Mathlib/Geometry/Manifold/Riemannian/PathELength.lean

modified theorem Manifold.riemannianEDist_le_pathELength

Modified Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

Modified Mathlib/Geometry/Manifold/SmoothEmbedding.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Hom.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean

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

modified theorem contMDiff_vectorSpace_iff_contDiff

Modified Mathlib/Geometry/Manifold/WhitneyEmbedding.lean