From 14ecf272ce72f5a0fc056e866e99aa73692cdbf4 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Sun, 19 Nov 2023 16:40:40 +0800
Subject: [PATCH 01/11] write Vector and Parallel trash

prove easy theorems
---
 EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean   |  7 ++++++-
 .../Foundation/Axiom/Linear/Parallel_trash.lean        | 10 +++++++++-
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
index 93e93d40..f6e1c127 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
@@ -863,7 +863,12 @@ theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : det u v = 0 ↔ (
     rcases e
     ring
 
-theorem det_eq_zero_of_toProj_eq (u v : Vec_nd) (toprojeq : Vec_nd.toProj u = v.toProj) : det u v = 0 := ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).2) (smul_of_eq_toproj u v toprojeq)
+-- det theorems for Vec_nd
+theorem det_eq_zero_of_toProj_eq (u v : Vec_nd) (toprojeq : u.toProj = v.toProj) : det u v = 0 := ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).2) (smul_of_eq_toproj u v toprojeq)
+
+theorem toProj_eq_of_det_eq_zero (u v : Vec_nd) (det_eq_zero : det u v = 0) : u.toProj = v.toProj := (Vec_nd.eq_toproj_iff u v).mpr ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).1 det_eq_zero)
+
+theorem det_eq_zero_iff_toProj_eq (u v : Vec_nd) : det u v = 0 ↔ u.toProj = v.toProj := ⟨fun z => ((Vec_nd.eq_toproj_iff u v).mpr ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).1 z)), fun z => (((det_eq_zero_iff_eq_smul u.1 v.1 u.2).2) (smul_of_eq_toproj u v z))⟩
 
 theorem det'_ne_zero_of_not_colinear {u v : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : det' u v ≠ 0 := by
   unfold det'
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
index e873a279..b2f24f6e 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
@@ -5,6 +5,14 @@ namespace EuclidGeom
 
 variable {P : Type _} [EuclideanPlane P]
 
-theorem Seg_nd.not_para_rev_of_not_para (seg_nd seg_nd' : Seg_nd P) : (¬ seg_nd ∥ seg_nd') → (¬ seg_nd ∥ seg_nd'.reverse) := sorry
+-- Later we need a version of this theorem in class DirFig
+theorem Seg_nd.para_self_rev (seg_nd : Seg_nd P) : seg_nd ∥ seg_nd.reverse := Eq.symm (Seg_nd.toproj_of_rev_eq_toproj seg_nd)
+-- The followings are corollaries:
+
+theorem Seg_nd.para_rev_of_para (seg_nd seg_nd' : Seg_nd P) : (seg_nd ∥ seg_nd') ↔ (seg_nd ∥ seg_nd'.reverse) := ⟨fun z => Eq.trans z (Seg_nd.para_self_rev seg_nd'), fun z => Eq.trans z (Eq.symm (Seg_nd.para_self_rev seg_nd'))⟩
+
+theorem Seg_nd.not_para_rev_of_not_para (seg_nd seg_nd' : Seg_nd P) : (¬ seg_nd ∥ seg_nd') → (¬ seg_nd ∥ seg_nd'.reverse) := by
+  let g := (Seg_nd.para_rev_of_para seg_nd seg_nd').2
+  tauto
 
 end EuclidGeom

From 2e6f37b54fcff11d37eaadb43f6e9d2c52c47362 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Sun, 19 Nov 2023 17:12:06 +0800
Subject: [PATCH 02/11] prove theorems about triangles

kill some sorry
---
 .../Foundation/Axiom/Triangle/Basic.lean       |  7 ++++++-
 .../Foundation/Axiom/Triangle/Basic_ex.lean    | 18 ++++++++++--------
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index 22a36727..f40a3b17 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -81,8 +81,10 @@ variable {P : Type u} [EuclideanPlane P]
 
 namespace Triangle
 
+-- When we have DirFig, rewrite this definition.
 protected def IsInt (A : P) (tr : Triangle P) : Prop := by
   by_cases colinear tr.1 tr.2 tr.3
+  -- why not using ¬ tr.is_nd?
   · exact False
   · let tr_nd : Triangle_nd P := ⟨tr, h⟩
     exact (if tr_nd.is_cclock then A LiesOnLeft Seg_nd.toRay ⟨tr.edge₁, tr_nd.nontriv₁⟩ ∧ A LiesOnLeft Seg_nd.toRay ⟨tr.edge₂, tr_nd.nontriv₂⟩ ∧ A LiesOnLeft Seg_nd.toRay ⟨tr.edge₃, tr_nd.nontriv₃⟩ else A LiesOnRight Seg_nd.toRay ⟨tr.edge₁, tr_nd.nontriv₁⟩ ∧ A LiesOnRight Seg_nd.toRay ⟨tr.edge₂, tr_nd.nontriv₂⟩ ∧ A LiesOnRight Seg_nd.toRay ⟨tr.edge₃, tr_nd.nontriv₃⟩)
@@ -182,7 +184,10 @@ theorem angle_sum_eq_pi_of_cclock (cclock : tr_nd.is_cclock): tr_nd.angle₁.val
 
 theorem angle_sum_eq_neg_pi_of_clock (clock : ¬ tr_nd.is_cclock): tr_nd.angle₁.value + tr_nd.angle₂.value + tr_nd.angle₃.value = - π := sorry
 -/
-theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.length := sorry
+theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.length := by
+  have l₃ : tr.edge₃.length = norm (VEC tr.point₁ tr.point₂) := rfl
+  rw [l₃, ← neg_vec point₂ _, norm_neg, ← vec_add_vec point₂ point₃ point₁]
+  exact norm_add_le _ _
 
 theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := sorry
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
index 28bc97f8..2dcf5306 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
@@ -15,7 +15,7 @@ def perm_vertices : (Triangle P) where
 -- We decide not to define reverse permutation of triangles, just do composition twice.
 
 -- Permuting three times returns to the original triangle.
-theorem eq_self_of_perm_vertices_three_times : tr.perm_vertices.perm_vertices.perm_vertices = tr := by sorry
+theorem eq_self_of_perm_vertices_three_times : tr.perm_vertices.perm_vertices.perm_vertices = tr := rfl
 
 -- flip vertices for triangles means to flip the second and the third vertices.
 
@@ -24,14 +24,16 @@ def flip_vertices : (Triangle P) where
   point₂ := tr.point₃
   point₃ := tr.point₂
 
-theorem eq_self_of_flip_vertices_twice : tr.flip_vertices.flip_vertices = tr := by sorry
+theorem eq_self_of_flip_vertices_twice : tr.flip_vertices.flip_vertices = tr := rfl
 
 -- Not sure this is the best theorem to p
-theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr.flip_vertices.perm_vertices.perm_vertices = tr.perm_vertices.flip_vertices := by sorry
+theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr.flip_vertices.perm_vertices.perm_vertices = tr.perm_vertices.flip_vertices := rfl
 
-theorem is_inside_of_is_inside_perm_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.perm_vertices := by sorry
+theorem is_inside_of_is_inside_perm_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.perm_vertices := by
+  sorry
 
-theorem is_inside_of_is_inside_flip_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.flip_vertices := by sorry
+theorem is_inside_of_is_inside_flip_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.flip_vertices := by
+  sorry
 
 end Triangle
 
@@ -41,12 +43,12 @@ def perm_vertices : (Triangle_nd P) := ⟨tr_nd.1.perm_vertices, flip_colinear_s
 
 def flip_vertices : (Triangle_nd P) := ⟨tr_nd.1.flip_vertices, flip_colinear_snd_trd.mt tr_nd.2⟩
 
-theorem eq_self_of_perm_vertices_three_times : tr_nd.perm_vertices.perm_vertices.perm_vertices = tr_nd := by sorry
+theorem eq_self_of_perm_vertices_three_times : tr_nd.perm_vertices.perm_vertices.perm_vertices = tr_nd := rfl
   --exact tr_nd.1.eq_self_of_perm_vertices_three_times
 
-theorem eq_self_of_flip_vertices_twice : tr_nd.flip_vertices.flip_vertices = tr_nd := by sorry
+theorem eq_self_of_flip_vertices_twice : tr_nd.flip_vertices.flip_vertices = tr_nd := rfl
 
-theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr_nd.flip_vertices.perm_vertices.perm_vertices = tr_nd.perm_vertices.flip_vertices := by sorry
+theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr_nd.flip_vertices.perm_vertices.perm_vertices = tr_nd.perm_vertices.flip_vertices := rfl
 
 -- compatibility of permutation/flip of vertices with orientation of the triangle
 

From 288510f2f97aefd9fa14439627961c7e4a8d06c4 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Sun, 19 Nov 2023 17:27:27 +0800
Subject: [PATCH 03/11] create section Non_trivial_triangle_inequalities in
 Trignometric.lean

---
 .../Foundation/Axiom/Triangle/Basic.lean         |  6 +++++-
 .../Foundation/Axiom/Triangle/Trigonometric.lean | 16 ++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index f40a3b17..2ae5aeb1 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -189,11 +189,15 @@ theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.len
   rw [l₃, ← neg_vec point₂ _, norm_neg, ← vec_add_vec point₂ point₃ point₁]
   exact norm_add_le _ _
 
+-- The following theorems are corollaries of the sine and cosine theorems of the triangle
 theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := sorry
 
 theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd  := sorry
 
-theorem nontrivial_of_edge_sum_ne_edge : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd  := sorry -- should this theorem stated as ≠, or as > ???
+-- should this theorem stated as ≠, or as > ???
+theorem nontrivial_of_edge_sum_ne_edge : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd  := sorry
+
+theorem nontrivial_of_edge_sum_gt_edge : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length → tr.is_nd  := sorry
 
 theorem edge_sum_eq_edge_iff_colinear :  colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry
 /- area ≥ 0, nontrivial → >0, =0 → trivial -/
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
index c4a9c007..477d0218 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
@@ -97,4 +97,20 @@ theorem Pythagoras_of_tr_nd (tr_nd : Triangle_nd P) (h : tr_nd.angle₁.value =
 
 end Pythagoras
 
+section Non_trivial_triangle_inequalities
+
+theorem triangle_ineq' (tr_nd : Triangle_nd P) : tr_nd.edge₁.length + tr_nd.edge₂.length > tr_nd.edge₃.length := sorry
+
+theorem trivial_of_edge_sum_eq_edge (tr : Triangle P) : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd  := sorry
+
+-- should this theorem stated as ≠, or as > ???
+theorem nontrivial_of_edge_sum_ne_edge (tr : Triangle P) : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd  := sorry
+
+theorem nontrivial_of_edge_sum_gt_edge (tr : Triangle P) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length → tr.is_nd  := sorry
+
+theorem edge_sum_eq_edge_iff_colinear (tr : Triangle P) :  colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry
+/- area ≥ 0, nontrivial → >0, =0 → trivial -/
+
+end Non_trivial_triangle_inequalities
+
 end EuclidGeom

From d71cc8956ed7664a5b49e6a8d41613a7852c88e3 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Sun, 19 Nov 2023 18:29:47 +0800
Subject: [PATCH 04/11] simplify proofs and add theorems about norm_neg

---
 .../Foundation/Axiom/Basic/Vector.lean        | 11 ++++
 .../Foundation/Axiom/Triangle/Basic.lean      |  5 +-
 .../Axiom/Triangle/Trigonometric.lean         | 53 ++++++-------------
 3 files changed, 31 insertions(+), 38 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
index f6e1c127..d1fa9c4d 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
@@ -72,6 +72,13 @@ theorem Vec.norm_smul_eq_mul_norm {x : ℝ} (x_nonneg : 0 ≤ x) (u : Vec) : Vec
   simp only [Complex.real_smul, map_mul, Complex.abs_ofReal, mul_eq_mul_right_iff, abs_eq_self, map_eq_zero]
   tauto
 
+@[simp]
+theorem norm_neg_Vec_eq_norm_Vec (z : Vec) : Vec.norm (-z) = Vec.norm z := by
+  have h : Complex.abs (-z) = Complex.abs (z) := by
+    simp only [map_neg_eq_map]
+  unfold Vec.norm
+  rw [h]
+
 -- norm is nonnegetive
 theorem Vec.norm_nonnegative (u : Vec) : 0 ≤ Vec.norm u := Real.sqrt_nonneg _
 
@@ -102,6 +109,10 @@ theorem fst_of_mul_eq_fst_mul_fst (z w : Vec_nd) : (z * w).1 = z.1 * w.1 := by r
 @[simp]
 theorem norm_of_Vec_nd_eq_norm_of_Vec_nd_fst (z : Vec_nd) : Vec_nd.norm z = Vec.norm z := rfl
 
+@[simp]
+theorem neg_norm_eq_norm (x : Vec_nd) : (-x).norm = x.norm := by
+  simp only [ne_eq, fst_neg_Vec_nd_is_neg_fst_Vec_nd, norm_of_Vec_nd_eq_norm_of_Vec_nd_fst, norm_neg_Vec_eq_norm_Vec]
+
 @[ext]
 class Dir where
   toVec : Vec
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index 2ae5aeb1..d20a88e2 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -189,7 +189,8 @@ theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.len
   rw [l₃, ← neg_vec point₂ _, norm_neg, ← vec_add_vec point₂ point₃ point₁]
   exact norm_add_le _ _
 
--- The following theorems are corollaries of the sine and cosine theorems of the triangle
+-- The following theorems are corollaries of sine theorem and cosine theorem
+/-
 theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := sorry
 
 theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd  := sorry
@@ -202,6 +203,8 @@ theorem nontrivial_of_edge_sum_gt_edge : tr.edge₁.length + tr.edge₂.length >
 theorem edge_sum_eq_edge_iff_colinear :  colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry
 /- area ≥ 0, nontrivial → >0, =0 → trivial -/
 
+-/
+
 end Triangle
 
 namespace Triangle_nd
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
index 477d0218..46e7b922 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
@@ -17,43 +17,18 @@ theorem cosine_rule (tr_nd : Triangle_nd P) : 2 * (tr_nd.edge₃.length * tr_nd.
   let A := tr_nd.1.point₁
   let B := tr_nd.1.point₂
   let C := tr_nd.1.point₃
-  dsimp only [Seg.length]
-  simp
-  have h : ¬colinear A B C := (tr_nd).2
-  have h0 : B ≠ A := by
-    intro k
-    rw [←k] at h
-    exact h (triv_colinear B C)
-  have h1 : C ≠ A := by
-    intro k
-    rw [←k] at h
-    have p : ¬colinear C C B := by
-     intro k
-     exact h (flip_colinear_snd_trd k)
-    exact p (triv_colinear C B)
-  have h2 : A ≠ C := Ne.symm h1
-  have h3 : 2 * (Vec.norm (⟨VEC A B,(ne_iff_vec_ne_zero A B).mp h0⟩ : Vec_nd) * Vec.norm (⟨VEC A C,(ne_iff_vec_ne_zero A C).mp h1⟩ : Vec_nd) * Real.cos (Vec_nd.angle ⟨VEC A B,(ne_iff_vec_ne_zero A B).mp h0⟩ ⟨VEC A C,(ne_iff_vec_ne_zero A C).mp h1⟩)) = Seg.length (SEG A B) ^ 2 + Seg.length (SEG A C) ^ 2 - Seg.length (SEG B C) ^ 2 := cosine_rule' A B C h0 h1
-  have h4 : Vec.norm (⟨VEC A C,(ne_iff_vec_ne_zero A C).mp h1⟩ : Vec_nd) = Vec.norm (⟨VEC C A,(ne_iff_vec_ne_zero C A).mp h2⟩ : Vec_nd) := by
-    unfold Vec.norm; simp; unfold Vec.mk_pt_pt
-    have l0 : A -ᵥ C = -1 * (C -ᵥ A) := by
-      rw [neg_one_mul]
-      simp
-    rw [l0,map_mul Complex.abs (-1) (C -ᵥ A)]
-    have l1: Complex.abs (-1)=1 := by simp
-    rw [l1,one_mul]
-  have h5 : Seg.length (SEG A C)=Seg.length (SEG C A) := by
-    unfold Seg.length
-    simp; unfold Vec.mk_pt_pt
-    have l0 : A -ᵥ C = -1 * (C -ᵥ A) := by
-      rw [neg_one_mul]
-      simp
-    rw [l0,map_mul Complex.abs (-1) (C -ᵥ A)]
-    have l1 : Complex.abs (-1) = 1 := by simp
-    rw [l1,one_mul]
-  rw [h4] at h3
-  unfold Vec.norm at h3;
-  rw [h5] at h3; unfold Seg.length at h3; simp at h3
-  exact h3
+  let h₃ := cosine_rule' A B C (tr_nd.nontriv₃) (Ne.symm tr_nd.nontriv₂)
+  have h₄ : Vec.norm (⟨VEC A C, (ne_iff_vec_ne_zero A C).mp (Ne.symm tr_nd.nontriv₂)⟩ : Vec_nd) = Vec.norm (⟨VEC C A, (ne_iff_vec_ne_zero C A).mp (tr_nd.nontriv₂)⟩ : Vec_nd) := by
+    simp only [ne_eq]
+    rw [← neg_vec A C]
+    simp only [norm_neg_Vec_eq_norm_Vec]
+  have h₅ : Seg.length (SEG A C) = Seg.length (SEG C A) := by
+    unfold Seg.length Seg.toVec
+    rw [← neg_vec (SEG A C).target (SEG A C).source]
+    simp only [norm_neg, Complex.norm_eq_abs]
+  rw [h₄, h₅] at h₃
+  simp only [ne_eq, Nat.cast_ofNat] at h₃
+  exact h₃
 
 theorem cosine_rule'' (tr_nd : Triangle_nd P) : tr_nd.edge₁.length = (tr_nd.edge₃.length ^ 2 + tr_nd.edge₂.length ^ 2 -  2 * (tr_nd.edge₃.length * tr_nd.edge₂.length * Real.cos tr_nd.angle₁.value)) ^ (1/2) := by sorry
 
@@ -99,6 +74,8 @@ end Pythagoras
 
 section Non_trivial_triangle_inequalities
 
+namespace Triangle
+
 theorem triangle_ineq' (tr_nd : Triangle_nd P) : tr_nd.edge₁.length + tr_nd.edge₂.length > tr_nd.edge₃.length := sorry
 
 theorem trivial_of_edge_sum_eq_edge (tr : Triangle P) : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd  := sorry
@@ -111,6 +88,8 @@ theorem nontrivial_of_edge_sum_gt_edge (tr : Triangle P) : tr.edge₁.length + t
 theorem edge_sum_eq_edge_iff_colinear (tr : Triangle P) :  colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry
 /- area ≥ 0, nontrivial → >0, =0 → trivial -/
 
+end Triangle
+
 end Non_trivial_triangle_inequalities
 
 end EuclidGeom

From bd17f0f335e129a997eab502b503cf2c01fcc5b3 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Sun, 19 Nov 2023 23:58:50 +0800
Subject: [PATCH 05/11] prove triangle ineq

---
 .../Foundation/Axiom/Basic/Vector.lean        | 22 ++++++++++++
 .../Foundation/Axiom/Triangle/Basic.lean      | 36 +++++++++++++++----
 .../Axiom/Triangle/Trigonometric.lean         | 20 -----------
 3 files changed, 51 insertions(+), 27 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
index d1fa9c4d..044f8cd4 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
@@ -1,6 +1,7 @@
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
+import Mathlib.Analysis.Complex.Arg
 import Mathlib.Data.Real.Sign
 /-!
 # Standard Vector Space
@@ -465,6 +466,27 @@ theorem mk_angle_neg_pi_div_two_eq_neg_I' : mk_angle ((-π) / 2) = -I := by
 
 end Make_angle_theorems
 
+-- Here is a small section which would not be used later. We just compare our definitions to the standard sameRay definitions.
+section sameRay_theorems
+
+theorem sameRay_iff_eq (a b : Dir) : SameRay ℝ a.1 b.1 ↔ a = b := by
+  rw [Complex.sameRay_iff]
+  constructor
+  · simp only [tovec_ne_zero, false_or]
+    intro h
+    let g := congrArg (fun z => mk_angle z) h
+    simp only [mk_angle_arg_toComplex_of_Dir_eq_self] at g
+    exact g
+  · tauto
+
+theorem sameRay_Vec_nd_toDir (z : Vec_nd) : SameRay ℝ z.1 z.toDir.1 := by
+  rw [Complex.sameRay_iff_arg_div_eq_zero, Vec_nd.self_eq_norm_smul_todir z, Complex.real_smul, ← mul_div, div_self (tovec_ne_zero (Vec_nd.toDir z)), mul_one, norm_of_Vec_nd_eq_norm_of_Vec_nd_fst]
+  exact Complex.arg_ofReal_of_nonneg (Vec.norm_nonnegative z)
+
+theorem toDir_eq_toDir_of_sameRay (z₁ z₂ : Vec_nd) : SameRay ℝ z₁.1 z₂.1 → z₁.toDir = z₂.toDir := fun h => (sameRay_iff_eq z₁.toDir z₂.toDir).1 (SameRay.symm (SameRay.trans (SameRay.symm (SameRay.trans h (sameRay_Vec_nd_toDir z₂) (by simp only [ne_eq, ne_zero_of_Vec_nd, false_or, IsEmpty.forall_iff]))) (sameRay_Vec_nd_toDir z₁) (by simp only [ne_eq, ne_zero_of_Vec_nd, false_or, IsEmpty.forall_iff])))
+
+end sameRay_theorems
+
 instance : SMul Dir Vec where
   smul := fun d v => d.1 * v
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index d20a88e2..e7106f02 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -189,11 +189,35 @@ theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.len
   rw [l₃, ← neg_vec point₂ _, norm_neg, ← vec_add_vec point₂ point₃ point₁]
   exact norm_add_le _ _
 
--- The following theorems are corollaries of sine theorem and cosine theorem
-/-
-theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := sorry
-
-theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd  := sorry
+theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd  := by
+  let A := tr.point₁
+  let B := tr.point₂
+  let C := tr.point₃
+  have l₃ : tr.edge₃.length = norm (VEC A B) := rfl
+  rw [l₃, ← neg_vec B _, norm_neg, ← vec_add_vec B C A]
+  intro eq
+  unfold is_nd
+  let g := Complex.sameRay_iff.2 ((Complex.abs_add_eq_iff).1 eq.symm)
+  by_cases h₁ : VEC B C = 0
+  · simp only [(eq_iff_vec_eq_zero B C).2 h₁, not_not]
+    apply flip_colinear_fst_trd
+    exact triv_colinear _ _
+  · by_cases h₂ : VEC C A = 0
+    · simp only [(eq_iff_vec_eq_zero C A).2 h₂, not_not]
+      apply flip_colinear_snd_trd
+      exact triv_colinear _ _
+    · rcases SameRay.exists_pos g h₁ h₂ with ⟨_, ⟨_, ⟨_, ⟨_, g⟩⟩⟩⟩
+      rw [← neg_vec C B, ← neg_one_smul ℝ, ← mul_smul, mul_neg_one, ← eq_inv_smul_iff₀ (by linarith), ← mul_smul] at g
+      exact not_not.2 (perm_colinear_snd_trd_fst (colinear_of_vec_eq_smul_vec g))
+
+theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := by
+  have ne : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length := by
+    by_contra h
+    let g := trivial_of_edge_sum_eq_edge tr h
+    tauto
+  by_contra h
+  let g := eq_of_le_of_not_lt (triangle_ineq tr) h
+  tauto
 
 -- should this theorem stated as ≠, or as > ???
 theorem nontrivial_of_edge_sum_ne_edge : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd  := sorry
@@ -203,8 +227,6 @@ theorem nontrivial_of_edge_sum_gt_edge : tr.edge₁.length + tr.edge₂.length >
 theorem edge_sum_eq_edge_iff_colinear :  colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry
 /- area ≥ 0, nontrivial → >0, =0 → trivial -/
 
--/
-
 end Triangle
 
 namespace Triangle_nd
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
index 46e7b922..e404e6e8 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
@@ -72,24 +72,4 @@ theorem Pythagoras_of_tr_nd (tr_nd : Triangle_nd P) (h : tr_nd.angle₁.value =
 
 end Pythagoras
 
-section Non_trivial_triangle_inequalities
-
-namespace Triangle
-
-theorem triangle_ineq' (tr_nd : Triangle_nd P) : tr_nd.edge₁.length + tr_nd.edge₂.length > tr_nd.edge₃.length := sorry
-
-theorem trivial_of_edge_sum_eq_edge (tr : Triangle P) : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd  := sorry
-
--- should this theorem stated as ≠, or as > ???
-theorem nontrivial_of_edge_sum_ne_edge (tr : Triangle P) : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd  := sorry
-
-theorem nontrivial_of_edge_sum_gt_edge (tr : Triangle P) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length → tr.is_nd  := sorry
-
-theorem edge_sum_eq_edge_iff_colinear (tr : Triangle P) :  colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry
-/- area ≥ 0, nontrivial → >0, =0 → trivial -/
-
-end Triangle
-
-end Non_trivial_triangle_inequalities
-
 end EuclidGeom

From aa91fd54055e5b4a370abc4b0403abee2cb8cd48 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Mon, 20 Nov 2023 00:12:39 +0800
Subject: [PATCH 06/11] Update Basic.lean

add funny comments
---
 EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index e7106f02..6b47df75 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -219,11 +219,14 @@ theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.len
   let g := eq_of_le_of_not_lt (triangle_ineq tr) h
   tauto
 
--- should this theorem stated as ≠, or as > ???
-theorem nontrivial_of_edge_sum_ne_edge : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd  := sorry
+/- The following two theorems are totally wrong:
+
+theorem nontrivial_of_edge_sum_ne_edge : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd  := by
 
 theorem nontrivial_of_edge_sum_gt_edge : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length → tr.is_nd  := sorry
 
+So funny. Can you get it? -/
+
 theorem edge_sum_eq_edge_iff_colinear :  colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry
 /- area ≥ 0, nontrivial → >0, =0 → trivial -/
 

From 7c60c03e04ac3be0efccf7a8e569da59da0697f2 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Mon, 20 Nov 2023 00:39:59 +0800
Subject: [PATCH 07/11] Update Parallel_trash.lean

no more seg_nd
---
 EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
index b2f24f6e..e8d34e8b 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
@@ -6,7 +6,7 @@ namespace EuclidGeom
 variable {P : Type _} [EuclideanPlane P]
 
 -- Later we need a version of this theorem in class DirFig
-theorem Seg_nd.para_self_rev (seg_nd : Seg_nd P) : seg_nd ∥ seg_nd.reverse := Eq.symm (Seg_nd.toproj_of_rev_eq_toproj seg_nd)
+theorem Seg_nd.para_self_rev (seg_nd : Seg_nd P) : seg_nd ∥ seg_nd.reverse := Eq.symm (toproj_of_rev_eq_toproj)
 -- The followings are corollaries:
 
 theorem Seg_nd.para_rev_of_para (seg_nd seg_nd' : Seg_nd P) : (seg_nd ∥ seg_nd') ↔ (seg_nd ∥ seg_nd'.reverse) := ⟨fun z => Eq.trans z (Seg_nd.para_self_rev seg_nd'), fun z => Eq.trans z (Eq.symm (Seg_nd.para_self_rev seg_nd'))⟩

From 4d74e6e5b755ddc831605fdf8c165a5c5ee908aa Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Mon, 20 Nov 2023 01:24:43 +0800
Subject: [PATCH 08/11] Update Orientation.lean

simplify proofs
---
 .../Foundation/Axiom/Position/Orientation.lean  | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
index 85cb35e6..8b49f5d5 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
@@ -20,25 +20,14 @@ def wedge (A B C : P) : ℝ := det (VEC A B) (VEC A C)
 def oarea (A B C : P) : ℝ := wedge A B C / 2
 
 theorem wedge213 (A B C : P) : wedge B A C = - wedge A B C := by
-  dsimp only [wedge]
-  have h1 : VEC B A = (-1 : ℝ) • VEC A B := by
-    dsimp only [Vec.mk_pt_pt]
-    rw[Complex.real_smul]
-    field_simp
-  rw [h1, det_smul_left_eq_mul_det, det_eq_neg_det, det_eq_neg_det (VEC A B) _]
-  field_simp
-  have h2 : VEC B C = VEC A C - VEC A B := by
-    dsimp only [Vec.mk_pt_pt]
-    exact Eq.symm (vsub_sub_vsub_cancel_right C B A)
-  rw [h2, det_sub_eq_det]
+  unfold wedge
+  rw [← neg_vec A B, ← neg_one_smul ℝ, det_smul_left_eq_mul_det, det_eq_neg_det, det_eq_neg_det (VEC A B) _, neg_one_mul, neg_neg, neg_neg, ← vec_sub_vec A B C, det_sub_eq_det]
 
 theorem wedge132 (A B C : P) : wedge A C B = - wedge A B C := by
-  dsimp only [wedge]
   apply det_symm
 
 theorem wedge312 (A B C : P) : wedge C A B = wedge A B C := by
-  rw [wedge213, wedge132]
-  ring
+  rw [wedge213, wedge132, neg_neg]
 
 theorem wedge231 (A B C : P) : wedge B C A = wedge A B C := by rw [wedge312, wedge312]
 

From 964f18d41d3eacb75209073ac7e796f149ce7581 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Mon, 20 Nov 2023 01:35:02 +0800
Subject: [PATCH 09/11] Update Orientation.lean

simplify proofs and correct descriptions
---
 .../Axiom/Position/Orientation.lean           | 30 +++++++------------
 1 file changed, 11 insertions(+), 19 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
index 8b49f5d5..f51e23d1 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
@@ -33,17 +33,11 @@ theorem wedge231 (A B C : P) : wedge B C A = wedge A B C := by rw [wedge312, wed
 
 theorem wedge321 (A B C : P) : wedge C B A = - wedge A B C := by rw [wedge213, wedge231]
 
-theorem wedge_eq_sine_mul_length_mul_length (A B C : P) (aneb : B ≠ A) (anec : C ≠ A) : wedge A B C = (Real.sin (Angle.mk_pt_pt_pt B A C aneb anec).value * (SEG A B).length *(SEG A C).length) := by
-  dsimp only [wedge]
-  have vecabnd : VEC A B ≠ 0 := by
-   exact (ne_iff_vec_ne_zero A B).mp aneb
-  have vecacnd : VEC A C ≠ 0 := by
-   exact (ne_iff_vec_ne_zero A C).mp anec
-  have h0 : (Angle.mk_pt_pt_pt B A C aneb anec).value = Vec_nd.angle ⟨VEC A B , vecabnd⟩ ⟨VEC A C, vecacnd⟩ := by
-   dsimp only [Angle.mk_pt_pt_pt,Vec_nd.angle,angle_value_eq_dir_angle]
-   rfl
+theorem wedge_eq_sine_mul_length_mul_length (A B C : P) (bnea : B ≠ A) (cnea : C ≠ A) : wedge A B C = (Real.sin (Angle.mk_pt_pt_pt B A C bnea cnea).value * (SEG A B).length *(SEG A C).length) := by
+  unfold wedge
+  have h0 : (Angle.mk_pt_pt_pt B A C bnea cnea).value = Vec_nd.angle (VEC_nd A B bnea) (VEC_nd A C cnea)  := rfl
   rw [h0]
-  apply det_eq_sin_mul_norm_mul_norm ⟨VEC A B , vecabnd⟩ ⟨VEC A C, vecacnd⟩
+  apply det_eq_sin_mul_norm_mul_norm (VEC_nd A B bnea) (VEC_nd A C cnea)
 
 theorem colinear_iff_wedge_eq_zero (A B C : P) : (colinear A B C) ↔ (wedge A B C = 0) := by
   dsimp only [wedge]
@@ -118,15 +112,13 @@ theorem odist'_eq_sine_mul_length (A : P) (ray : Ray P) (h : A ≠ ray.source) :
   rw [mul_comm]
   rfl
 
-theorem wedge_eq_odist'_mul_length (A B C : P) (aneb : B ≠ A) : (wedge A B C) = ((odist' C (RAY A B aneb)) * (SEG A B).length) := by
+theorem wedge_eq_odist'_mul_length (A B C : P) (bnea : B ≠ A) : (wedge A B C) = ((odist' C (RAY A B bnea)) * (SEG A B).length) := by
   by_cases p : C ≠ A
-  rw [wedge_eq_sine_mul_length_mul_length A B C aneb p,odist'_eq_sine_mul_length C (RAY A B aneb),mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B aneb) C p).value)) ((SEG (RAY A B aneb).source C).length) ((SEG A B).length),mul_comm ((SEG (RAY A B aneb).source C).length) ((SEG A B).length),←mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B aneb) C p).value)) ((SEG A B).length) ((SEG (RAY A B aneb).source C).length)]
+  rw [wedge_eq_sine_mul_length_mul_length A B C bnea p,odist'_eq_sine_mul_length C (RAY A B bnea),mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B bnea) C p).value)) ((SEG (RAY A B bnea).source C).length) ((SEG A B).length),mul_comm ((SEG (RAY A B bnea).source C).length) ((SEG A B).length),←mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B bnea) C p).value)) ((SEG A B).length) ((SEG (RAY A B bnea).source C).length)]
   congr
-  simp at p
-  have vecac0 : VEC A C = 0 := (eq_iff_vec_eq_zero A C).mp p
-  have vecrayc0 : VEC (RAY A B aneb).source C = 0 := (eq_iff_vec_eq_zero A C).mp p
-  dsimp only [wedge,odist',det]
-  field_simp [vecac0,vecrayc0]
+  have vecrayc0 : VEC (RAY A B bnea).source C = 0 := (eq_iff_vec_eq_zero A C).mp (not_not.1 p)
+  dsimp only [wedge, odist', det]
+  field_simp [(eq_iff_vec_eq_zero A C).mp (not_not.1 p), vecrayc0]
 
 theorem odist'_eq_odist'_of_to_dirline_eq_to_dirline (A : P) (ray ray' : Ray P) (h : same_dir_line ray ray') : odist' A ray = odist' A ray' := by
   have h₁ : ray.2.1 =ray'.2.1 := by
@@ -213,11 +205,11 @@ end point_toray
 
 section oriented_area
 
-theorem oarea_eq_length_mul_odist_div_2 (A B C : P) (aneb : B ≠ A) : (oarea A B C) = ((odist C (Seg_nd.mk A B aneb)) * (SEG A B).length) / 2:= sorry
+theorem oarea_eq_length_mul_odist_div_2 (A B C : P) (bnea : B ≠ A) : (oarea A B C) = ((odist C (Seg_nd.mk A B bnea)) * (SEG A B).length) / 2:= sorry
 
 theorem oarea_eq_oarea_iff_odist_eq_odist_of_ne (A B C D : P) (bnea : B ≠ A) : (odist C (Seg_nd.mk A B bnea) = odist D (Seg_nd.mk A B bnea)) ↔ oarea A B C = oarea A B D := sorry
 
-theorem oarea_eq_sine_mul_length_mul_length_div_2 (A B C : P) (aneb : B ≠ A) (anec : C ≠ A) : oarea A B C = (Real.sin (Angle.mk_pt_pt_pt B A C aneb anec).value * (SEG A B).length *(SEG A C).length) / 2 := sorry
+theorem oarea_eq_sine_mul_length_mul_length_div_2 (A B C : P) (bnea : B ≠ A) (cnea : C ≠ A) : oarea A B C = (Real.sin (Angle.mk_pt_pt_pt B A C bnea cnea).value * (SEG A B).length *(SEG A C).length) / 2 := sorry
 
 theorem oarea_eq_zero_of_colinear (A B C : P) : oarea A B C = 0 ↔ colinear A B C := sorry
 

From 17582ff89a8688496d4e573dde5e893f97d8cc6a Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Mon, 20 Nov 2023 02:00:21 +0800
Subject: [PATCH 10/11] Update Angle.lean

prove a small theorem
---
 EuclideanGeometry/Foundation/Axiom/Position/Angle.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean
index 36ff6920..efd7479c 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean
@@ -98,7 +98,13 @@ instance : IntFig Angle where
 
 end Angle
 
-theorem eq_end_ray_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := sorry
+theorem eq_end_ray_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := by
+  ext : 1
+  rw [← ang₁.source_eq_source, ← ang₂.source_eq_source, (congrArg (fun z => z.source)) h]
+  let g := (congrArg (fun z => Dir.mk_angle z)) v
+  unfold Angle.value Dir.angle at g
+  simp only [Dir.mk_angle_arg_toComplex_of_Dir_eq_self, (congrArg (fun z => z.toDir)) h, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_self, mul_one] at g
+  exact g
 
 theorem eq_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁ = ang₂ := Angle.ext ang₁ ang₂ h (eq_end_ray_of_eq_value_eq_start_ray h v)
 

From 7aad918109fc38710de838b78aa6e16ad6884f74 Mon Sep 17 00:00:00 2001
From: cybcatppuccino <1538580589@qq.com>
Date: Mon, 20 Nov 2023 02:23:29 +0800
Subject: [PATCH 11/11] neg_norm_namings

namings
---
 EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean        | 6 +++---
 .../Foundation/Axiom/Triangle/Trigonometric.lean            | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
index 044f8cd4..b4d54173 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
@@ -74,7 +74,7 @@ theorem Vec.norm_smul_eq_mul_norm {x : ℝ} (x_nonneg : 0 ≤ x) (u : Vec) : Vec
   tauto
 
 @[simp]
-theorem norm_neg_Vec_eq_norm_Vec (z : Vec) : Vec.norm (-z) = Vec.norm z := by
+theorem neg_Vec_norm_eq_Vec_norm (z : Vec) : Vec.norm (-z) = Vec.norm z := by
   have h : Complex.abs (-z) = Complex.abs (z) := by
     simp only [map_neg_eq_map]
   unfold Vec.norm
@@ -111,8 +111,8 @@ theorem fst_of_mul_eq_fst_mul_fst (z w : Vec_nd) : (z * w).1 = z.1 * w.1 := by r
 theorem norm_of_Vec_nd_eq_norm_of_Vec_nd_fst (z : Vec_nd) : Vec_nd.norm z = Vec.norm z := rfl
 
 @[simp]
-theorem neg_norm_eq_norm (x : Vec_nd) : (-x).norm = x.norm := by
-  simp only [ne_eq, fst_neg_Vec_nd_is_neg_fst_Vec_nd, norm_of_Vec_nd_eq_norm_of_Vec_nd_fst, norm_neg_Vec_eq_norm_Vec]
+theorem neg_Vec_nd_norm_eq_Vec_nd_norm (x : Vec_nd) : (-x).norm = x.norm := by
+  simp only [ne_eq, fst_neg_Vec_nd_is_neg_fst_Vec_nd, norm_of_Vec_nd_eq_norm_of_Vec_nd_fst, neg_Vec_norm_eq_Vec_norm]
 
 @[ext]
 class Dir where
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
index e404e6e8..3b773534 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
@@ -21,7 +21,7 @@ theorem cosine_rule (tr_nd : Triangle_nd P) : 2 * (tr_nd.edge₃.length * tr_nd.
   have h₄ : Vec.norm (⟨VEC A C, (ne_iff_vec_ne_zero A C).mp (Ne.symm tr_nd.nontriv₂)⟩ : Vec_nd) = Vec.norm (⟨VEC C A, (ne_iff_vec_ne_zero C A).mp (tr_nd.nontriv₂)⟩ : Vec_nd) := by
     simp only [ne_eq]
     rw [← neg_vec A C]
-    simp only [norm_neg_Vec_eq_norm_Vec]
+    simp only [neg_Vec_norm_eq_Vec_norm]
   have h₅ : Seg.length (SEG A C) = Seg.length (SEG C A) := by
     unfold Seg.length Seg.toVec
     rw [← neg_vec (SEG A C).target (SEG A C).source]