mathlib

e6444585 - feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts (#17668)

feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts (#17668) * This PR generalizes some smoothness results from `ext_chart_at` to arbitrary members of the maximal atlas * Useful for smooth vector bundle refactor * Motivated by the sphere eversion project