diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean
index 001f0314..cf1e229c 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean
@@ -1,4 +1,5 @@
 import EuclideanGeometry.Foundation.Axiom.Basic.Angle.FromMathlib
+import Mathlib.Data.Int.Parity
 
 /-!
 # Theorems that should exist in Mathlib
@@ -7,6 +8,7 @@ Maybe we can create some PRs to mathlib in the future.
 -/
 
 open Real
+attribute [ext] Complex.ext
 
 /-!
 ## More theorems about trigonometric functions in Mathlib
diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
index b281f8c4..4463af3f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
@@ -184,7 +184,7 @@ lemma toComplex_inv (z : 𝕜) : ↑(z⁻¹) = (z : ℂ)⁻¹ := by ext <;> simp
 
 @[simp, norm_cast]
 lemma abs_toComplex (z : 𝕜) : Complex.abs (z : ℂ) = ‖z‖ := by
-  rw [← pow_left_inj (map_nonneg _ _) (norm_nonneg _) zero_lt_two,
+  rw [← pow_left_inj (map_nonneg _ _) (norm_nonneg _) two_ne_zero,
     Complex.sq_abs, Complex.normSq_apply, norm_sq_eq_def]
   rfl
 
@@ -400,7 +400,7 @@ 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; ring
+  smul_left v₁ v₂ z := by dsimp; simp; ring
 
 lemma real_inner_apply (v₁ v₂ : Vec) :
     ⟪v₁, v₂⟫_ℝ = v₁.fst * v₂.fst + v₁.snd * v₂.snd :=
@@ -694,7 +694,7 @@ lemma cdiv_eq_cdiv_iff_cdiv_eq_cdiv {v₁ v₂ v₃ v₄ : Vec} (hv₂ : v₂ 
 
 @[simp]
 lemma abs_inner (v₁ v₂ : Vec) : Complex.abs ⟪v₁, v₂⟫_ℂ = ‖v₁‖ * ‖v₂‖ := by
-  rw [← pow_left_inj (by simp) (by positivity) zero_lt_two]
+  rw [← pow_left_inj (by simp) (by positivity) two_ne_zero]
   rw [Complex.abs_apply, sq_sqrt (Complex.normSq_nonneg _)]
   dsimp [inner, det]
   rw [mul_pow, norm_sq, norm_sq]
@@ -1582,7 +1582,7 @@ theorem map_trans (f g : Dir ≃ Dir) {_ : Dir.NegCommute f} {_ : Dir.NegCommute
     Proj.map (f.trans g) = (Proj.map f).trans (Proj.map g) := by
   ext p
   induction p using Proj.ind
-  
+
   simp
 
 instance : Nonempty Proj := (nonempty_quotient_iff _).mpr <| inferInstanceAs (Nonempty Dir)
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
index 3edcd92f..f2831ebf 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
@@ -170,7 +170,7 @@ theorem CC_inscribe_point_centers_colinear {ω₁ : Circle P} {ω₂ : Circle P}
   apply colinear_of_vec_eq_smul_vec this
 
 
-theorem CC_included_pt_isint_second_circle {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h₁ : ω₁ IncludeIn ω₂) (h₂ : A LiesOn ω₁) : Circle.IsInt A ω₂ := by
+theorem CC_included_pt_isint_second_circle {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h₁ : ω₁ IncludeIn ω₂) (h₂ : A LiesOn ω₁) : A LiesInt ω₂ := by
   have : dist ω₂.center A < ω₂.radius := by
     calc
       _ ≤ dist ω₁.center ω₂.center + dist ω₁.center A := by apply dist_triangle_left
@@ -253,14 +253,12 @@ theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Int
   rw [← sub_smul]
   simp
   push_neg
-  constructor
-  · apply Real.sqrt_ne_zero'.mpr
-    have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by
-      apply sq_lt_sq.mpr
-      rw [abs_of_pos ω₁.rad_pos]
-      exact radical_axis_dist_lt_radius h
-    linarith
-  exact Complex.I_ne_zero
+  apply Real.sqrt_ne_zero'.mpr
+  have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by
+    apply sq_lt_sq.mpr
+    rw [abs_of_pos ω₁.rad_pos]
+    exact radical_axis_dist_lt_radius h
+  linarith
 
 theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : ((CC_Intersected_pts h).left LiesOn ω₁) ∧ ((CC_Intersected_pts h).left LiesOn ω₂) ∧ ((CC_Intersected_pts h).right LiesOn ω₁) ∧ ((CC_Intersected_pts h).right LiesOn ω₂) := by
   haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩