refactor(Geometry/Euclidean/Projection): revert everything back to metric space (leanprover-community#33385)

After leanprover-community#27378 was merged, @jsm28 noted that `[NormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P]` implies `[MetricSpace P]` anyways so there's no point distinguishing between `PseudoMetricSpace` and `MetricSpace`.

Author: peakpoint

Mathlib/Geometry/Euclidean/Projection.lean

@@ -37,9 +37,7 @@ variable {V₂ P₂ : Type*} [NormedAddCommGroup V₂] [InnerProductSpace 𝕜 V
 
 open AffineSubspace
 
-section PseudoMetricSpace
-
-variable [PseudoMetricSpace P] [NormedAddTorsor V P]
+variable [MetricSpace P] [NormedAddTorsor V P]
 
 /-- The orthogonal projection of a point onto a nonempty affine subspace. -/
 def orthogonalProjection (s : AffineSubspace 𝕜 P) [Nonempty s]
@@ -177,6 +175,19 @@ theorem eq_orthogonalProjection_of_eq_subspace {s s' : AffineSubspace 𝕜 P} [N
   have h := SetLike.coe_mem (orthogonalProjection (affineSpan 𝕜 {p₁}) p₂)
   rwa [mem_affineSpan_singleton] at h
 
+/-- The distance to a point's orthogonal projection is 0 iff it lies in the subspace. -/
+theorem dist_orthogonalProjection_eq_zero_iff {s : AffineSubspace 𝕜 P} [Nonempty s]
+    [s.direction.HasOrthogonalProjection] {p : P} :
+    dist p (orthogonalProjection s p) = 0 ↔ p ∈ s := by
+  rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_iff]
+
+/-- The distance between a point and its orthogonal projection is
+nonzero if it does not lie in the subspace. -/
+theorem dist_orthogonalProjection_ne_zero_of_notMem {s : AffineSubspace 𝕜 P} [Nonempty s]
+    [s.direction.HasOrthogonalProjection] {p : P} (hp : p ∉ s) :
+    dist p (orthogonalProjection s p) ≠ 0 :=
+  mt dist_orthogonalProjection_eq_zero_iff.mp hp
+
 /-- Subtracting `p` from its `orthogonalProjection` produces a result
 in the orthogonal direction. -/
 theorem orthogonalProjection_vsub_mem_direction_orthogonal (s : AffineSubspace 𝕜 P) [Nonempty s]
@@ -505,11 +516,6 @@ theorem reflection_vadd_smul_vsub_orthogonalProjection {s : AffineSubspace 𝕜
   reflection_orthogonal_vadd hp₁
     (Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal s _))
 
-end PseudoMetricSpace
-
-section MetricSpace
-
-variable [MetricSpace P] [NormedAddTorsor V P]
 variable [MetricSpace P₂] [NormedAddTorsor V₂ P₂]
 
 @[simp] lemma orthogonalProjection_map (s : AffineSubspace 𝕜 P) [Nonempty s]
@@ -537,19 +543,6 @@ lemma orthogonalProjection_subtype (s : AffineSubspace 𝕜 P) [Nonempty s] (s'
     infer_instance
   convert orthogonalProjection_map s' s.subtypeₐᵢ p
 
-/-- The distance to a point's orthogonal projection is 0 iff it lies in the subspace. -/
-theorem dist_orthogonalProjection_eq_zero_iff {s : AffineSubspace 𝕜 P} [Nonempty s]
-    [s.direction.HasOrthogonalProjection] {p : P} :
-    dist p (orthogonalProjection s p) = 0 ↔ p ∈ s := by
-  rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_iff]
-
-/-- The distance between a point and its orthogonal projection is
-nonzero if it does not lie in the subspace. -/
-theorem dist_orthogonalProjection_ne_zero_of_notMem {s : AffineSubspace 𝕜 P} [Nonempty s]
-    [s.direction.HasOrthogonalProjection] {p : P} (hp : p ∉ s) :
-    dist p (orthogonalProjection s p) ≠ 0 :=
-  mt dist_orthogonalProjection_eq_zero_iff.mp hp
-
 @[simp] lemma reflection_map (s : AffineSubspace 𝕜 P) [Nonempty s]
     [s.direction.HasOrthogonalProjection] (f : P →ᵃⁱ[𝕜] P₂)
     [(s.map f.toAffineMap).direction.HasOrthogonalProjection] (p : P) :
@@ -562,8 +555,6 @@ lemma reflection_subtype (s : AffineSubspace 𝕜 P) [Nonempty s] (s' : AffineSu
     (reflection s' p : P) = reflection (s'.map s.subtype) p := by
   simp [reflection_apply', orthogonalProjection_subtype]
 
-end MetricSpace
-
 end EuclideanGeometry
 
 namespace Affine
@@ -576,9 +567,7 @@ variable {𝕜 : Type*} {V : Type*} {P : Type*} [RCLike 𝕜]
 variable [NormedAddCommGroup V] [InnerProductSpace 𝕜 V]
 variable {V₂ P₂ : Type*} [NormedAddCommGroup V₂] [InnerProductSpace 𝕜 V₂]
 
-section PseudoMetricSpace
-
-variable [PseudoMetricSpace P] [NormedAddTorsor V P]
+variable [MetricSpace P] [NormedAddTorsor V P]
 
 /-- The orthogonal projection of a point `p` onto the hyperplane spanned by the simplex's points. -/
 def orthogonalProjectionSpan {n : ℕ} (s : Simplex 𝕜 P n) :
@@ -627,11 +616,6 @@ lemma orthogonalProjectionSpan_faceOpposite_eq_point_rev (s : Simplex 𝕜 P 1)
     (p : P) : (s.faceOpposite i).orthogonalProjectionSpan p = s.points i.rev := by
   simp [faceOpposite_point_eq_point_rev]
 
-end PseudoMetricSpace
-
-section MetricSpace
-
-variable [MetricSpace P] [NormedAddTorsor V P]
 variable [MetricSpace P₂] [NormedAddTorsor V₂ P₂]
 
 lemma orthogonalProjectionSpan_map {n : ℕ} (s : Simplex 𝕜 P n) (f : P →ᵃⁱ[𝕜] P₂) (p : P) :
@@ -648,8 +632,6 @@ lemma orthogonalProjectionSpan_map {n : ℕ} (s : Simplex 𝕜 P n) (f : P →
   rw [eq_comm]
   convert (s.restrict S hS).orthogonalProjectionSpan_map S.subtypeₐᵢ p
 
-end MetricSpace
-
 end Simplex
 
 end Affine