write Vector and Parallel trash

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
@@ -72,6 +73,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 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
+  rw [h]
+
 -- norm is nonnegetive
 theorem Vec.norm_nonnegative (u : Vec) : 0 ≤ Vec.norm u := Real.sqrt_nonneg _
 
@@ -102,6 +110,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_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
   toVec : Vec
@@ -454,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
 
@@ -863,7 +896,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'

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 (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'))⟩
+
+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

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)
 

EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean

@@ -20,41 +20,24 @@ 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]
 
 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]
@@ -129,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
@@ -224,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
 

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,13 +184,48 @@ 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' (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 > ???
+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 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
+
+/- 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 -/

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
 

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 [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]
+    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