mathlib

c91fc150 - chore(geometry/manifold/real_instances): use euclidean_space (#3077)

chore(geometry/manifold/real_instances): use euclidean_space (#3077) Now that `euclidean_space` has been refactored to use the product topology, we can fix the geometry file that used a version of the product space (with the sup norm!) called `euclidean_space2`, using now instead the proper `euclidean_space`.