From 58f4fd110831b85a8ae5924a02cef4f58dfb9c9c Mon Sep 17 00:00:00 2001
From: Tony Beta Lambda <tonybetalambda@gmail.com>
Date: Wed, 17 Jan 2024 17:55:50 +0800
Subject: [PATCH 1/2] prove perpendicular from inner product zero

---
 .../Axiom/Linear/Perpendicular.lean           | 27 +++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
index 5b0b6098..6eb33537 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
@@ -105,4 +105,31 @@ theorem eq_dist_eq_perp_foot {A B : P} {l : DirLine P} (h : A LiesOn l) (heq : d
 
 end Perpendicular_constructions
 
+section Perpendicular_inner_product
+
+theorem perp_of_inner_product_eq_zero (v w : VecND) (h : inner v.1 w.1 = (0 : ℝ)) : v ⟂ w := by
+  unfold perpendicular Proj.perp
+  rw [Proj.vadd_coe_left]
+  unfold Dir.rotate
+  erw [Proj.map_vecND_toProj]
+  simp only [Dir.map_apply, ne_eq, LinearEquiv.restrictScalars_apply, VecND.toDir_toProj]
+  erw [VecND.toProj_eq_toProj_iff]
+  obtain ⟨ ⟨ xv, yv ⟩, hv ⟩ := v
+  obtain ⟨ ⟨ xw, yw ⟩, hw ⟩ := w
+  rw [Vec.real_inner_apply] at h
+  simp only [Vec.rotate_mk, AngValue.cos_coe, Real.cos_pi_div_two, zero_mul, AngValue.sin_coe, Real.sin_pi_div_two, one_mul, zero_sub, zero_add, Vec.smul_mk, mul_neg, Vec.mk.injEq] at h ⊢
+  have : xw ≠ 0 ∨ yw ≠ 0 := by
+    contrapose! hw
+    obtain ⟨rfl, rfl⟩ := hw
+    rfl
+  rcases this with (h | h)
+  · use yv / xw
+    field_simp
+    linarith
+  · use -xv / yw
+    field_simp
+    linarith
+
+end Perpendicular_inner_product
+
 end EuclidGeom

From eb903d0cffcb1f06b13580233ab02cdf06153382 Mon Sep 17 00:00:00 2001
From: Tony Beta Lambda <tonybetalambda@gmail.com>
Date: Wed, 17 Jan 2024 19:38:26 +0800
Subject: [PATCH 2/2] prove inner product zero from perpendicular

---
 .../Foundation/Axiom/Linear/Perpendicular.lean | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
index 6eb33537..e667681b 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
@@ -110,7 +110,6 @@ section Perpendicular_inner_product
 theorem perp_of_inner_product_eq_zero (v w : VecND) (h : inner v.1 w.1 = (0 : ℝ)) : v ⟂ w := by
   unfold perpendicular Proj.perp
   rw [Proj.vadd_coe_left]
-  unfold Dir.rotate
   erw [Proj.map_vecND_toProj]
   simp only [Dir.map_apply, ne_eq, LinearEquiv.restrictScalars_apply, VecND.toDir_toProj]
   erw [VecND.toProj_eq_toProj_iff]
@@ -122,7 +121,7 @@ theorem perp_of_inner_product_eq_zero (v w : VecND) (h : inner v.1 w.1 = (0 : 
     contrapose! hw
     obtain ⟨rfl, rfl⟩ := hw
     rfl
-  rcases this with (h | h)
+  rcases this
   · use yv / xw
     field_simp
     linarith
@@ -130,6 +129,21 @@ theorem perp_of_inner_product_eq_zero (v w : VecND) (h : inner v.1 w.1 = (0 : 
     field_simp
     linarith
 
+theorem inner_product_eq_zero_of_perp (v w : VecND) (h : v ⟂ w) : inner v.1 w.1 = (0 : ℝ) := by
+  unfold perpendicular Proj.perp at h
+  rw [Proj.vadd_coe_left] at h
+  erw [Proj.map_vecND_toProj] at h
+  simp only [Dir.map_apply, ne_eq, LinearEquiv.restrictScalars_apply, VecND.toDir_toProj] at h 
+  erw [VecND.toProj_eq_toProj_iff] at h
+  obtain ⟨ ⟨ xv, yv ⟩, hv ⟩ := v
+  obtain ⟨ ⟨ xw, yw ⟩, hw ⟩ := w
+  rw [Vec.real_inner_apply]
+  simp only [Vec.rotate_mk, AngValue.cos_coe, Real.cos_pi_div_two, zero_mul, AngValue.sin_coe, Real.sin_pi_div_two, one_mul, zero_sub, zero_add, Vec.smul_mk, mul_neg, Vec.mk.injEq] at h ⊢
+  obtain ⟨a, ⟨ h₁, h₂ ⟩⟩ := h
+  rw [h₁, h₂]
+  linarith
+
+
 end Perpendicular_inner_product
 
 end EuclidGeom