Merge pull request #282 from mbkybky/master

Complete Position/Angle.lean and Clean trash of Ray.lean

EuclideanGeometry/Example/SCHAUM/Problem1.5.lean

@@ -95,13 +95,13 @@ As a consequence, we know that $PQRS$ is a parallelogram.
       -- Since $P$ lies on $AB$, we have $AP, AB$ are of the same direction,
       _= (SEG_nd e.A e.B B_ne_A).toDir := by
         symm;
-        exact eq_todir_of_lies_int_seg_nd e.A e.B e.P B_ne_A e.P_int_AB
+        exact SegND.toDir_eq_of_lies_int e.A e.B e.P B_ne_A e.P_int_AB
       -- in parallelogram $ABCD$, we have $AB, DC$ are of the same direction,
       _= (SEG_nd e.D e.C C_ne_D).toDir := todir_eq_of_is_prg_nd e.A e.B e.C e.D e.hprgnd B_ne_A C_ne_D
       -- $CD, DC$ are of the opposite direction because of symmetry,
       _= - (SEG_nd e.C e.D C_ne_D.symm).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.D C_ne_D.symm))
       -- since $R$ lies on $CD$, we have $CR, CD$ are of the same direction,
-      _= - (SEG_nd e.C e.R R_ne_C).toDir := by simp only [eq_todir_of_lies_int_seg_nd e.C e.D e.R C_ne_D.symm e.R_int_CD]
+      _= - (SEG_nd e.C e.R R_ne_C).toDir := by simp only [SegND.toDir_eq_of_lies_int e.C e.D e.R C_ne_D.symm e.R_int_CD]
       -- $CR, RC$ are of the opposite direction because of symmetry.
       _= (SEG_nd e.R e.C R_ne_C.symm).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.R R_ne_C))
     -- We have $AP = RC$.
@@ -125,13 +125,13 @@ As a consequence, we know that $PQRS$ is a parallelogram.
       -- Since $S$ lies on $AD$, we have $AS, AD$ are of the same direction,
       _= (SEG_nd e.A e.D D_ne_A).toDir := by
         symm;
-        exact eq_todir_of_lies_int_seg_nd e.A e.D e.S D_ne_A S_int_AD
+        exact SegND.toDir_eq_of_lies_int e.A e.D e.S D_ne_A S_int_AD
       -- in parallelogram $ABCD$, we have $AD, BC$ are of the same direction,
       _= (SEG_nd e.B e.C C_ne_B).toDir := todir_eq_of_is_prg_nd_variant e.A e.B e.C e.D e.hprgnd D_ne_A C_ne_B
       -- $BC, CB$ are of the opposite direction because of symmetry,
       _= - (SEG_nd e.C e.B C_ne_B.symm).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.B C_ne_B.symm))
       -- since $Q$ lies on $CB$, we have $CQ, CB$ are of the same direction,
-      _= - (SEG_nd e.C e.Q Q_ne_C).toDir := by simp only [eq_todir_of_lies_int_seg_nd e.C e.B e.Q C_ne_B.symm Q_int_CB]
+      _= - (SEG_nd e.C e.Q Q_ne_C).toDir := by simp only [SegND.toDir_eq_of_lies_int e.C e.B e.Q C_ne_B.symm Q_int_CB]
       -- $CQ, QC$ are of the opposite direction because of symmetry.
       _= (SEG_nd e.Q e.C Q_ne_C.symm).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.Q Q_ne_C))
     -- We have $AS = QC$.
@@ -169,7 +169,7 @@ As a consequence, we know that $PQRS$ is a parallelogram.
     _= (SEG e.S e.Q).midpoint := by
       exact eq_midpt_of_diag_inx_of_is_prg_nd'_variant isprgnd_ASCQ
     -- the midpoint of $SQ$ is the same as the midpoint of $QS$ by symmetry.
-    _= (SEG e.Q e.S).midpoint := midpt_of_rev_eq_midpt e.S e.Q
+    _= (SEG e.Q e.S).midpoint := (SEG e.Q e.S).reverse_midpt_eq_midpt
   -- We have that $ABCD$ is convex, since it's a nondegenerate parallelogram.
   have hprgnd' : (QDR e.A e.B e.C e.D) IsPRG_nd := e.hprgnd
   have cvx_ABCD : (QDR e.A e.B e.C e.D).IsConvex := by

EuclideanGeometry/Example/SCHAUM/Problem1.7.lean

@@ -82,7 +82,6 @@ Therefore, $DX = EY$.
   have E_int_ray_CB : e.E LiesInt (RAY e.C e.B C_ne_B.symm) := by
     -- It suffices to prove that $E$ lies on segment $CB$.
     apply SegND.lies_int_toRay_of_lies_int (seg_nd := (SEG_nd e.C e.B C_ne_B.symm))
-    apply lies_int_seg_nd_of_lies_int_seg e.C e.B e.E C_ne_B.symm _
     -- By symmetry, we only need to show that $E$ lies on segment $BC$,
     apply (Seg.lies_int_rev_iff_lies_int (seg := (SEG e.B e.C))).mpr
     -- which is what we already know.
@@ -115,7 +114,7 @@ Therefore, $DX = EY$.
     -- It suffices to prove that $D$ lies on segment $BC$.
     apply SegND.lies_int_toRay_of_lies_int (seg_nd := (SEG_nd e.B e.C C_ne_B))
     -- which is what we already know.
-    exact lies_int_seg_nd_of_lies_int_seg e.B e.C e.D C_ne_B e.D_int_BC
+    exact e.D_int_BC
   -- We have that $X$ lies on ray $BA$.
   have X_int_ray_BA : e.X LiesInt (RAY e.B e.A A_ne_B) := by
     simp only [e.hd, Line.line_of_pt_pt_eq_rev A_ne_B.symm]

EuclideanGeometry/Example/SCHAUM/Problem1.8.lean

@@ -89,8 +89,8 @@ Therefore, $BD = CE$.
     -- Since $D$ lies on the extension of $BC$, we know that $\angle DBA$ is the same as $\angle CBA$.
     _= ∠ e.C e.B e.A B_ne_C.symm e.A_ne_B := by
       symm;
-      apply Angle.value_eq_of_lies_on_ray_pt_pt (e.B_ne_C.symm) e.A_ne_B D_ne_B e.A_ne_B
-      · exact lies_int_toray_of_lies_int_ext_of_seg_nd e.B e.C e.D e.B_ne_C.symm e.D_int_BC_ext
+      apply Angle.value_eq_of_lies_on_ray_pt_pt e.A_ne_B D_ne_B e.A_ne_B
+      · exact lies_int_toRay_of_lies_int_extn e.B e.C e.D e.B_ne_C.symm e.D_int_BC_ext
       · exact Ray.snd_pt_lies_int_mk_pt_pt e.B e.A e.A_ne_B
     -- In regular triangle $ABC$, $\angle CBA = \angle ACB$.
     _= ∠ e.A e.C e.B A_ne_C e.B_ne_C := by
@@ -99,7 +99,7 @@ Therefore, $BD = CE$.
     -- Since $E$ lies on the extension of $CA$, we know that $\angle BCA$ is the same as $\angle ECB$.
     _= ∠ e.E e.C e.B E_ne_C e.B_ne_C := by
       apply Angle.value_eq_of_lies_on_ray_pt_pt A_ne_C e.B_ne_C E_ne_C e.B_ne_C
-      · exact lies_int_toray_of_lies_int_ext_of_seg_nd e.C e.A e.E A_ne_C e.E_int_CA_ext
+      · exact lies_int_toRay_of_lies_int_extn e.C e.A e.E A_ne_C e.E_int_CA_ext
       · exact Ray.snd_pt_lies_int_mk_pt_pt e.C e.B e.B_ne_C
   -- We have $BD = CE$.
   have BD_eq_CE : (SEG e.B e.D).length = (SEG e.C e.E).length := by

EuclideanGeometry/Example/SCHAUM/Problem1.9.lean

@@ -9,6 +9,8 @@ namespace Schaum
 
 namespace Problem1_9
 
+open Angle
+
 /-
 Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$. Let $E$ be a point on the extension of $BA$.Let X be a point on the ray through $A$ with the same direction to $\vec{BC}$.
 
@@ -113,7 +115,7 @@ Therefore, $\angle EAX = \angle ABC = - \angle ACB = \angle XAC$.
   calc
   ∠ e.E e.A e.X e.E_ne_A e.X_ne_A
   -- As $AE$ has the same direction as $BA$ and that $AX$ has the same direction as $BC$, we know that $\angle EAX = \angle ABC$,
-  _= ∠ e.A e.B e.C e.B_ne_A.symm e.C_ne_B := ang_eq_ang_of_toDir_eq_toDir dir_AE_eq_dir_BA dir_AX_eq_dir_BC
+  _= ∠ e.A e.B e.C e.B_ne_A.symm e.C_ne_B := value_eq_of_dir_eq dir_AE_eq_dir_BA dir_AX_eq_dir_BC
   -- $\angle ABC = - \angle CBA$ by symmetry,
   _= - ∠ e.C e.B e.A e.C_ne_B e.B_ne_A.symm := by exact neg_value_of_rev_ang e.B_ne_A.symm e.C_ne_B
   -- $ - \angle CBA = - \angle ACB$ because $\angle CBA = \angle ACB$ in the isoceles triangle $ABC$,

EuclideanGeometry/Example/ShanZun/Ex1a.lean

@@ -30,10 +30,8 @@ variable {E : P} {he : E = (SEG A B).midpoint}
 theorem Shan_Problem_1_3 : (SEG C D).length = 2 * (SEG C E).length := by
   -- Extend $AC$ to $F$ such that $CF = AC$
   let F := Ray.extpoint (SEG_nd A C c_ne_a).extension (SEG A C).length
-  have cf_eq_ac : (SEG C F).length = (SEG A C).length := by
-    apply seg_length_eq_dist_of_extpoint (SEG_nd A C c_ne_a).extension
-    simp
-    exact length_nonneg
+  have cf_eq_ac : (SEG C F).length = (SEG A C).length :=
+    (SEG_nd A C c_ne_a).extension.dist_of_extpoint (SEG A C).length_nonneg
   -- $\triangle A B F$ is congruent to $\triangle A C D$, so $BF = CD$
   have iso : (▵ A B F) ≅ₐ (▵ A C D) := sorry
   have bf_eq_cd : (SEG B F).length = (SEG C D).length := iso.edge₁
@@ -63,10 +61,8 @@ variable {D : P} {hd : D = perp_foot A (LIN B C B_ne_C.symm)}
 theorem Shan_Problem_1_4 : (SEG B D).length = (SEG A C).length + (SEG C D).length := by
   -- Extend $BC$ to $E$ such that $CE = CA$
   let E := Ray.extpoint (SEG_nd B C B_ne_C.symm).extension (SEG C A).length
-  have ce_eq_ca : (SEG C E).length = (SEG C A).length := by
-    apply seg_length_eq_dist_of_extpoint (SEG_nd B C B_ne_C.symm).extension
-    simp
-    exact length_nonneg
+  have ce_eq_ca : (SEG C E).length = (SEG C A).length :=
+    (SEG_nd B C B_ne_C.symm).extension.dist_of_extpoint (SEG C A).length_nonneg
   -- $DE = AC + CD$
   have de_eq_ac_plus_cd : (SEG D E).length = (SEG A C).length + (SEG C D).length := sorry
   -- $C A E$ is not colinear

EuclideanGeometry/Example/ShanZun/Ex1d.lean

@@ -86,10 +86,8 @@ theorem Shan_Problem_1_10 : (SEG A D).length = (SEG D C).length := by
   have a_ne_e : A ≠ E := sorry
   -- Extend $EA$ to $M$ such that $AM = EC$
   let M := Ray.extpoint (SEG_nd E A a_ne_e).extension (SEG E C).length
-  have am_eq_ec : (SEG A M).length = (SEG E C).length := by
-    apply seg_length_eq_dist_of_extpoint (SEG_nd E A a_ne_e).extension
-    simp
-    exact length_nonneg
+  have am_eq_ec : (SEG A M).length = (SEG E C).length :=
+    (SEG_nd E A a_ne_e).extension.dist_of_extpoint (SEG E C).length_nonneg
   -- Claim: $M \ne C$, $B \ne M$
   have m_ne_c : M ≠ C := sorry
   have b_ne_m : B ≠ M := sorry

EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean

@@ -418,11 +418,15 @@ theorem isND_iff : θ.IsND ↔ θ ≠ 0 ∧ θ ≠ π :=
 theorem not_isND_iff : ¬ θ.IsND ↔ (θ = 0 ∨ θ = π) :=
   (not_iff_not.mpr θ.isND_iff).trans or_iff_not_and_not.symm
 
-theorem isND_iff_two_nsmul_ne_zero : θ.IsND ↔ 2 • θ ≠ 0 :=
-  (θ.isND_iff).trans (θ.two_nsmul_ne_zero_iff).symm
+theorem two_nsmul_ne_zero_iff_isND : 2 • θ ≠ 0 ↔ θ.IsND :=
+  (θ.two_nsmul_ne_zero_iff).trans (θ.isND_iff).symm
 
-theorem not_isND_iff_two_nsmul_eq_zero : ¬ θ.IsND ↔ 2 • θ = 0 :=
-  (θ.not_isND_iff).trans (θ.two_nsmul_eq_zero_iff).symm
+theorem two_nsmul_eq_zero_iff_not_isND : 2 • θ = 0 ↔ ¬ θ.IsND :=
+  (θ.two_nsmul_eq_zero_iff).trans (θ.not_isND_iff).symm
+
+theorem ne_neg_self_iff_isND : θ ≠ - θ ↔ θ.IsND := sorry
+
+theorem eq_neg_self_iff_not_isND : θ = - θ ↔ ¬ θ.IsND := sorry
 
 theorem not_isND_iff_coe : ¬ θ.IsND ↔ θ = (0 : AngDValue) :=
   not_isND_iff.trans (θ.coe_eq_zero_iff).symm
@@ -865,7 +869,7 @@ section cos
 theorem isAcu_iff_zero_lt_cos : θ.IsAcu ↔ 0 < cos θ :=
   (θ.isAcu_iff).trans (θ.zero_lt_cos_iff).symm
 
-theorem isObt_iff_zero_lt_cos : θ.IsObt ↔ cos θ < 0 :=
+theorem isObt_iff_cos_lt_zero : θ.IsObt ↔ cos θ < 0 :=
   (θ.isObt_iff).trans (θ.cos_lt_zero_iff).symm
 
 theorem isRight_iff_cos_eq_zero : θ.IsRight ↔ cos θ = 0 :=
@@ -898,7 +902,7 @@ theorem not_isRight_of_eq_zero (h : θ = 0) : ¬ θ.IsRight := by
   exact zero_not_isRight
 
 theorem pi_isObt : ∠[π].IsObt := by
-  simp only [isObt_iff_zero_lt_cos, cos_coe, cos_pi, Left.neg_neg_iff, zero_lt_one]
+  simp only [isObt_iff_cos_lt_zero, cos_coe, cos_pi, Left.neg_neg_iff, zero_lt_one]
 
 theorem pi_not_isAcu : ¬ ∠[π].IsAcu := not_isAcu_of_isObt pi_isObt
 
@@ -926,7 +930,7 @@ theorem neg_isAcu_iff_isAcu : (- θ).IsAcu ↔ θ.IsAcu := by
 
 @[simp]
 theorem neg_isObt_iff_isObt : (- θ).IsObt ↔ θ.IsObt := by
-  simp only [isObt_iff_zero_lt_cos, cos_neg]
+  simp only [isObt_iff_cos_lt_zero, cos_neg]
 
 @[simp]
 theorem neg_isRight_iff_isRight : (- θ).IsRight ↔ θ.IsRight := by
@@ -938,11 +942,11 @@ section add_pi
 
 @[simp]
 theorem add_pi_isAcu_iff_isObt : (θ + π).IsAcu ↔ θ.IsObt := by
-  rw [isAcu_iff_zero_lt_cos, cos_add_pi, Left.neg_pos_iff, isObt_iff_zero_lt_cos]
+  rw [isAcu_iff_zero_lt_cos, cos_add_pi, Left.neg_pos_iff, isObt_iff_cos_lt_zero]
 
 @[simp]
 theorem add_pi_isObt_iff_isAcu : (θ + π).IsObt ↔ θ.IsAcu := by
-  rw [isAcu_iff_zero_lt_cos, isObt_iff_zero_lt_cos, cos_add_pi, Left.neg_neg_iff]
+  rw [isAcu_iff_zero_lt_cos, isObt_iff_cos_lt_zero, cos_add_pi, Left.neg_neg_iff]
 
 @[simp]
 theorem add_pi_isRight_iff_isRight : (θ + π).IsRight ↔ θ.IsRight := by
@@ -972,11 +976,11 @@ section pi_sub
 
 @[simp]
 theorem pi_sub_isAcu_iff_isObt : (π - θ).IsAcu ↔ θ.IsObt := by
-  rw [isAcu_iff_zero_lt_cos, cos_pi_sub, Left.neg_pos_iff, isObt_iff_zero_lt_cos]
+  rw [isAcu_iff_zero_lt_cos, cos_pi_sub, Left.neg_pos_iff, isObt_iff_cos_lt_zero]
 
 @[simp]
 theorem pi_sub_isObt_iff_isAcu : (π - θ).IsObt ↔ θ.IsAcu := by
-  rw [isAcu_iff_zero_lt_cos, isObt_iff_zero_lt_cos, cos_pi_sub, Left.neg_neg_iff]
+  rw [isAcu_iff_zero_lt_cos, isObt_iff_cos_lt_zero, cos_pi_sub, Left.neg_neg_iff]
 
 @[simp]
 theorem pi_sub_isRight_iff_isRight : (π - θ).IsRight ↔ θ.IsRight := by
@@ -996,7 +1000,7 @@ theorem add_pi_div_two_isPos_iff_isAcu : (θ + ∠[π / 2]).IsPos ↔ θ.IsAcu :
   rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, sin_add_pi_div_two]
 
 theorem add_pi_div_two_isNeg_iff_isObt : (θ + ∠[π / 2]).IsNeg ↔ θ.IsObt := by
-  rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, sin_add_pi_div_two]
+  rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, sin_add_pi_div_two]
 
 theorem add_pi_div_two_not_isND_iff_isRight : ¬ (θ + ∠[π / 2]).IsND ↔ θ.IsRight := by
   rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, sin_add_pi_div_two]
@@ -1008,7 +1012,7 @@ theorem add_pi_div_two_isAcu_iff_isNeg : (θ + ∠[π / 2]).IsAcu ↔ θ.IsNeg :
   rw [isNeg_iff_sin_lt_zero, isAcu_iff_zero_lt_cos, cos_add_pi_div_two, Left.neg_pos_iff]
 
 theorem add_pi_div_two_isObt_iff_isPos : (θ + ∠[π / 2]).IsObt ↔ θ.IsPos := by
-  rw [isPos_iff_zero_lt_sin, isObt_iff_zero_lt_cos, cos_add_pi_div_two, Left.neg_neg_iff]
+  rw [isPos_iff_zero_lt_sin, isObt_iff_cos_lt_zero, cos_add_pi_div_two, Left.neg_neg_iff]
 
 theorem add_pi_div_two_isRight_iff_not_isND : (θ + ∠[π / 2]).IsRight ↔ ¬ θ.IsND := by
   rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, cos_add_pi_div_two, neg_eq_zero]
@@ -1017,7 +1021,7 @@ theorem add_pi_div_two_not_isRight_iff_isND : ¬ (θ + ∠[π / 2]).IsRight ↔
   rw [isND_iff_sin_ne_zero, isRight_iff_cos_eq_zero, cos_add_pi_div_two, neg_eq_zero]
 
 theorem sub_pi_div_two_isPos_iff_isObt : (θ - ∠[π / 2]).IsPos ↔ θ.IsObt := by
-  rw [isPos_iff_zero_lt_sin, isObt_iff_zero_lt_cos, sin_sub_pi_div_two, Left.neg_pos_iff]
+  rw [isPos_iff_zero_lt_sin, isObt_iff_cos_lt_zero, sin_sub_pi_div_two, Left.neg_pos_iff]
 
 theorem sub_pi_div_two_isNeg_iff_isAcu : (θ - ∠[π / 2]).IsNeg ↔ θ.IsAcu := by
   rw [isNeg_iff_sin_lt_zero, isAcu_iff_zero_lt_cos, sin_sub_pi_div_two, Left.neg_neg_iff]
@@ -1032,7 +1036,7 @@ theorem sub_pi_div_two_isAcu_iff_isPos : (θ - ∠[π / 2]).IsAcu ↔ θ.IsPos :
   rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, cos_sub_pi_div_two]
 
 theorem sub_pi_div_two_isObt_iff_isNeg : (θ - ∠[π / 2]).IsObt ↔ θ.IsNeg := by
-  rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, cos_sub_pi_div_two]
+  rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, cos_sub_pi_div_two]
 
 theorem sub_pi_div_two_isRight_iff_not_isND : (θ - ∠[π / 2]).IsRight ↔ ¬ θ.IsND := by
   rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, cos_sub_pi_div_two]
@@ -1044,7 +1048,7 @@ theorem pi_div_two_sub_isPos_iff_isAcu : (∠[π / 2] - θ).IsPos ↔ θ.IsAcu :
   rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, sin_pi_div_two_sub]
 
 theorem pi_div_two_sub_isNeg_iff_isAcu : (∠[π / 2] - θ).IsNeg ↔ θ.IsObt := by
-  rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, sin_pi_div_two_sub]
+  rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, sin_pi_div_two_sub]
 
 theorem pi_div_two_sub_not_isND_iff_isRight : ¬ (∠[π / 2] - θ).IsND ↔ θ.IsRight := by
   rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, sin_pi_div_two_sub]
@@ -1056,7 +1060,7 @@ theorem pi_div_two_sub_isAcu_iff_isPos : (∠[π / 2] - θ).IsAcu ↔ θ.IsPos :
   rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, cos_pi_div_two_sub]
 
 theorem pi_div_two_sub_isObt_iff_isNeg : (∠[π / 2] - θ).IsObt ↔ θ.IsNeg := by
-  rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, cos_pi_div_two_sub]
+  rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, cos_pi_div_two_sub]
 
 theorem pi_div_two_sub_isRight_iff_not_isND : (∠[π / 2] - θ).IsRight ↔ ¬ θ.IsND := by
   rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, cos_pi_div_two_sub]

EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean

@@ -1634,6 +1634,9 @@ instance : AddTorsor AngDValue Proj where
     induction p using Proj.ind
     simp
 
+instance instCircularOrderedAddTorsor : CircularOrderedAddTorsor AngDValue Proj :=
+  AddTorsor.CircularOrderedAddTorsor_of_CircularOrderedAddCommGroup AngDValue Proj
+
 @[pp_dot]
 def perp (p : Proj) : Proj := ∡[π / 2] +ᵥ p
 

EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean

@@ -133,7 +133,7 @@ theorem mk_pt_pt_lieson {O A : P} [PtNe O A] : A LiesOn (CIR O A) := rfl
 theorem mk_pt_pt_diam_fst_lieson {A B : P} [_h : PtNe A B] : A LiesOn (mk_pt_pt_diam A B) := by
   show dist (SEG A B).midpoint A = dist (SEG A B).midpoint B
   rw [dist_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist]
-  exact dist_target_eq_dist_source_of_midpt (seg := (SEG A B))
+  exact (SEG A B).dist_target_eq_dist_source_of_midpt
 
 theorem mk_pt_pt_diam_snd_lieson {A B : P} [_h : PtNe A B] : B LiesOn (mk_pt_pt_diam A B) := rfl
 

EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean

@@ -8,7 +8,7 @@ namespace EuclidGeom
 
 variable {P : Type _} [EuclideanPlane P]
 
-open DirLC CC
+open DirLC CC Angle
 
 namespace Circle
 
@@ -123,7 +123,7 @@ lemma tangents_perp₁ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_
   calc
     _ = (RAY p (pt_tangent_circle_pts h).left).toProj := rfl
     _ = (RAY (pt_tangent_circle_pts h).left p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt
-    _ = (RAY (pt_tangent_circle_pts h).left ω.center).toProj.perp := dvalue_eq_ang_rays_perp heq₁
+    _ = (RAY (pt_tangent_circle_pts h).left ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₁
     _ = (RAY ω.center (pt_tangent_circle_pts h).left).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt]
     _ = (DLIN ω.center (pt_tangent_circle_pts h).left).toProj.perp := rfl
 
@@ -139,7 +139,7 @@ lemma tangents_perp₂ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_
   calc
     _ = (RAY p (pt_tangent_circle_pts h).right).toProj := rfl
     _ = (RAY (pt_tangent_circle_pts h).right p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt
-    _ = (RAY (pt_tangent_circle_pts h).right ω.center).toProj.perp := dvalue_eq_ang_rays_perp heq₂
+    _ = (RAY (pt_tangent_circle_pts h).right ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₂
     _ = (RAY ω.center (pt_tangent_circle_pts h).right).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt]
     _ = (DLIN ω.center (pt_tangent_circle_pts h).right).toProj.perp := rfl
 

EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean

@@ -9,7 +9,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex
 noncomputable section
 namespace EuclidGeom
 
-open AngValue
+open AngValue Angle
 
 @[ext]
 structure Arc (P : Type _) [EuclideanPlane P] where
@@ -133,14 +133,11 @@ theorem cangle_of_complementary_arc_are_opposite (β : Arc P) : β.cangle.value
   apply neg_value_of_rev_ang
 
 theorem antipode_iff_colinear (A B : P) {ω : Circle P} [h : PtNe B A] (h₁ : A LiesOn ω) (h₂ : B LiesOn ω) : Arc.IsAntipode A B h₁ h₂ ↔ colinear ω.center A B := by
-  constructor
-  · intro hh
-    unfold Arc.IsAntipode Arc.cangle Arc.mk_pt_pt_circle Arc.angle_mk_pt_arc at hh
-    simp at hh
-    apply colinear_of_angle_eq_pi hh
-  intro hh
   haveI : PtNe A ω.center := Circle.pt_lieson_ne_center h₁
   haveI : PtNe B ω.center := Circle.pt_lieson_ne_center h₂
+  constructor
+  · exact colinear_of_angle_eq_pi
+  intro hh
   show ∠ A ω.center B = π
   have hl : B LiesOn LIN ω.center A := Line.pt_pt_maximal hh
   have heq₁ : VEC A ω.center = VEC ω.center B := by
@@ -160,7 +157,7 @@ theorem antipode_iff_colinear (A B : P) {ω : Circle P} [h : PtNe B A] (h₁ : A
     show VEC A ω.center = 2⁻¹ • (VEC A B)
     rw [heq₂]
     simp
-  apply liesint_segnd_value_eq_pi _ hli
+  exact value_eq_pi_of_lies_int_seg_nd hli
 
 theorem mk_pt_pt_diam_isantipode {A B : P} [h : PtNe A B] : Arc.IsAntipode A B (Circle.mk_pt_pt_diam_fst_lieson) (Circle.mk_pt_pt_diam_snd_lieson) := by
   have hc : colinear (SEG A B).midpoint A B := by

EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean

@@ -69,7 +69,7 @@ lemma dist_pt_line_ineq {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersect
     rw [abs_of_nonneg, abs_of_pos]
     exact this
     exact ω.rad_pos
-    exact length_nonneg
+    exact Seg.length_nonneg
   linarith
 
 def Inxpts {l : DirLine P} {ω : Circle P} (_h : DirLine.IsIntersected l ω) : DirLCInxpts P where
@@ -165,8 +165,7 @@ theorem inx_pts_same_iff_tangent {l : DirLine P} {ω : Circle P} (h : DirLine.Is
         apply dist_pt_line_ineq h
       apply (sq_eq_sq _ _).mp
       linarith
-      unfold dist_pt_line
-      exact length_nonneg
+      exact Seg.length_nonneg
       apply le_iff_lt_or_eq.mpr
       left; exact ω.rad_pos
     exfalso