mathlib3

17fe3632 - feat(geometry/manifold/cont_mdiff_mfderiv): prove that mfderiv is smooth (#18827)

feat(geometry/manifold/cont_mdiff_mfderiv): prove that mfderiv is smooth (#18827) * From the sphere eversion project * `cont_mdiff_at.mfderiv` is strong enough to prove `cont_mdiff.cont_mdiff_tangent_map`. This is already done in [the sphere eversion project](https://github.com/leanprover-community/sphere-eversion/blob/9486e7f42c283041bc512f133daec359b73d4986/src/to_mathlib/unused/geometry_manifold_misc.lean#L383). We would need to generalize `cont_mdiff_at.mfderiv` to something like `cont_mdiff_within_at.mfderiv_within` to prove the full version of `cont_mdiff_on.cont_mdiff_on_tangent_map_within`. This is non-trivial and needs additions to already ported files, so I'll wait with doing that till after the port.