Commit 2026-07-17 10:49 19f249b3

View on Github →

chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) As requested here.

Estimated changes

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

modified theorem ContMDiff.mdifferentiable

modified theorem ContMDiff.mdifferentiableAt

modified theorem ContMDiff.mdifferentiableWithinAt

modified theorem ContMDiffAt.mdifferentiableAt

modified theorem ContMDiffOn.mdifferentiableOn

modified theorem ContMDiffWithinAt.mdifferentiableWithinAt

modified theorem Filter.EventuallyEq.mfderiv_eq

modified theorem HasMFDerivAt.comp

modified theorem HasMFDerivAt.comp_hasMFDerivWithinAt

modified theorem HasMFDerivAt.congr_mfderiv

modified theorem HasMFDerivAt.congr_of_eventuallyEq

modified theorem HasMFDerivAt.continuousAt

modified theorem HasMFDerivAt.hasMFDerivWithinAt

modified theorem HasMFDerivAt.mdifferentiableAt

modified theorem HasMFDerivWithinAt.comp

modified theorem HasMFDerivWithinAt.congr_mfderiv

modified theorem HasMFDerivWithinAt.congr_mono

modified theorem HasMFDerivWithinAt.congr_of_eventuallyEq

modified theorem HasMFDerivWithinAt.continuousWithinAt

modified theorem HasMFDerivWithinAt.hasMFDerivAt

modified theorem HasMFDerivWithinAt.mdifferentiableWithinAt

modified theorem HasMFDerivWithinAt.mono

modified theorem HasMFDerivWithinAt.mono_of_mem_nhdsWithin

modified theorem HasMFDerivWithinAt.union

modified theorem MDifferentiable.comp

modified theorem MDifferentiable.comp_mdifferentiableOn

modified theorem MDifferentiable.continuous

modified theorem MDifferentiable.mdifferentiableAt

modified theorem MDifferentiable.mdifferentiableOn

modified theorem MDifferentiable.mfderivWithin

modified theorem MDifferentiableAt.comp

modified theorem MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq

modified theorem MDifferentiableAt.comp_of_eq

modified theorem MDifferentiableAt.congr_of_eventuallyEq

modified theorem MDifferentiableAt.hasMFDerivAt

modified theorem MDifferentiableAt.mdifferentiableWithinAt

modified theorem MDifferentiableOn.comp

modified theorem MDifferentiableOn.congr

modified theorem MDifferentiableOn.congr_mono

modified theorem MDifferentiableOn.continuousOn

modified theorem MDifferentiableOn.iUnion_of_isOpen

modified theorem MDifferentiableOn.mdifferentiableAt

modified theorem MDifferentiableOn.mono

modified theorem MDifferentiableWithinAt.comp

modified theorem MDifferentiableWithinAt.comp_of_eq

modified theorem MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq

modified theorem MDifferentiableWithinAt.congr'

modified theorem MDifferentiableWithinAt.congr

modified theorem MDifferentiableWithinAt.congr_mono

modified theorem MDifferentiableWithinAt.congr_nhds

modified theorem MDifferentiableWithinAt.congr_of_eventuallyEq

modified theorem MDifferentiableWithinAt.congr_of_mem

modified theorem MDifferentiableWithinAt.hasMFDerivWithinAt

modified theorem MDifferentiableWithinAt.mdifferentiableAt

modified theorem MDifferentiableWithinAt.mfderivWithin_congr_mono

modified theorem MDifferentiableWithinAt.mfderivWithin_mono

modified theorem MDifferentiableWithinAt.mono

modified theorem MDifferentiableWithinAt.mono_of_mem_nhdsWithin

modified theorem hasMFDerivAt_unique

modified theorem hasMFDerivWithinAt_univ

modified theorem mdifferentiableAt_of_isInvertible_mfderiv

modified theorem mdifferentiableAt_of_mfderiv_injective

modified theorem mdifferentiableOn_congr

modified theorem mdifferentiableOn_empty

modified theorem mdifferentiableOn_iUnion_iff_of_isOpen

modified theorem mdifferentiableOn_univ

modified theorem mdifferentiableWithinAt_congr_set

modified theorem mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas

modified theorem mdifferentiableWithinAt_insert

modified theorem mdifferentiableWithinAt_insert_self

modified theorem mdifferentiableWithinAt_inter'

modified theorem mdifferentiableWithinAt_inter

modified theorem mdifferentiableWithinAt_of_isInvertible_mfderivWithin

modified theorem mdifferentiableWithinAt_of_mfderivWithin_injective

modified theorem mdifferentiableWithinAt_of_subsingleton

modified theorem mdifferentiableWithinAt_univ

modified theorem mdifferentiable_of_mdifferentiableOn_union_of_isOpen

modified theorem mdifferentiable_of_subsingleton

modified theorem mfderivWithin_comp

modified theorem mfderivWithin_comp_of_eq

modified theorem mfderivWithin_comp_of_preimage_mem_nhdsWithin

modified theorem mfderivWithin_congr_set

modified theorem mfderivWithin_eq_mfderiv

modified theorem mfderivWithin_inter

modified theorem mfderivWithin_of_isOpen

modified theorem mfderivWithin_of_mem_nhds

modified theorem mfderivWithin_subset

modified theorem mfderivWithin_univ

modified theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt

modified theorem mfderiv_comp

modified theorem mfderiv_comp_apply

modified theorem mfderiv_comp_apply_of_eq

modified theorem mfderiv_comp_mfderivWithin

modified theorem mfderiv_comp_mfderivWithin_of_eq

modified theorem mfderiv_comp_of_eq

modified theorem mfderiv_zero_of_not_mdifferentiableAt

modified theorem tangentMapWithin_comp_at

modified theorem tangentMapWithin_proj

modified theorem tangentMapWithin_snd

modified theorem tangentMapWithin_subset

modified theorem tangentMapWithin_univ

modified theorem tangentMap_comp

modified theorem tangentMap_comp_at

modified theorem tangentMap_proj

modified theorem tangentMap_snd