Commit 2023-06-07 13:00 e354e865

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