Fix errors

EuclideanGeometry/Example/SCHAUM/Problem1.1.lean

@@ -133,15 +133,15 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SE
     have h₅₁ : -∠ e.E e.C e.M  = -∠ e.A e.C e.B := by
       have inner_h₅₁ : ∠  e.E e.C e.M = ∠  e.A e.C e.B := by
         symm
-        apply eq_ang_val_of_lieson_lieson
+        apply Angle.value_eq_of_lies_on_ray_pt_pt
         · exact E_int_ray_CA
         · exact M_int_ray_CB
       simp only [inner_h₅₁]
     have h₅₂ : ∠ e.D e.B e.M = -∠ e.C e.B e.A := by
       rw [← neg_value_of_rev_ang]
       have inner_h₅₂ : ∠  e.D e.B e.M = ∠  e.A e.B e.C := by
         symm
-        apply eq_ang_val_of_lieson_lieson
+        apply Angle.value_eq_of_lies_on_ray_pt_pt
         · exact D_int_ray_BA
         · exact M_int_ray_BC
       simp only [inner_h₅₂]

EuclideanGeometry/Example/SCHAUM/Problem1.3.lean

@@ -110,14 +110,14 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠
       rw [← neg_value_of_rev_ang (e.A_ne_B) (e.C_ne_B)]
       have inner_h₂₁ : ∠  e.A e.B e.D (e.A_ne_B) (e.D_ne_B) = ∠  e.A e.B e.C (e.A_ne_B) (e.C_ne_B) := by
         symm
-        apply eq_ang_val_of_lieson_lieson
+        apply Angle.value_eq_of_lies_on_ray_pt_pt
         ·exact A_int_ray_BA
         .exact D_int_ray_BC
       simp only [inner_h₂₁]
     have h₂₂ : ∠ e.A e.C e.E (e.A_ne_C) (e.E_ne_C) = ∠ e.A e.C e.B (e.A_ne_C) (e.B_ne_C) := by
       have inner_h₂₂ : ∠  e.A e.C e.E (e.A_ne_C) (e.E_ne_C) = ∠  e.A e.C e.B (e.A_ne_C) (e.B_ne_C) := by
         symm
-        apply eq_ang_val_of_lieson_lieson
+        apply Angle.value_eq_of_lies_on_ray_pt_pt
         ·exact A_int_ray_CA
         ·exact E_int_ray_CB
       simp only [inner_h₂₂]

EuclideanGeometry/Example/SCHAUM/Problem1.7.lean

@@ -182,12 +182,12 @@ Therefore, $DX = EY$.
     ∠ e.D e.B e.X D_ne_B X_ne_B
     -- $\angle DBX = \angle CBA$ because $D$ lies on ray $BC$ and $X$ lies on ray $BA$,
     _= ∠ e.C e.B e.A C_ne_B A_ne_B := by
-      symm; exact eq_ang_val_of_lieson_lieson C_ne_B A_ne_B D_ne_B X_ne_B D_int_ray_BC X_int_ray_BA
+      symm; exact Angle.value_eq_of_lies_on_ray_pt_pt C_ne_B A_ne_B D_ne_B X_ne_B D_int_ray_BC X_int_ray_BA
     -- $\angle CBA = - \angle BCA$,
     _= - ∠ e.B e.C e.A C_ne_B.symm A_ne_C := angle_CBA_eq_neg_angle_BCA
     -- $\angle BCA = - \angle ECY$ because $e$ lies on ray $CB$ and $Y$ lies on ray $CA$.
     _= - ∠ e.E e.C e.Y E_ne_C Y_ne_C := by
-      simp only [eq_ang_val_of_lieson_lieson C_ne_B.symm A_ne_C E_ne_C Y_ne_C E_int_ray_CB Y_int_ray_CA]
+      simp only [Angle.value_eq_of_lies_on_ray_pt_pt C_ne_B.symm A_ne_C E_ne_C Y_ne_C E_int_ray_CB Y_int_ray_CA]
   -- $\triangle XBD \cong_a \triangle YEC$ (by AAS)
   have triangle_XBD_acongr_triangle_YCE : (TRI_nd e.X e.B e.D not_colinear_XBD) ≅ₐ (TRI_nd e.Y e.C e.E not_colinear_YCE) := by
     apply acongr_of_AAS_variant

EuclideanGeometry/Example/SCHAUM/Problem1.8.lean

@@ -89,7 +89,7 @@ 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 eq_ang_val_of_lieson_lieson (e.B_ne_C.symm) e.A_ne_B D_ne_B e.A_ne_B
+      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
       · 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$.
@@ -98,7 +98,7 @@ Therefore, $BD = CE$.
       exact Triangle.isoceles_of_regular (▵ e.A e.B e.C) e.regular_ABC
     -- 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 eq_ang_val_of_lieson_lieson A_ne_C e.B_ne_C E_ne_C e.B_ne_C
+      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 Ray.snd_pt_lies_int_mk_pt_pt e.C e.B e.B_ne_C
   -- We have $BD = CE$.

EuclideanGeometry/Example/ShanZun/Ex1f.lean

@@ -88,7 +88,7 @@ theorem Shan_Problem_2_11 : (SEG C E).length = (SEG D E).length := by
         exact (length_eq_length_add_length a_lies_on_be).symm
   -- $\angle EBF = \angle ABC$
   have ang₁ : ∠ F B E f_ne_b e_ne_b = ∠ C B A c_ne_a a_ne_b := by
-    apply eq_ang_value_of_lies_int_lies_int
+    apply value_eq_of_lies_on_ray_pt_pt
     constructor
     exact SegND.lies_on_toRay_of_lies_on c_lies_on_bf
     exact b_ne_c.symm

EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean

@@ -1,4 +1,5 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
+import Mathlib.Data.Int.Parity
 
 /-!
 # APIs about Angle from Mathlib
@@ -8,6 +9,8 @@ We use `AngValue` as an alias of `Real.Angle`.
 
 noncomputable section
 
+attribute [ext] Complex.ext
+
 open Real
 
 section Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean

@@ -400,7 +400,10 @@ instance innerProductSpace' : InnerProductSpace ℝ Vec where
   norm_sq_eq_inner v := by simp [norm_sq]
   conj_symm v₁ v₂ := by simp [Complex.conj_ofReal, mul_comm]
   add_left v₁ v₂ v₃ := by dsimp; ring
-  smul_left v₁ v₂ z := by dsimp; simp; ring
+  smul_left v₁ v₂ z := by
+    dsimp
+    simp only [zero_mul, sub_zero, add_zero, conj_trivial]
+    ring
 
 lemma real_inner_apply (v₁ v₂ : Vec) :
     ⟪v₁, v₂⟫_ℝ = v₁.fst * v₂.fst + v₁.snd * v₂.snd :=
@@ -1256,6 +1259,9 @@ lemma neg_vsub_left (d₁ d₂ : Dir) : -d₁ -ᵥ d₂ = d₁ -ᵥ d₂ + ∠[
 lemma neg_vsub_right (d₁ d₂ : Dir) : d₁ -ᵥ -d₂ = d₁ -ᵥ d₂ + ∠[π] := by
   rw [← pi_vadd, vsub_vadd_eq_vsub_sub, sub_eq_add_neg, AngValue.neg_coe_pi]
 
+lemma eq_neg_of_vsub_eq_pi (d₁ d₂ : Dir) : d₁ = - d₂ ↔ d₁ -ᵥ d₂ = ∠[π] :=
+  ((pi_vadd d₂).symm.congr_right).trans (eq_vadd_iff_vsub_eq d₁ ∠[π] d₂)
+
 protected abbrev normalize {M : Type*} [AddCommGroup M] [Module ℝ M]
     {F : Type*} [LinearMapClass F ℝ Vec M]
     (f : F) :
@@ -1464,6 +1470,20 @@ theorem Dir.toProj_eq_toProj_iff_unitVecND {d₁ d₂ : Dir} :
   conv_lhs => rw [← d₁.unitVecND_toDir, ← d₂.unitVecND_toDir]
   rw [VecND.toProj_eq_toProj_iff']
 
+theorem Dir.toProj_eq_toProj_iff_vsub_not_isND {d₁ d₂ : Dir} : d₁.toProj = d₂.toProj ↔ ¬ (d₁ -ᵥ d₂).IsND :=
+  toProj_eq_toProj_iff.trans <|
+    (or_congr vsub_eq_zero_iff_eq.symm (eq_neg_of_vsub_eq_pi d₁ d₂)).trans AngValue.not_isND_iff.symm
+
+theorem Dir.toProj_ne_toProj_iff_vsub_isND {d₁ d₂ : Dir} : d₁.toProj ≠ d₂.toProj ↔ (d₁ -ᵥ d₂).IsND :=
+  toProj_eq_toProj_iff_vsub_not_isND.not_left
+
+theorem Dir.toProj_ne_toProj_iff_neg_vsub_isND {d₁ d₂ : Dir} : d₁.toProj ≠ d₂.toProj ↔ (d₂ -ᵥ d₁).IsND := by
+  apply toProj_ne_toProj_iff_vsub_isND.trans
+  rw [← neg_vsub_eq_vsub_rev d₂ d₁, AngValue.neg_isND_iff_isND]
+
+theorem Dir.toProj_eq_toProj_iff_neg_vsub_not_isND {d₁ d₂ : Dir} : d₁.toProj = d₂.toProj ↔ ¬ (d₂ -ᵥ d₁).IsND :=
+  toProj_ne_toProj_iff_neg_vsub_isND.not_right
+
 @[simp]
 lemma VecND.neg_toProj (v : VecND) : (-v).toProj = v.toProj := by
   rw [toProj_eq_toProj_iff']

EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean

@@ -249,9 +249,9 @@ def CC_Intersected_pts {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersec
 theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (CC_Intersected_pts h).left ≠ (CC_Intersected_pts h).right := by
   apply (ne_iff_vec_ne_zero _ _).mpr
   unfold Vec.mkPtPt CC_Intersected_pts
-  simp
-  rw [← sub_smul]
-  simp
+  simp only [neg_mul, vadd_vsub_vadd_cancel_right, ne_eq, ← sub_smul]
+  simp only [add_sub_add_right_eq_sub, sub_neg_eq_add, smul_eq_zero, add_self_eq_zero, mul_eq_zero,
+    Complex.ofReal_eq_zero, Complex.I_ne_zero, or_false, VecND.ne_zero]
   push_neg
   apply Real.sqrt_ne_zero'.mpr
   have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by

EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean

@@ -202,12 +202,10 @@ theorem cangle_eq_two_times_inscribed_angle {p : P} {β : Arc P} (h₁ : p LiesO
     have : (ANG β.target β.circle.center p).end_ray = (ANG p β.circle.center β.source).start_ray := rfl
     have hhs : (Angle.sum_adj this).value = ∠ β.target β.circle.center β.source := rfl
     rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang]
-    rfl
   have hsum₂ : ∠ β.source p β.circle.center + ∠ β.circle.center p β.target = ∠ β.source p β.target := by
     have : (ANG β.source p β.circle.center).end_ray = (ANG β.circle.center p β.target).start_ray := rfl
     have hhs : (Angle.sum_adj this).value = ∠ β.source p β.target := rfl
     rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang]
-    rfl
   have eq₃ : ∠ β.target β.circle.center β.source + 2 • (∠ β.source p β.target) = 0 := by
     calc
       _ = ∠ β.target β.circle.center p + ∠ p β.circle.center β.source + 2 • (∠ β.source p β.circle.center + ∠ β.circle.center p β.target) := by rw [hsum₁, hsum₂]