mathlib

7c9a86d4 - refactor(geometry/manifold): use a sigma type for the total space of the tangent bundle (#3966)

refactor(geometry/manifold): use a sigma type for the total space of the tangent bundle (#3966) Redefine the total space of the tangent bundle to be a sigma type instead of a product type. Before ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: E ``` After ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: tangent_space I x ``` This seems more natural, and is probably needed to do Riemannian manifolds right. The drawback is that we can not abuse identifications any more between the tangent bundle to a vector space and a product space (but we can still identify the tangent space with the vector space itself, which is the most important thing). Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>