feat(Geometry/Euclidean/Angle): angles with orthogonal projections

Add some lemmas that angles involving orthogonal projections are right
angles.  The unoriented versions abstract something used multiple
times in `Mathlib.Geometry.Euclidean.Angle.Bisector` (which is thus
refactored to use the new lemmas); I expect the oriented versions may
be of use in future in further oriented angle bisection lemmas
building on top of leanprover-community#30477.

Author: jsm28

Mathlib.lean

@@ -3888,13 +3888,15 @@ import Mathlib.Geometry.Euclidean.Altitude
 import Mathlib.Geometry.Euclidean.Angle.Bisector
 import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
 import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
+import Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
 import Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
 import Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
 import Mathlib.Geometry.Euclidean.Angle.Sphere
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
+import Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
 import Mathlib.Geometry.Euclidean.Basic
 import Mathlib.Geometry.Euclidean.Circumcenter

Mathlib/Geometry/Euclidean/Angle/Bisector.lean

@@ -3,6 +3,7 @@ Copyright (c) 2025 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
+import Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
 import Mathlib.Geometry.Euclidean.Projection
 
@@ -41,15 +42,12 @@ private lemma dist_orthogonalProjection_eq_iff_angle_eq_aux₁ {p p' : P}
     · subst hpp'
       exact hp'.2
     · by_contra hn
-      rw [angle_self_of_ne hpp', angle_comm, angle_eq_arcsin_of_angle_eq_pi_div_two,
+      rw [angle_self_of_ne hpp', angle_comm,
+        angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'.2),
         Real.zero_eq_arcsin_iff, div_eq_zero_iff] at h
       · simp only [dist_eq_zero, hpp', or_false] at h
         rw [eq_comm] at h
         simp [orthogonalProjection_eq_self_iff, hn] at h
-      · rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
-        exact Submodule.inner_left_of_mem_orthogonal (K := s₂.direction)
-          (AffineSubspace.vsub_mem_direction hp'.2 (orthogonalProjection_mem _))
-          (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
       · exact .inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 hn))
 
 /-- Auxiliary lemma for the degenerate case of `dist_orthogonalProjection_eq_iff_angle_eq` where
@@ -86,10 +84,10 @@ lemma dist_orthogonalProjection_eq_iff_angle_eq {p p' : P} {s₁ s₂ : AffineSu
   · exact dist_orthogonalProjection_eq_iff_angle_eq_aux hp' h'
   rw [not_or] at h'
   rw [angle_comm,
-    angle_eq_arcsin_of_angle_eq_pi_div_two ?_
+    angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'.1)
       (.inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 h'.1))),
     angle_comm,
-    angle_eq_arcsin_of_angle_eq_pi_div_two ?_
+    angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'.2)
       (.inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 h'.2)))]
   · refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
     · rw [h]
@@ -105,13 +103,5 @@ lemma dist_orthogonalProjection_eq_iff_angle_eq {p p' : P} {s₁ s₂ : AffineSu
         exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'.1)
       · rw [dist_orthogonalProjection_eq_infDist]
         exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'.2)
-  · rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
-    exact Submodule.inner_left_of_mem_orthogonal (K := s₂.direction)
-      (AffineSubspace.vsub_mem_direction hp'.2 (orthogonalProjection_mem _))
-      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
-  · rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
-    exact Submodule.inner_left_of_mem_orthogonal (K := s₁.direction)
-      (AffineSubspace.vsub_mem_direction hp'.1 (orthogonalProjection_mem _))
-      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
 
 end EuclideanGeometry

Mathlib/Geometry/Euclidean/Angle/Oriented/Projection.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2025 Joseph Myers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Myers
+-/
+import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
+import Mathlib.Geometry.Euclidean.Projection
+import IMO.AngleProjection
+
+/-!
+# Oriented angles and orthogonal projection.
+
+This file proves lemmas relating to oriented angles involving orthogonal projections.
+
+-/
+
+
+namespace EuclideanGeometry
+
+open Module
+open scoped Real
+
+variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
+variable [NormedAddTorsor V P] [hd2 : Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]
+
+lemma oangle_self_orthogonalProjection (p : P) {p' : P} {s : AffineSubspace ℝ P}
+    [s.direction.HasOrthogonalProjection] (hp : p ∉ s) (h : p' ∈ s)
+    (hp' : haveI : Nonempty s := ⟨p', h⟩; p' ≠ orthogonalProjection s p) :
+    haveI : Nonempty s := ⟨p', h⟩
+    ∡ p (orthogonalProjection s p) p' = (π / 2 : ℝ) ∨
+      ∡ p (orthogonalProjection s p) p' = (-π / 2 : ℝ) := by
+  haveI : Nonempty s := ⟨p', h⟩
+  have hpne : p ≠ orthogonalProjection s p := Ne.symm (orthogonalProjection_eq_self_iff.not.2 hp)
+  have ha := oangle_eq_angle_or_eq_neg_angle hpne hp'
+  rw [angle_self_orthogonalProjection p h] at ha
+  rwa [neg_div]
+
+lemma oangle_orthogonalProjection_self (p : P) {p' : P} {s : AffineSubspace ℝ P}
+    [s.direction.HasOrthogonalProjection] (hp : p ∉ s) (h : p' ∈ s)
+    (hp' : haveI : Nonempty s := ⟨p', h⟩; p' ≠ orthogonalProjection s p) :
+    haveI : Nonempty s := ⟨p', h⟩
+    ∡ p' (orthogonalProjection s p) p = (π / 2 : ℝ) ∨
+      ∡ p' (orthogonalProjection s p) p = (-π / 2 : ℝ) := by
+  rw [oangle_rev, neg_eq_iff_eq_neg, neg_eq_iff_eq_neg, or_comm, ← Real.Angle.coe_neg, neg_div,
+    neg_neg, ← Real.Angle.coe_neg, ← neg_div]
+  exact oangle_self_orthogonalProjection p hp h hp'
+
+lemma two_zsmul_oangle_self_orthogonalProjection (p : P) {p' : P} {s : AffineSubspace ℝ P}
+    [s.direction.HasOrthogonalProjection] (hp : p ∉ s) (h : p' ∈ s)
+    (hp' : haveI : Nonempty s := ⟨p', h⟩; p' ≠ orthogonalProjection s p) :
+    haveI : Nonempty s := ⟨p', h⟩
+    (2 : ℤ) • ∡ p (orthogonalProjection s p) p' = π := by
+  rw [Real.Angle.two_zsmul_eq_pi_iff]
+  exact oangle_self_orthogonalProjection p hp h hp'
+
+lemma two_zsmul_oangle_orthogonalProjection_self (p : P) {p' : P} {s : AffineSubspace ℝ P}
+    [s.direction.HasOrthogonalProjection] (hp : p ∉ s) (h : p' ∈ s)
+    (hp' : haveI : Nonempty s := ⟨p', h⟩; p' ≠ orthogonalProjection s p) :
+    haveI : Nonempty s := ⟨p', h⟩
+    (2 : ℤ) • ∡ p' (orthogonalProjection s p) p = π := by
+  rw [Real.Angle.two_zsmul_eq_pi_iff]
+  exact oangle_orthogonalProjection_self p hp h hp'
+
+end EuclideanGeometry

Mathlib/Geometry/Euclidean/Angle/Unoriented/Projection.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2025 Joseph Myers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Myers
+-/
+import Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
+import Mathlib.Geometry.Euclidean.Projection
+
+/-!
+# Angles and orthogonal projection.
+
+This file proves lemmas relating to angles involving orthogonal projections.
+
+-/
+
+
+namespace EuclideanGeometry
+
+variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
+variable [NormedAddTorsor V P]
+
+open scoped Real
+
+@[simp] lemma angle_self_orthogonalProjection (p : P) {p' : P} {s : AffineSubspace ℝ P}
+    [s.direction.HasOrthogonalProjection] (h : p' ∈ s) :
+    haveI : Nonempty s := ⟨p', h⟩
+    ∠ p (orthogonalProjection s p) p' = π / 2 := by
+  haveI : Nonempty s := ⟨p', h⟩
+  rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
+  exact Submodule.inner_left_of_mem_orthogonal (K := s.direction)
+    (AffineSubspace.vsub_mem_direction h (orthogonalProjection_mem _))
+    (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
+
+@[simp] lemma angle_orthogonalProjection_self (p : P) {p' : P} {s : AffineSubspace ℝ P}
+    [s.direction.HasOrthogonalProjection] (h : p' ∈ s) :
+    haveI : Nonempty s := ⟨p', h⟩
+    ∠ p' (orthogonalProjection s p) p = π / 2 := by
+  rw [angle_comm, angle_self_orthogonalProjection p h]
+
+end EuclideanGeometry