mathlib3

4ece2ee4 - feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv (#15523)

feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv (#15523) * Define `achart` * Rename and reformulate `mem_maximal_atlas_of_mem_atlas -> subset_maximal_atlas` * Used to prove smoothness of `mfderiv` (that result still has to be generalized to `mfderiv_within`, so is not included yet) * From the sphere eversion project