mathlib3

e354e865 - feat(geometry/manifold): lemmas from the sphere eversion project (#18877)

feat(geometry/manifold): lemmas from the sphere eversion project (#18877) * Also adds a new library note `comp_of_eq lemmas` about how (I think) we should better formulate composition lemmas of properties of functions. * About the library note `comp_of_eq lemmas`: exactly the same problems happen in Lean 4. * renamings ``` smooth_iff_proj_smooth -> smooth_prod_iff differentiable_at.fderiv_within_prod -> differentiable_within_at.fderiv_within_prod ``` * We add a `path_connected_space` instance of the tangent space. This instance is sufficient to compile sphere-eversion, without any `normed_space` instances on the tangent space (which are not the canonical structure on the tangent space). * From the sphere eversion project