diff --git a/EuclideanGeometry/Check.lean b/EuclideanGeometry/Check.lean
index 2550a369a..f4eac78fa 100644
--- a/EuclideanGeometry/Check.lean
+++ b/EuclideanGeometry/Check.lean
@@ -9,13 +9,13 @@ Here exhibits unfamiliar codes for learning.
 -/
 
 section HEq
-def T {A A' B : Type _} (e : A = A') (f : A → B) : A' → B := by
+def T {A A' B : Type*} (e : A = A') (f : A → B) : A' → B := by
   rw [← e]
   exact f
-theorem heq {A A' B : Type _} (e : A = A') (f : A → B) : HEq f (T e f) := by
+theorem heq {A A' B : Type*} (e : A = A') (f : A → B) : HEq f (T e f) := by
   subst e
   rfl
-theorem heq' {g : Type _ → Type _ } {A A' B : Type _} (e : g A = g A') (f : g A → B) : HEq f (T e f) := by
+theorem heq' {g : Type* → Type* } {A A' B : Type*} (e : g A = g A') (f : g A → B) : HEq f (T e f) := by
   exact heq e f
 
 #check heq
@@ -24,13 +24,13 @@ theorem heq' {g : Type _ → Type _ } {A A' B : Type _} (e : g A = g A') (f : g
 #check Eq.ndrec
 #check Eq.mpr
 
-theorem heq_funext' {c₁ c₂ d : Type _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), (HEq s t) → f₁ s = f₂ t) : HEq f₁ f₂ := by
+theorem heq_funext' {c₁ c₂ d : Type*} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), (HEq s t) → f₁ s = f₂ t) : HEq f₁ f₂ := by
   exact Function.hfunext e (fun s t g => (heq_of_eq (h s t g)))
 
-theorem heq_funext_prop {c₁ c₂ : Prop} {d : Type _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := by
+theorem heq_funext_prop {c₁ c₂ : Prop} {d : Type*} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := by
   exact Function.hfunext e (fun s t _ => (heq_of_eq (h s t)))
 
-theorem heq_funext {c₁ c₂ d: Sort _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _)))
+theorem heq_funext {c₁ c₂ d: Sort*} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _)))
 
 
 end HEq
@@ -49,7 +49,7 @@ namespace EuclidGeom
 /- check instance VAdd-/
 section VAddCheck
 
-variable (P : Type _) [EuclidGeom.EuclideanPlane P] (l : Ray P)
+variable (P : Type*) [EuclidGeom.EuclideanPlane P] (l : Ray P)
 #check l.toDir.toVec
 #check @AddAction.toVAdd _ _ _ (@AddTorsor.toAddAction _ _ _ (@NormedAddTorsor.toAddTorsor _ P _ _ _))
 
@@ -64,7 +64,7 @@ end raymk
 /- check angle notation-/
 section anglecheck
 
-variable {P : Type _} [h : EuclideanPlane P] (O : P) (A : P) (B : P)
+variable {P : Type*} [h : EuclideanPlane P] (O : P) (A : P) (B : P)
 #check ANG A O B
 
 variable (l : GDirSeg P)
@@ -72,7 +72,7 @@ variable (l : GDirSeg P)
 
 end anglecheck
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 theorem test_is_on (A : P) (seg : Seg P) : (p LiesOn seg) = (Seg.IsOn p seg) := rfl
 
 
diff --git a/EuclideanGeometry/Example/AOPS/Chap2.lean b/EuclideanGeometry/Example/AOPS/Chap2.lean
index f9ae9e6ac..5adfb333c 100644
--- a/EuclideanGeometry/Example/AOPS/Chap2.lean
+++ b/EuclideanGeometry/Example/AOPS/Chap2.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace AOPS_Problem_2_14
 
diff --git a/EuclideanGeometry/Example/AOPS/Chap3.lean b/EuclideanGeometry/Example/AOPS/Chap3.lean
index 9f909bedf..f3bf01d85 100644
--- a/EuclideanGeometry/Example/AOPS/Chap3.lean
+++ b/EuclideanGeometry/Example/AOPS/Chap3.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Exercise_3_4_4
 
diff --git a/EuclideanGeometry/Example/AOPS/Chap3a.lean b/EuclideanGeometry/Example/AOPS/Chap3a.lean
index 96569e41e..51c158940 100644
--- a/EuclideanGeometry/Example/AOPS/Chap3a.lean
+++ b/EuclideanGeometry/Example/AOPS/Chap3a.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace AOPS_Problem_3_21
 /- Let $\triangle ABC$ be a regular triangle, and let $P$, $Q$, $R$ be three points in the interior of $\triangle ABC$ such that
diff --git a/EuclideanGeometry/Example/AOPS/Chap5.lean b/EuclideanGeometry/Example/AOPS/Chap5.lean
index 759421704..68ddc24ce 100644
--- a/EuclideanGeometry/Example/AOPS/Chap5.lean
+++ b/EuclideanGeometry/Example/AOPS/Chap5.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace AOPS_Problem_5_7
 /- Let $\triangle ABC$ be a triangle, and let $D$, $E$ be two points in the interior of $AB$ and $AC$ respectively such that $DE\parallel BC$ . $X$ lies inside $AB$ and $Y$ lies on the ray $XE$ so that $AY\parallel XC$
diff --git a/EuclideanGeometry/Example/AOPS/Chap5a.lean b/EuclideanGeometry/Example/AOPS/Chap5a.lean
index 66c256dfd..fe7cb28b0 100644
--- a/EuclideanGeometry/Example/AOPS/Chap5a.lean
+++ b/EuclideanGeometry/Example/AOPS/Chap5a.lean
@@ -6,14 +6,14 @@ noncomputable section
 
 namespace EuclidGeom
 namespace AOPS
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace AOPS_Problem_5_7
 /- Let $\triangle ABC$ be a triangle, and let $D$, $E$ be two points in the interior of $AB$ and $AC$ respectively such that $DE\parallel BC$ . $X$ lies inside $AB$ and $Y$ lies on the ray $XE$ so that $AY\parallel XC$
 
 Prove that $\frac{EY}{EX}=\frac{AD}{DB}$ -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be a nontrivial triangle
   A : Plane
   B : Plane
@@ -55,7 +55,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   hY₂ : (LIN A Y Y_ne_A)∥(LIN X C X_ne_C.symm)
 
 --$\frac{EY}{EX}=\frac{AD}{DB}$
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) :  (SEG e.E e.Y).length/(SEG e.E e.X).length = (SEG e.A e.D).length/(SEG e.D e.B).length := sorry
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) :  (SEG e.E e.Y).length/(SEG e.E e.X).length = (SEG e.A e.D).length/(SEG e.D e.B).length := sorry
 
 end AOPS_Problem_5_7
 
@@ -81,7 +81,7 @@ namespace AOPS_Exercise_5_3_2
 Prove that $IJ\prar BC$-/
 --It is simpler to use vectors but I think we should avoid vectors.
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be a nontrivial triangle
   A : Plane
   B : Plane
@@ -122,7 +122,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   -- Claim : $J \ne I$
   J_ne_I : J ≠ I := sorry
   --$IJ\parallel BC$
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : LIN e.I e.J e.J_ne_I ∥ LIN e.B e.C e.C_ne_B := sorry
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : LIN e.I e.J e.J_ne_I ∥ LIN e.B e.C e.C_ne_B := sorry
 
 end AOPS_Exercise_5_3_2
 end AOPS
diff --git a/EuclideanGeometry/Example/ArefWernick/Chap1.lean b/EuclideanGeometry/Example/ArefWernick/Chap1.lean
index 94f7d8396..cd20a7a9c 100644
--- a/EuclideanGeometry/Example/ArefWernick/Chap1.lean
+++ b/EuclideanGeometry/Example/ArefWernick/Chap1.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Aref_Wernick_Exercise_1_1
 /- Two triangles are congruent if two sides and the enclosed median in one triangle are respectively equal to two sides and the enclosed median of the other.
diff --git a/EuclideanGeometry/Example/ArefWernick/Chap1a.lean b/EuclideanGeometry/Example/ArefWernick/Chap1a.lean
index 60b9b2763..aac66e7f1 100644
--- a/EuclideanGeometry/Example/ArefWernick/Chap1a.lean
+++ b/EuclideanGeometry/Example/ArefWernick/Chap1a.lean
@@ -8,7 +8,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Aref_Wernick_Exercise_1_1
 /- Two triangles are congruent if two sides and the enclosed median in one triangle are respectively equal to two sides and the enclosed median of the other.
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean
index d903e31a2..8eb419d05 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean
+++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean
@@ -12,7 +12,7 @@ $C, D$ lies in segment $BF$, $AB \parallel DE$, $AB = DF$, $BC = DE$.
 
 Prove that $∠ BAC = ∠ EFD$.
 -/
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
   -- $C, D$ lies in segment $BF$, they lies on the same line $l$.
   B : Plane
   C : Plane
@@ -34,26 +34,26 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   -- $BC = DE$
   h₂ : (SEG B C).length = (SEG D E).length
 attribute [instance] Setting1.B_ne_F
-lemma hnd₁ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.B e.A e.C := by
+lemma hnd₁ {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.B e.A e.C := by
   apply Collinear.perm₂₁₃.mt
   exact e.ABC_nd
-lemma hnd₂ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.D e.F e.E := by
+lemma hnd₂ {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.D e.F e.E := by
   apply Collinear.perm₃₁₂.mt
   exact e.EDF_nd
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.B := ⟨(ne_of_not_collinear hnd₁).2.2⟩
-instance D_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.E := ⟨(ne_of_not_collinear hnd₂).2.1⟩
-instance A_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.C := ⟨(ne_of_not_collinear hnd₁).1.symm⟩
-instance E_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.E e.F := ⟨(ne_of_not_collinear hnd₂).1⟩
-instance D_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.F := ⟨(ne_of_not_collinear hnd₂).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.B e.C := ⟨(ne_of_not_collinear hnd₁).2.1⟩
-instance D_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.B := ⟨(ne_vertex_of_lies_int_seg_nd e.D_int).1⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.B := ⟨(ne_of_not_collinear hnd₁).2.2⟩
+instance D_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.E := ⟨(ne_of_not_collinear hnd₂).2.1⟩
+instance A_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.C := ⟨(ne_of_not_collinear hnd₁).1.symm⟩
+instance E_ne_F {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.E e.F := ⟨(ne_of_not_collinear hnd₂).1⟩
+instance D_ne_F {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.F := ⟨(ne_of_not_collinear hnd₂).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.B e.C := ⟨(ne_of_not_collinear hnd₁).2.1⟩
+instance D_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.B := ⟨(ne_vertex_of_lies_int_seg_nd e.D_int).1⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
   -- $AB ∥ DE$
   hpr : (SEG_nd B A) ∥ (SEG_nd D E)
 
 -- Prove that $∠ BAC = ∠ EFD$.
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.A e.C = ∠ e.E e.F e.D := by
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.A e.C = ∠ e.E e.F e.D := by
   /-
   $\angle ABC$ and $\angle EDF$ are corresponding angles,thus equal.
   In $\triangle BAC \congr_a \triangle DFE$.
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean
index ed7feca46..c91a74ea7 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean
+++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean
@@ -11,7 +11,7 @@ namespace Problem_2
 Given $AB = DC$, $DB = AC$, $B,C$ is on the same side of line $AD$.
 Prove that $∠B = ∠ C$.
 -/
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
   -- $AB = DC$, $DB = AC$.
   A : Plane
   B : Plane
@@ -26,12 +26,12 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   -- $B,C$ is on the same side of line $AD$.
   B_side : IsOnRightSide B (SEG_nd A D D_ne_A)
   C_side : IsOnRightSide C (SEG_nd A D D_ne_A)
-lemma a_ne_b {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.B := (ne_of_not_collinear e.hnd₁).1
-lemma a_ne_c {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.C := (ne_of_not_collinear e.hnd₂).2.2.symm
-lemma b_ne_d {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.D :=  (ne_of_not_collinear e.hnd₁).2.2
-lemma c_ne_d {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.C ≠ e.D :=(ne_of_not_collinear e.hnd₂).1.symm
+lemma a_ne_b {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.B := (ne_of_not_collinear e.hnd₁).1
+lemma a_ne_c {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.C := (ne_of_not_collinear e.hnd₂).2.2.symm
+lemma b_ne_d {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.D :=  (ne_of_not_collinear e.hnd₁).2.2
+lemma c_ne_d {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.C ≠ e.D :=(ne_of_not_collinear e.hnd₂).1.symm
 -- Prove that $∠B = ∠ C$.
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}:  ∠ e.A e.B e.D a_ne_b b_ne_d.symm = -∠ e.D e.C e.A c_ne_d.symm a_ne_c := by
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}:  ∠ e.A e.B e.D a_ne_b b_ne_d.symm = -∠ e.D e.C e.A c_ne_d.symm a_ne_c := by
   -- Use SSS to prove that $\triangle DBA \congr \triangle ACD$ or $\triangle DBA \congr_a \triangle ACD$.
   have h : (TRI_nd e.D e.B e.A e.hnd₁) ≅ₐ (TRI_nd e.A e.C e.D e.hnd₂) := by
     apply TriangleND.acongr_of_SSS_of_ne_orientation
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean
index f0d4570b9..586948fe6 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean
+++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean
@@ -12,7 +12,7 @@ namespace Problem_3
 In (convex) quadrilateral $A B D C$,$AB = AC$, $BD = CD$.
 Prove that $\angle A B D = -\angle A C D$
 -/
-structure Setting  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting  (Plane : Type*) [EuclideanPlane Plane] where
   --In (convex) quadrilateral $A B D C$,$AB = AC$, $BD = CD$.
   A : Plane
   B : Plane
@@ -27,7 +27,7 @@ structure Setting  (Plane : Type _) [EuclideanPlane Plane] where
   --$A \ne C$ and $D \ne B$ for $\angle A C D$
   A_ne_C : A ≠ C := (Quadrilateral_cvx.nd₁₄ (QDR_cvx A B D C cvx_ABDC)).symm
   D_ne_C : D ≠ C := (Quadrilateral_cvx.nd₃₄ (QDR_cvx A B D C cvx_ABDC)).symm
-theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠  e.A e.B e.D (e.A_ne_B) (e.D_ne_B) = - ∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C):= by
+theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠  e.A e.B e.D (e.A_ne_B) (e.D_ne_B) = - ∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C):= by
   /-
   Because $AB = AC$ ,we have $\angle A B C = -\angle A C B$.
   Because $DB = DC$ ,we have $\angle D B C = -\angle D C B$
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean
index 702112665..cfaf1bc01 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean
+++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean
@@ -12,7 +12,7 @@ $A,D$ are on the opposite side of line $BC$,which satisfies $BD \parallel CA$, $
 $E$ liesint $BC$ and $BE = AC$
 Prove that $\angle B D E = -\angle C B A $.
 -/
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
@@ -22,11 +22,11 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   hnd₂ : ¬ Collinear B C D
   --$A,D$ are on the opposite side of line $BC$,which satisfies $BD \para CA$(lemma needed), $BD = BC$
   BD_eq_BC : (SEG B D).length = (SEG B C).length
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd₁).2.2.symm⟩
-instance D_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.D e.B := ⟨(ne_of_not_collinear e.hnd₂).2.1.symm⟩
-instance A_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.C := ⟨(ne_of_not_collinear e.hnd₁).1⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd₁).2.2.symm⟩
+instance D_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.D e.B := ⟨(ne_of_not_collinear e.hnd₂).2.1.symm⟩
+instance A_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.C := ⟨(ne_of_not_collinear e.hnd₁).1⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
   --$BD \para CA$
   BD_para_CA : (SEG_nd B D) ∥ (SEG_nd C A)
   --$A,D$ are on the opposite side of line $BC$
@@ -36,12 +36,12 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
   E : Plane
   E_int : E LiesInt (SEG_nd B C)
   E_position : (SEG B E).length = (SEG A C).length
-lemma hnd₃ {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane}: ¬ Collinear e.B e.E e.D := by sorry
-instance E_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.E e.D := ⟨(ne_of_not_collinear hnd₃).1.symm⟩
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd₁).2.1.symm⟩
-instance B_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.E := ⟨(ne_of_not_collinear hnd₃).2.2.symm⟩
+lemma hnd₃ {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane}: ¬ Collinear e.B e.E e.D := by sorry
+instance E_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.E e.D := ⟨(ne_of_not_collinear hnd₃).1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd₁).2.1.symm⟩
+instance B_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.E := ⟨(ne_of_not_collinear hnd₃).2.2.symm⟩
 --Prove that $\angle B D E = -\angle C B A $.
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.D e.E = -∠ e.C e.B e.A := by
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.D e.E = -∠ e.C e.B e.A := by
   /-
   Because $BD \parallel CA$,($A,D$ are on the opposite side of line $BC$),
   $\angle D B E $ and $\angle A C B$ are Alternate Interior Angle, thus equal.
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean
index 9dccc8911..65f9615c3 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean
+++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Wuwowuji_Problem_1_6
 /-
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean
index 79b270528..8b4496c6f 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean
+++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Wuwowuji_Problem_1_7
 /-
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean
index 71f28a7da..f21ecb84f 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean
+++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace Wuwowuji_Problem_1_8
 /-
diff --git a/EuclideanGeometry/Example/ExerciseXT8.lean b/EuclideanGeometry/Example/ExerciseXT8.lean
index bf515faa0..42c5b5e9d 100644
--- a/EuclideanGeometry/Example/ExerciseXT8.lean
+++ b/EuclideanGeometry/Example/ExerciseXT8.lean
@@ -5,7 +5,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 
 
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean
index 0c6cafd32..f535b322e 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Schaum
 
@@ -26,7 +26,7 @@ variable {E_ray_position : (SEG A E).length = (SEG A D).length}
 --Let $M$ be the midpoint of $BC$.
 variable {M : P} {median_M_position : M = (SEG B C).midpoint}
 -/
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   --Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
   A : Plane
   B : Plane
@@ -46,7 +46,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   midpoint_M : M = (SEG B C).midpoint
 
 --Prove that $DM = EM$.
-theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.M).length = (SEG e.E e.M).length := by
+theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.M).length = (SEG e.E e.M).length := by
   /-In the isoceles triangle $ABC$, we have $AB = AC$.
     Meanwhile $AE = AD$
     We have $BD = AB - AD = AC - AE = CE$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean
index bec0d6141..332421670 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace SCHAUM_Problem_1_10
 /-
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean
index 935d4c0f6..39f7e787c 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean
@@ -4,14 +4,14 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace SCHAUM_Problem_1_11
 /-
 If $ABCD$ is a parallelogram and $EFCD$ is a parallelogram, then $ABFE$ is a parallelogram.
 -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- $ABCD$ is a parallelogram.
   A : Plane
   B : Plane
@@ -23,7 +23,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   F : Plane
   EFCD_IsPRG : (QDR E F C D) IsPRG
 -- Prove that $ABFE$ is a parallelogram.
-theorem result (Plane : Type _) [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.F e.E) IsPRG := by
+theorem result (Plane : Type*) [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.F e.E) IsPRG := by
   /-
   Because $ABCD$ is a parallelogram, $\overarrow{AB} = \overarrow{DC}$.
   Because $EFCD$ is a parallelogram, $\overarrow{EF} = \overarrow{DC}$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean
index b5bd0fee3..089039358 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace SCHAUM_Problem_1_12
 /-
@@ -15,7 +15,7 @@ Prove that $ABCD$ is a parallelogram.
 -/
 
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $ABCD$ be a convex quadrilateral.
   A : Plane
   B : Plane
@@ -33,7 +33,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   BC_eq_DA : (SEG B C).length = (SEG D A).length
 
 -- Prove that $ABCD$ is a parallelogram.
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.C e.D) IsPRG_nd := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.C e.D) IsPRG_nd := by
   sorry
 
 
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean
index 2c41adc0f..d82919252 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace SCHAUM_Problem_1_13
 /-
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean
index baa4828cf..7f4717656 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace SCHAUM_Problem_1_14
 /-
@@ -15,7 +15,7 @@ Let $ABCD$ be a parallelogram. Let $P$ and $Q$ be points on the segments $AB$ an
 Prove that $PM = QN$ and $PM \parallel QN$.
 -/
 
-structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $ABCD$ be a parallelogram.
   A : Plane
   B : Plane
@@ -37,23 +37,23 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
   perp_foot_N : N = perp_foot Q (LIN B D D_ne_B)
 
 -- Because $P$ is not on line $BD$, $M$, the foot of the perpendicular from $P$ to the diagonal $BD$ doesn't equal to $P$.
-lemma not_P_lieson_BD {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.P LiesOn (LIN e.B e.D e.D_ne_B) := sorry
-lemma not_Q_lieson_BD {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.Q LiesOn (LIN e.B e.D e.D_ne_B) := sorry
-lemma M_ne_P {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.M ≠ e.P := by
+lemma not_P_lieson_BD {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.P LiesOn (LIN e.B e.D e.D_ne_B) := sorry
+lemma not_Q_lieson_BD {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.Q LiesOn (LIN e.B e.D e.D_ne_B) := sorry
+lemma M_ne_P {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.M ≠ e.P := by
   simp only [e.perp_foot_M]
   exact (perp_foot_eq_self_iff_lies_on e.P (LIN e.B e.D e.D_ne_B)).not.mpr (not_P_lieson_BD)
-lemma N_ne_Q {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.N ≠ e.Q := by
+lemma N_ne_Q {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.N ≠ e.Q := by
   simp only [e.perp_foot_N]
   exact (perp_foot_eq_self_iff_lies_on e.Q (LIN e.B e.D e.D_ne_B)).not.mpr (not_Q_lieson_BD)
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends (Setting1 Plane) where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends (Setting1 Plane) where
   not_P_lieson_BD : ¬ P LiesOn (LIN B D D_ne_B) := not_P_lieson_BD
   not_Q_lieson_BD : ¬ Q LiesOn (LIN B D D_ne_B) := not_Q_lieson_BD
   M_ne_P : M ≠ P := M_ne_P
   N_ne_Q : N ≠ Q := N_ne_Q
 
 -- Prove that $PM = QN$.
-theorem result1 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (SEG e.P e.M).length = (SEG e.Q e.N).length := by
+theorem result1 {Plane : Type*} [EuclideanPlane Plane] (e : Setting2 Plane) : (SEG e.P e.M).length = (SEG e.Q e.N).length := by
   /- Because quadrilateral $ABCD$ is a parallelogram, $AB \parallel CD$, thus the alternate interior angle $\angle ABD = \angle CDB$,
   therefore $\angle PBM = \angle ABD = \angle CDB = \angle QDN$. Also, $\angle BMP = \pm\frac{\pi}{2}$, $\angle DNQ = \pm\frac{\pi}{2}$
   because $M$ and $N$ are the foot of perpendicular from $P$, $Q$ to $BD$, respectively.
@@ -77,7 +77,7 @@ theorem result1 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (
   exact MBP_congr_NCQ.edge₂
 
 -- Prove that $PM \parallel QN$.
-theorem result2 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (LIN e.P e.M e.M_ne_P) ∥ (LIN e.Q e.N e.N_ne_Q) := by
+theorem result2 {Plane : Type*} [EuclideanPlane Plane] (e : Setting2 Plane) : (LIN e.P e.M e.M_ne_P) ∥ (LIN e.Q e.N e.N_ne_Q) := by
   -- We have $PM \perp BD$ because $M$ is the perpendicular foot from $P$ to $BD$.
   have PM_perp_BD : LIN e.P e.M e.M_ne_P ⟂ LIN e.B e.D e.D_ne_B := by
     simp only [e.perp_foot_M]
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean
index d7dfb41ac..62a7b09b1 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean
@@ -14,7 +14,7 @@ Let $Q$ be the foot of perpendicular from $E$ to $BC$.
 Prove that $DP = EQ$.
 -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
   A : Plane
   B : Plane
@@ -41,7 +41,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   hQ : Q = perp_foot E (LIN B C B_ne_C.symm)
 
 /- # Another Style of Setting-/
-structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
   A : Plane
   B : Plane
@@ -58,11 +58,11 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
   AE_eq_AD : (SEG A E).length = (SEG A D).length
 
 -- Claim: $B \ne C$.
-lemma B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.C := by
+lemma B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.C := by
     -- This is because vertices $B, C$ of a nondegenerate triangle are distinct.
   exact (ne_of_not_collinear e.not_collinear_ABC).1.symm
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
   B_ne_C : B ≠ C := B_ne_C
   -- Let $P$ be the foot of perpendicular from $D$ to $BC$.
   P : Plane
@@ -72,7 +72,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
   hQ : Q = perp_foot E (LIN B C B_ne_C.symm)
 
 -- Prove that $DP = EQ$.
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.P).length = (SEG e.E e.Q).length := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.P).length = (SEG e.E e.Q).length := by
 /-
   In the isoceles triangle $ABC$, we have $AB = AC$.
   Thus we have $BD = AB - AD = AC - AE = CE$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean
index e5d1e2847..89f4c2eb9 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace Problem1_2_
 /-Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.Let $D$ be a point on $AB$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean
index 9c6b6b83b..8aedf2099 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean
@@ -30,7 +30,7 @@ lemma b_ne_c : B ≠ C := (ne_of_not_collinear hnd).1.symm
 lemma c_ne_b : C ≠ B := (ne_of_not_collinear hnd).1
 --Prove that $∠ D A B = ∠ C A E$.
 -/
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   --Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
   A : Plane
   B : Plane
@@ -53,13 +53,13 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   C_ne_B : C ≠ B := (ne_of_not_collinear not_collinear_ABC).1
 --Points not equal for angles ∠ A B D and ∠ A C E
 namespace Setting
-lemma D_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.A := sorry
-lemma E_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.A := sorry
-lemma D_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.B := e.D_Int_BC.2.1
-lemma E_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.C := e.E_Int_BC.2.2
+lemma D_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.A := sorry
+lemma E_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.A := sorry
+lemma D_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.B := e.D_Int_BC.2.1
+lemma E_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.C := e.E_Int_BC.2.2
 end Setting
 --Prove that $∠ D A B = ∠ C A E$.
-theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.D e.A e.B (e.D_ne_A) (e.B_ne_A)= ∠ e.C e.A e.E (e.C_ne_A) (e.E_ne_A) := by
+theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.D e.A e.B (e.D_ne_A) (e.B_ne_A)= ∠ e.C e.A e.E (e.C_ne_A) (e.E_ne_A) := by
   /-In the isoceles triangle $ABC$ we have $AB = AC$.
     Beacause $BD = CE$ we have $DB = EC$.
     In the isoceles triangle $A B C$, we have $\angle A B C = -\angle A C B$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean
index 36557861a..8aa92dfa1 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {Plane : Type _} [EuclideanPlane Plane]
+variable {Plane : Type*} [EuclideanPlane Plane]
 
 namespace Problem1_4_
 /-Let $B$ $D$ be points on segment $AF$, such that $AD = BF$. Let $C$ be a point.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean
index f4a16f22f..a06987c58 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean
@@ -18,7 +18,7 @@ such that $AP = CR$ and $AS = CQ$.
 
 Prove that $PQRS$ is a parallelogram.
 -/
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
 --Let $ABCD$ be a parallelogram
   A : Plane
   B : Plane
@@ -42,7 +42,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
 --such that $AS = CQ$
   AS_eq_CQ : (SEG A S).length = (SEG C Q).length
 --Prove that $PQRS$ is a parallelogram
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.P e.Q e.R e.S).IsParallelogram_nd := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.P e.Q e.R e.S).IsParallelogram_nd := by
 /-
 In parallelogram $ABCD$, we have $AB, DC$ are of the same direction.
 Since $P$ lies on $AB$, we have $AP, AB$ are of the same direction.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean
index ae808e8c1..4960c43ba 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean
@@ -13,7 +13,7 @@ Let $ABCD$ be a parallelogram, and let $P$, $Q$ be points on the segments $AB$ a
 
 Prove that $PB = QD$.
 -/
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
 --Let $ABCD$ be a parallelogram
   A : Plane
   B : Plane
@@ -29,7 +29,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
 --such that $AP = CQ$
   AP_eq_CQ : (SEG A P).length = (SEG C Q).length
 --Prove that $PB = QD$
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.P e.B).length = (SEG e.Q e.D).length := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.P e.B).length = (SEG e.Q e.D).length := by
 /-
 In the parallelogram $ABCD$ we have $AB = CD$.
 Therefore, $PB = AB - AP = CD - CQ = QD$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean
index cf69a53ac..22402e406 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean
@@ -18,7 +18,7 @@ Let $D$ and $E$ be points on the segment $BC$ such that $BD = CE$.
 Prove that the height of $D$ to $AB$ is the same as the height of $E$ to $AC$.
 -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
 --Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$
   A : Plane
   B : Plane
@@ -49,7 +49,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   he : Y = perp_foot E (LIN A C C_ne_A)
 --Prove that $DX = EY$.
 
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.X).length = (SEG e.E e.Y).length := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.X).length = (SEG e.E e.Y).length := by
 /-
 In isoceles triangle $ABC$, we have $\angle ABC$ and $\angle ACB$ are acute.
 From $D$ lies on $BC$ and $\angle ABC$ is acute, we know that $X$ lies on ray $BA$, so $\angle XBD$ is the same as $\angle ABC$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean
index 9d238f9fb..1a6913e3b 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean
@@ -16,7 +16,7 @@ such that $CD = AE$.
 
 Prove that $AD = BE$
 -/
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
 --Let $\triangle ABC$ be a regular triangle.
   A : Plane
   B : Plane
@@ -44,7 +44,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
 --such that $CD = AE$
   CD_eq_AE : ((SEG C D).length = (SEG A E).length)
 --Prove that $AD = BE$
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ((SEG e.A e.D).length = (SEG e.B e.E).length):= by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ((SEG e.A e.D).length = (SEG e.B e.E).length):= by
 /-
 In regular triangle $ABC$, $\angle ABC = \angle BCA$.
 Since $D$ lies on the extension of $BC$, we know that $\angle ABD$ is the same as $\angle ABC$.
diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean
index 94021f158..5595e27c9 100644
--- a/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean
+++ b/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean
@@ -17,7 +17,7 @@ Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$. Let $E$ be a poi
 Prove that $\angle EAX = \angle XAC$.
 -/
 
-structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where
 -- Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$.
   A : Plane
   B : Plane
@@ -52,7 +52,7 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
   X : Plane
   X_int_la : X LiesInt l_a
 -- Claim $E \ne A$
-lemma E_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.E ≠ e.A := by
+lemma E_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.E ≠ e.A := by
   -- This is because $E$ lies on the extension of $BA$ and $A$ is the source of that ray.
   -- We have $E$ is not equal to the source of the extension of $BA$, since $E$ lies on the extension of $BA$.
   have h1 : e.E ≠ e.BA_ext.source := e.E_int_ext.2
@@ -60,19 +60,19 @@ lemma E_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.E
   have h2 : e.A = e.BA_ext.source := by simp only [e.hlba]; rfl
   simp only [h2]; exact h1
 -- Claim : $X \ne A$
-lemma X_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.X ≠ e.A := by
+lemma X_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.X ≠ e.A := by
   -- This is because $X$ lies on $l_a$ and $A$ is the source of that ray.
   -- We have $X$ is not equal to the source $l_a$, since $X$ lies on the extension of $BA$.
   have h1 : e.X ≠ e.l_a.source := e.X_int_la.2
   -- We have $A$ is the source of $l_a$ by definition.
   have h2 : e.A = e.l_a.source := by simp only [e.hla]
   simp only [h2]; exact h1
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
   E_ne_A : E ≠ A := E_ne_A
   X_ne_A : X ≠ A := X_ne_A
 
 -- Prove that $\angle EAX = \angle XAC$
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : ∠ e.E e.A e.X e.E_ne_A e.X_ne_A = ∠ e.X e.A e.C e.X_ne_A e.C_ne_A := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting2 Plane) : ∠ e.E e.A e.X e.E_ne_A e.X_ne_A = ∠ e.X e.A e.C e.X_ne_A e.C_ne_A := by
 /-
 As $AX$ has the same direction as $BC$ and that $E$ is on the extension of $BA$, we know that $\angle EAX = \angle ABC$.
 In isoceles triangle $ABC$, $\angle ABC = - \angle ACB$.
diff --git a/EuclideanGeometry/Example/ShanZun-Ex1a.lean b/EuclideanGeometry/Example/ShanZun-Ex1a.lean
index 892148a39..cca59132e 100644
--- a/EuclideanGeometry/Example/ShanZun-Ex1a.lean
+++ b/EuclideanGeometry/Example/ShanZun-Ex1a.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_1_3
 /- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$. Let $D$ be a point in the extension of $AB$ such that $BD = AB$. Let $E$ be the midpoint of $AB$.
diff --git a/EuclideanGeometry/Example/ShanZun-Ex1b.lean b/EuclideanGeometry/Example/ShanZun-Ex1b.lean
index 2ced19d98..0c68efb0f 100644
--- a/EuclideanGeometry/Example/ShanZun-Ex1b.lean
+++ b/EuclideanGeometry/Example/ShanZun-Ex1b.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_1_5
 /- In $\triangle ABC$, let $AD$ be the median.  Let $E$ be a point on $AD$ such that $BE = AC$. The line $BE$ intersects $AC$ at $F$.
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1.lean b/EuclideanGeometry/Example/ShanZun/Ex1.lean
index 1accc03ed..d51004779 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_1_1
 /- In $\triangle ABC$, let $AD$ be the height and $AE$ be the angle bisector of $\triangle ABC$.
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1a.lean b/EuclideanGeometry/Example/ShanZun/Ex1a.lean
index 18510ab58..20216c431 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1a.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1a.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_1_3
 /- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1b.lean b/EuclideanGeometry/Example/ShanZun/Ex1b.lean
index f6e7f0326..cb6600227 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1b.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1b.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_1_5
 /- In $\triangle ABC$, let $AD$ be the median.  Let $E$ be a point on $AD$ such that $BE = AC$. The line $BE$ intersects $AC$ at $F$.
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1c'.lean b/EuclideanGeometry/Example/ShanZun/Ex1c'.lean
index a972254f3..39371ac41 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1c'.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1c'.lean
@@ -13,7 +13,7 @@ namespace Shan_Problem_1_7
 
 Prove that $CD = AB / 2$. -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be a nontrivial triangle in which $\angle ACB= \pi/2$.
   A : Plane
   B : Plane
@@ -35,7 +35,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   D : Plane
   hD : D = (SEG A B).midpoint
 
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.C e.D).length = (SEG e.A e.B).length/2 := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.C e.D).length = (SEG e.A e.B).length/2 := by
   have D_ne_A: e.D ≠ e.A := by
     rw[e.hD]
     apply (SegND.midpt_lies_int (seg_nd := SEG_nd e.A e.B (e.B_ne_A))).2.1
@@ -179,7 +179,7 @@ namespace Shan_Problem_1_8
 
 Prove that $FG \perp DE$. -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be a nontrivial triangle in which $\angle ACB= \pi/2$.
   A : Plane
   B : Plane
@@ -212,7 +212,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   E_ne_D : E ≠ D := sorry
 
 -- Theorem : $FG \perp DE$
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) :(SEG_nd e.F e.G e.G_ne_F) ⟂ (SEG_nd e.D e.E e.E_ne_D) := sorry
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) :(SEG_nd e.F e.G e.G_ne_F) ⟂ (SEG_nd e.D e.E e.E_ne_D) := sorry
 
 end Shan_Problem_1_8
 
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1c.lean b/EuclideanGeometry/Example/ShanZun/Ex1c.lean
index 5676b29a2..c27d2f6d0 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1c.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1c.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_1_7
 /- In $\triangle ABC$, $\angle ACB = \pi /2$. Let $D$ be the midpoint of $AB$.
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1d.lean b/EuclideanGeometry/Example/ShanZun/Ex1d.lean
index 3785e5ee3..111f1600d 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1d.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1d.lean
@@ -6,7 +6,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_1_9
 /- In $\triangle ABC$, assume that $\angle CBA = 2\cdot \angle ACB$. Let $AD$ be the height and $AE$ the median.
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1e'.lean b/EuclideanGeometry/Example/ShanZun/Ex1e'.lean
index 3524919c0..488207e28 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1e'.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1e'.lean
@@ -10,7 +10,7 @@ namespace Shan_Problem_2_13
 the perpendicular line passing through $D$ of the bisector of $\angle BAC$ intersects $AB,AC$ at $E,F$ respectively.
 Prove that $BE=CF=\frac{1}{2}|AB-AC|$.  -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be a nontrivial triangle
   A : Plane
   B : Plane
@@ -43,7 +43,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
 
 
 -- Theorem : $BE=CF=\frac{1}{2}|AB-AC|$
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.B e.E).length=|((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 ∧ (SEG e.C e.F).length = |((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 := sorry
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.B e.E).length=|((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 ∧ (SEG e.C e.F).length = |((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 := sorry
 
 end Shan_Problem_2_13
 
@@ -52,7 +52,7 @@ namespace Shan_Problem_2_18
  $CE$ be the bisector of $\angle ACB$ and $CF$ be the median.
 Prove that $E$ liesInt $DF$ -/
 
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $\triangle ABC$ be a nontrivial triangle
   A : Plane
   B : Plane
@@ -87,11 +87,11 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   --Claim : $F\ne C$
   F_ne_C : F ≠ C := sorry
 
-theorem result1 {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : e.E LiesInt (SEG e.D e.F) := sorry
+theorem result1 {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : e.E LiesInt (SEG e.D e.F) := sorry
 
 
 -- Theorem : $CE$ is the bisector of $\angle FCD$
-theorem result2 {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.F e.C e.E e.F_ne_C e.E_ne_C = ∠ e.E e.C e.D e.E_ne_C e.D_ne_C := sorry
+theorem result2 {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.F e.C e.E e.F_ne_C e.E_ne_C = ∠ e.E e.C e.D e.E_ne_C e.D_ne_C := sorry
 
 
 end Shan_Problem_2_18
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1e.lean b/EuclideanGeometry/Example/ShanZun/Ex1e.lean
index d3af9003c..0cb852358 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1e.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1e.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_2_13
 /- In $\triangle ABC$. Let $D$ be the midpoint of segment $BC$,
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1f'.lean b/EuclideanGeometry/Example/ShanZun/Ex1f'.lean
index f5a9e9be5..519fc7fee 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1f'.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1f'.lean
@@ -5,7 +5,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_2_11
 /- Let $\triangle ABC$ be a regular triangle,
@@ -13,7 +13,7 @@ Let $E$ be a point on the extension of $BA$ and $D$ a point on the extension of
 such that $AE = BD$, connect $CE,DE$
 Prove that $CE = DE$ -/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- Let $\triangle ABC$ be a regular triangle
   A : Plane
   B : Plane
@@ -21,11 +21,11 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   hnd : ¬ Collinear A B C
   hreg : (▵ A B C).IsRegular
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
 -- Let $E$ be a point on the extension of $BA$ and $D$ a point on the extension of $BC$
   D : Plane
   E : Plane
@@ -35,7 +35,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
   h : (SEG A E).length = (SEG B D).length
 
 -- Theorem : $CE = DE$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.C e.E).length = (SEG e.D e.E).length := by
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.C e.E).length = (SEG e.D e.E).length := by
 /-
   Extend $BD$ to $F$ such that $DF = BC$.
   Then $BF = BD + DF = AE + AB = BE$, and $\angle FBE = 60^{\circ}$  or $-60^{\circ}$.
@@ -176,18 +176,18 @@ $F,G$ are points of trisection of $AC$,
 line $DF$ and $EG$ intersect at $H$
 Prove that quadrilateral $ABCH$ is parallelogram -/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have triangle $\triangle ABC$
   A : Plane
   B : Plane
   C : Plane
   hnd : ¬ Collinear A B C
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
 -- $D$ is midpoint of $BA$, $E$ is midpoint of $BC$
   D : Plane
   E : Plane
@@ -200,16 +200,16 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
   hg : G LiesInt (SEG_nd A C)
   htri : (SEG A F).length = (SEG F G).length ∧ (SEG F G).length = (SEG G C).length
 -- Claim: $F \ne D$ and $G \ne E$
-instance F_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.F e.D := ⟨sorry⟩
-instance G_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.G e.E := ⟨sorry⟩
+instance F_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.F e.D := ⟨sorry⟩
+instance G_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.G e.E := ⟨sorry⟩
 
-structure Setting3 (Plane : Type _) [EuclideanPlane Plane] extends Setting2 Plane where
+structure Setting3 (Plane : Type*) [EuclideanPlane Plane] extends Setting2 Plane where
 -- $H$ is the intersection of line $DF$ and $EG$
   H : Plane
   hh : is_inx H (LIN D F) (LIN E G)
 
 -- Theorem : quadrilateral $ABCH$ is parallelogram
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : QDR e.A e.B e.C e.H IsPRG := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : QDR e.A e.B e.C e.H IsPRG := sorry
 
 end Shan_Problem_2_22
 
@@ -220,18 +220,18 @@ $F,G$ are points lies on line $BC$,
 such that $FB = CG$ and $AF \parallel BE$ ,
 Prove that $AG \parallel DC$-/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have triangle $\triangle ABC$
   A : Plane
   B : Plane
   C : Plane
   hnd : ¬ Collinear A B C
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
 -- $D,E$ are points in $AB,AC$ respectively
   D : Plane
   E : Plane
@@ -245,18 +245,18 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
 -- We have $FB = CG$
   hedge : (SEG F B).length = (SEG C G).length
 -- Claim : $F \ne A$ and $E \ne B$
-instance F_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.F e.A := ⟨sorry⟩
-instance E_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.E e.B := ⟨sorry⟩
+instance F_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.F e.A := ⟨sorry⟩
+instance E_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.E e.B := ⟨sorry⟩
 
-structure Setting3 (Plane : Type _) [EuclideanPlane Plane] extends Setting2 Plane where
+structure Setting3 (Plane : Type*) [EuclideanPlane Plane] extends Setting2 Plane where
 -- We have $AF \parallel BE$
   hpara : (SEG_nd A F) ∥ (SEG_nd B E)
 -- Claim: $G \ne A$ and $D \ne C$
-instance G_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.G e.A := ⟨sorry⟩
-instance D_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.D e.C := ⟨sorry⟩
+instance G_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.G e.A := ⟨sorry⟩
+instance D_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.D e.C := ⟨sorry⟩
 
 -- Theorem : $AG \parallel DC$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.A e.G) ∥ (SEG_nd e.C e.D) := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.A e.G) ∥ (SEG_nd e.C e.D) := sorry
 
 end Shan_Problem_2_36
 
@@ -267,7 +267,7 @@ $BE, CF$ are heights,
 such that $AE = 2 EC$
 Prove that $AF = 3 FB$ -/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have acute triangle $\triangle ABC$
   A : Plane
   B : Plane
@@ -275,11 +275,11 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   hnd : ¬ Collinear A B C
   hacute : TriangleND.IsAcute (TRI_nd A B C hnd)
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
 -- $D,E$ are points in $AB,AC$ respectively
   E : Plane
   F : Plane
@@ -289,7 +289,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
   h : (SEG A E).length = 2 * (SEG E C).length
 
 -- Theorem : $AF = 3 FB$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.F).length = 3 * (SEG e.F e.B).length := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.F).length = 3 * (SEG e.F e.B).length := sorry
 
 end Shan_Problem_2_37
 
@@ -298,37 +298,37 @@ namespace Shan_Problem_2_38
 let the angle bisectors of $\angle ADB$ and $\angle ADC$ intersect $AB$ and $AC$ at $E,F$,
 Prove that $EF \parallel BC$-/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have triangle $\triangle ABC$
   A : Plane
   B : Plane
   C : Plane
   hnd : ¬ Collinear A B C
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
 -- $D$ is the midpoint of $BC$
   D : Plane
   hd : D = (SEG B C).midpoint
 -- Claim: $A \ne D$ and $B \ne D$ and $C \ne D$
-instance A_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.D := ⟨sorry⟩
-instance B_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.D := ⟨sorry⟩
-instance C_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.C e.D := ⟨sorry⟩
+instance A_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.D := ⟨sorry⟩
+instance B_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.D := ⟨sorry⟩
+instance C_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.C e.D := ⟨sorry⟩
 
-structure Setting3 (Plane : Type _) [EuclideanPlane Plane] extends Setting2 Plane where
+structure Setting3 (Plane : Type*) [EuclideanPlane Plane] extends Setting2 Plane where
 -- let the angle bisectors of $\angle ADB$ and $\angle ADC$ intersect $AB$ and $AC$ at $E,F$
   E : Plane
   F : Plane
   he : is_inx E (ANG A D B).AngBis (SEG A B)
   hf : is_inx F (ANG A D C).AngBis (SEG A C)
 -- Claim: $F \ne E$
-instance F_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.F e.E := ⟨sorry⟩
+instance F_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.F e.E := ⟨sorry⟩
 
 -- Theorem : $EF \parallel BC$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.E e.F) ∥ (SEG_nd e.B e.C) := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.E e.F) ∥ (SEG_nd e.B e.C) := sorry
 
 end Shan_Problem_2_38
 
@@ -338,7 +338,7 @@ $E$ lies on $AC$ such that $AE = 2 CE$,
 $CD,BE$ intersects at $O$
 Prove that $OE = \frac{1}{4} BE$-/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have triangle $\triangle ABC$
   A : Plane
   B : Plane
@@ -355,7 +355,7 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   ho : is_inx O (SEG C D) (SEG B E)
 
 -- Theorem : $OE = \frac{1}{4} BE$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.O e.E).length = (1 / 4) * (SEG e.B e.E).length := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.O e.E).length = (1 / 4) * (SEG e.B e.E).length := sorry
 
 end Shan_Problem_2_42
 
@@ -364,18 +364,18 @@ namespace Shan_Problem_2_43
 The parallel line to $AC$ of $E,F$ intersect $BC$ at $G,H$ respectively,
 Prove that $EG + FH = AC$-/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have triangle $\triangle ABC$
   A : Plane
   B : Plane
   C : Plane
   hnd : ¬ Collinear A B C
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
 -- $E,F$ lies on $AB$ such that $AE = FB$
   E : Plane
   F : Plane
@@ -395,7 +395,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
   hh : is_inx H l₂ (SEG B C)
 
 -- Theorem : $EG + FH = AC$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.E e.G).length + (SEG e.F e.H).length = (SEG e.A e.C).length := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.E e.G).length + (SEG e.F e.H).length = (SEG e.A e.C).length := sorry
 
 end Shan_Problem_2_43
 
@@ -404,7 +404,7 @@ namespace Shan_Problem_2_44
 $A₁,B₁,C₁$ are points on line $l₁$ such that $AA₁ \parallel BB₁ \parallel CC₁$.
 Prove that $BB₁ = \frac{n}{m+n} AA₁ + \frac{m}{m+n} CC₁$-/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have line $l$ and points $A,B,C$ lies on $l
   l : Line Plane
   A : Plane
@@ -434,7 +434,7 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   hpara₂ : (SEG_nd B B₁) ∥ (SEG_nd C C₁)
 
 -- Theorem : $BB₁ = \frac{n}{m+n} AA₁ + \frac{m}{m+n} CC₁$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.B e.B₁).length = (e.n / (e.m+e.n)) * (SEG e.A e.A₁).length + (e.m/(e.m+e.n)) * (SEG e.C e.C₁).length := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.B e.B₁).length = (e.n / (e.m+e.n)) * (SEG e.A e.A₁).length + (e.m/(e.m+e.n)) * (SEG e.C e.C₁).length := sorry
 
 end Shan_Problem_2_44
 
@@ -442,7 +442,7 @@ namespace Shan_Problem_2_48
 /- $ABCD$ are convex quadrilateral, $AC$ and $BD$ intersect at $E$,
 Prove that area of $\triangle ABD$ : area of $\triangle CBD = AE : CE$  -/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- We have convex quadrilateral $ABCD$
   A : Plane
   B : Plane
@@ -455,7 +455,7 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
 
 
 -- Theorem : area of $\triangle ABC :$ area of $\triangle DBC = AE : DE$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : Triangle.area (▵ e.A e.B e.D) / Triangle.area (▵ e.C e.B e.D) = (SEG e.A e.E).length / (SEG e.D e.E).length := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : Triangle.area (▵ e.A e.B e.D) / Triangle.area (▵ e.C e.B e.D) = (SEG e.A e.E).length / (SEG e.D e.E).length := sorry
 
 end Shan_Problem_2_48
 
@@ -464,18 +464,18 @@ namespace Shan_Problem_2_52
 the angle bisector of $\angle ABC$ intersect $AD$ and $AC$ at $M,N$ respectively,
 Prove that $AB^2 - AN^2 = BM \times BN$-/
 
-structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
 -- Let triangle $\triangle ABC$
   A : Plane
   B : Plane
   C : Plane
   hnd : ¬ Collinear A B C
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
 
-structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
+structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where
 --$\triangle ABC$ is a right triangle with $\angle BAC = 90^{circ}$
   hright : ∠ B A C = ↑ (π / 2)
 -- $AD$ is the height of $\triangle ABC$
@@ -490,6 +490,6 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
   hn : is_inx N (SEG A C) l
 
 -- Theorem : $AB^2 - AN^2 = BM \times BN$
-theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.B).length * (SEG e.A e.B).length - (SEG e.A e.N).length * (SEG e.A e.N).length = (SEG e.B e.M).length * (SEG e.B e.N).length := sorry
+theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.B).length * (SEG e.A e.B).length - (SEG e.A e.N).length * (SEG e.A e.N).length = (SEG e.B e.M).length * (SEG e.B e.N).length := sorry
 
 end Shan_Problem_2_52
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1f.lean b/EuclideanGeometry/Example/ShanZun/Ex1f.lean
index 905be2b9f..0b6842b86 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1f.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1f.lean
@@ -5,7 +5,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_2_11
 /- Let $\triangle ABC$ be a regular triangle,
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1h'.lean b/EuclideanGeometry/Example/ShanZun/Ex1h'.lean
index c8da9eab3..ebb6547d3 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1h'.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1h'.lean
@@ -9,7 +9,7 @@ namespace Shan_Problem_2_21
 
 /- In a parallelogram ABCD, E and F lies on the segment AC, and $AE=FC$
 Prove that $DE\parallel BF$ -/
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $ ABCD$ be a nontrivial parallelogram
   A : Plane
   B : Plane
@@ -52,7 +52,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
 
 
 -- $DE \parallel BF $
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (LIN e.D e.E e.E_ne_D) ∥ (LIN e.B e.F e.F_ne_B):= by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (LIN e.D e.E e.E_ne_D) ∥ (LIN e.B e.F e.F_ne_B):= by
 
   -- $\ang BAE=\ang DCF$
   have ang_BAE_eq_ang_DCF : ∠ e.B e.A e.E e.B_ne_A e.E_ne_A = ∠ e.D e.C e.F e.D_ne_C e.F_ne_C := sorry
@@ -67,7 +67,7 @@ end Shan_Problem_2_21
 namespace Shan_Problem_2_23
 /- In a parallelogram ABCD, E is the midpoint of the segment BC, and F is the midpoint of the segment AD. Let G, H be the intersection of AC with BF and DE respectively.
 Prove that $AG=GH=HC$ -/
-structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+structure Setting (Plane : Type*) [EuclideanPlane Plane] where
   -- Let $ ABCD$ be a nontrivial parallelogram
   A : Plane
   B : Plane
@@ -105,7 +105,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   hH : is_inx H (LIN A C C_ne_A) (LIN D E E_ne_D)
 
 --The pair of points (G,H) divides the segement AC into three segments with the same length.
-theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.A e.G).length=(SEG e.G e.H).length ∧ (SEG e.A e.G).length=(SEG e.H e.C).length := by
+theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.A e.G).length=(SEG e.G e.H).length ∧ (SEG e.A e.G).length=(SEG e.H e.C).length := by
   -- $▵AFG$ is nontrivial
   have AFG_nd : ¬ Collinear e.A e.F e.G := sorry
   -- $▵CBG$ is nontrivial
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1h.lean b/EuclideanGeometry/Example/ShanZun/Ex1h.lean
index b1f7bb12b..d2194a96e 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1h.lean
+++ b/EuclideanGeometry/Example/ShanZun/Ex1h.lean
@@ -4,7 +4,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Shan_Problem_2_21
 /- In a parallelelogram ABCD, E and F lies on the segment AC, and $AE=FC$
diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
index 586a909a1..4d6edc07b 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
@@ -29,9 +29,9 @@ noncomputable section
 namespace EuclidGeom
 
 /- Define Euclidean plane as normed vector space over ℝ of dimension 2 -/
-class EuclideanPlane (P : Type _) extends MetricSpace P, NormedAddTorsor Vec P
+class EuclideanPlane (P : Type*) extends MetricSpace P, NormedAddTorsor Vec P
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 def Vec.mkPtPt (A B : P) : Vec := (B -ᵥ A)
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean
index b3e64077d..f7978916a 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean
@@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Plane
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 /- point reflection -/
 def pt_flip (A O : P) : P := (VEC A O) +ᵥ O
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
index c265c216b..51108663f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
@@ -9,12 +9,12 @@ namespace EuclidGeom
 
 /- Class of Circles-/
 @[ext]
-structure Circle (P : Type _) [EuclideanPlane P] where
+structure Circle (P : Type*) [EuclideanPlane P] where
   center : P
   radius : ℝ
   rad_pos : 0 < radius
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Circle
 
@@ -277,7 +277,7 @@ section arc
 variable (ω : Circle P)
 
 @[ext]
-structure Arc (P : Type _) [EuclideanPlane P] (ω : Circle P) where
+structure Arc (P : Type*) [EuclideanPlane P] (ω : Circle P) where
   source : P
   target : P
   ison : (source LiesOn ω) ∧ (target LiesOn ω)
@@ -375,7 +375,7 @@ end arc
 section chord
 
 @[ext]
-structure Chord (P : Type _) [EuclideanPlane P] (ω : Circle P) where
+structure Chord (P : Type*) [EuclideanPlane P] (ω : Circle P) where
   toSegND : SegND P
   ison : (toSegND.source LiesOn ω) ∧ (toSegND.target LiesOn ω)
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
index ae7d018c2..785d18ac7 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
@@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence_trash
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section position
 
@@ -251,7 +251,7 @@ lemma intersected_centers_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω
 end CC
 
 @[ext]
-structure CCInxpts (P : Type _) [EuclideanPlane P] where
+structure CCInxpts (P : Type*) [EuclideanPlane P] where
   left : P
   right : P
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean
index 528118a57..eeb5dc58a 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean
@@ -6,7 +6,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.InscribedAngle
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 open DirLC CC Angle
 
@@ -50,7 +50,7 @@ section tangent
 namespace Circle
 
 @[ext]
-structure Tangents (P : Type _) [EuclideanPlane P] where
+structure Tangents (P : Type*) [EuclideanPlane P] where
   left : P
   right : P
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean
index 3580d66e7..5f5f02bba 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean
@@ -5,7 +5,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle_trash
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 open AngValue Angle
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean
index 9309acaf6..39353dde0 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean
@@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.Basic
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section DirLC
 
@@ -66,7 +66,7 @@ theorem pt_liesint_intersect {l : DirLine P} {ω : Circle P} {A : P} (h₁ : A L
 end DirLC
 
 @[ext]
-structure DirLCInxpts (P : Type _) [EuclideanPlane P] where
+structure DirLCInxpts (P : Type*) [EuclideanPlane P] where
   front : P
   back : P
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean b/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean
index 8ff5d9dcd..348d9f2d3 100644
--- a/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean
@@ -4,6 +4,6 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray
 
 namespace EuclidGeom
 
-variable {P: Type _} [EuclideanPlane P] (o : P)
+variable {P: Type*} [EuclideanPlane P] (o : P)
 
 end EuclidGeom
\ No newline at end of file
diff --git a/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean b/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean
index 6b90a3fe2..14b8c570b 100644
--- a/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean
@@ -7,7 +7,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P: Type _} [EuclideanPlane P] (v : Vec)
+variable {P: Type*} [EuclideanPlane P] (v : Vec)
 
 -- We fix the amount of translation to be v
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean
index 873d60ac3..16498448f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean
@@ -44,7 +44,7 @@ namespace EuclidGeom
 class LinFig (α : Type*) (P : outParam <| Type*) [outParam <| EuclideanPlane P] extends Fig α P where
   collinear' : ∀ {A B C : P} {F : α}, A LiesOn F → B LiesOn F → C LiesOn F → Collinear A B C
 
-class ProjObj (β : Type _) where
+class ProjObj (β : Type*) where
   toProj : β → Proj
 
 -- the information here is abundant, choose toProj' + a field carrier_to_proj_eq_to_proj is also enough. Or even ∃ A B ∈ carrier, A ≠ B is enough. toProj' can be defined later. However, we choose to write this way in order to avoid `∃` and use as many rfl as possible.
@@ -54,7 +54,7 @@ class ProjFig (α : Type*) (P : outParam <| Type*) [outParam <| EuclideanPlane P
   carrier_subset_toLine {F} : carrier F ⊆ (toLine F).carrier
   toLine_toProj_eq_toProj {F} : (toLine F).toProj = toProj' F
 
-class DirObj (β : Type _) extends ProjObj β where
+class DirObj (β : Type*) extends ProjObj β where
   toDir : β → Dir
   toDir_toProj_eq_toProj : ∀ {G : β}, (toDir G).toProj = toProj G
 
@@ -69,7 +69,7 @@ class DirFig (α : Type*) (P : outParam <| Type*) [outParam <| EuclideanPlane P]
   toDirLine_rev_eq_to_rev_toDirLine {F} : ((toDirLine F).reverse = toDirLine (reverse F))
 
 section fig_to_obj
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 instance {α} [ProjFig α P] : ProjObj α where
   toProj := ProjFig.toProj'
@@ -86,7 +86,7 @@ export DirFig (toDir' toDirLine toDir_toProj_eq_toProj toDirLine_toLine_eq_toLin
 export DirObj (toDir)
 
 section instances
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 -- Fun Fact: Vec is none of these. Id is LinFig.
 
 instance : DirObj VecND where
@@ -167,7 +167,7 @@ section theorems
 
 open Line DirLine
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem carrier_toProj_eq_toProj {α} {A B : P} [ProjFig α P] {F : α} [_h : PtNe B A] (ha : A LiesOn F) (hb : B LiesOn F) : (SEG_nd A B).toProj = toProj' F :=
   (toProj_eq_seg_nd_toProj_of_lies_on (carrier_subset_toLine ha) (carrier_subset_toLine hb)).trans toLine_toProj_eq_toProj
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean
index 5b9927a26..a5d6d0307 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean
@@ -8,7 +8,7 @@ namespace EuclidGeom
 
 open Classical
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section Collinear
 
@@ -214,7 +214,7 @@ Note that we do not need all reverse, extension line,... here. instead we should
 end compatibility
 
 /-- There exists three points $A$, $B$, $C$ on the plane such that they are not collinear. -/
-theorem nontriv_of_plane {H : Type _} [h : EuclideanPlane H] : ∃ A B C : H, ¬(Collinear A B C) := by
+theorem nontriv_of_plane {H : Type*} [h : EuclideanPlane H] : ∃ A B C : H, ¬(Collinear A B C) := by
   rcases h.nonempty with ⟨A⟩
   let B := (⟨1, 0⟩ : Vec) +ᵥ A
   let C := (⟨0, 1⟩ : Vec) +ᵥ A
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean
index acea84c26..d34a6120a 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean
@@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Parallel
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean
index bd9375677..0275cff38 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean
@@ -6,7 +6,7 @@ namespace EuclidGeom
 
 section setoid
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 -- `Future change plan` Change this to "structure" instead of "and".
 /-- We say that rays $r$ and $r'$ \emph{induce the same directed line} if, (1) they have the same direction, and (2) the source of $r'$ lies on $r$ or the reverse range of $r$.-/
@@ -128,12 +128,12 @@ theorem same_dir_line_le_same_extn_line : same_dir_line.setoid (P := P) ≤ same
 end setoid
 
 /-- A \emph{directed line} is the equivalence class of rays with the same directed lines. -/
-def DirLine (P : Type _) [EuclideanPlane P] := Quotient (@same_dir_line.setoid P _)
+def DirLine (P : Type*) [EuclideanPlane P] := Quotient (@same_dir_line.setoid P _)
 
 /-- A \emph{line} is the equivalence class of rays with the same exetnsion lines. -/
-def Line (P : Type _) [EuclideanPlane P] := Quotient (@same_extn_line.setoid P _)
+def Line (P : Type*) [EuclideanPlane P] := Quotient (@same_extn_line.setoid P _)
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section make
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean
index 946d6c376..46bbffcb1 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean
@@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem pt_flip_collinear {A B O : P} (h : B = pt_flip A O) : Collinear A O B := by
   apply Collinear.perm₁₃₂
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean
index b6532902c..eb632a219 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean
@@ -20,7 +20,7 @@ namespace EuclidGeom
 
 open Line
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 /-
 /-- A linear object is one of the following five types: a nondegenerate vector, a direction, a ray, a nondegenerate segment, or a line.
 In the following, we define natural ways to view a nondegenerate vector, a direction, a ray, a nondegenerate segment or a line, as a linear object.
@@ -525,13 +525,10 @@ theorem inx_eq_of_same_extn_line {a₁ b₁ a₂ b₂ : Ray P} (g₁ : same_extn
     (inx_lies_on_fst_extn_line a₂ b₂ h₂) ha1 (inx_lies_on_snd_extn_line a₂ b₂ h₂) hb1
   exact h₂ (congrArg Line.toProj heq)
 
--- This theorem deals only with `HEq`
-theorem heq_funext {c₁ c₂ d: Sort _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _)))
-
 theorem heq_of_inx_of_extn_line (a₁ b₁ a₂ b₂ : Ray P) (h₁ : same_extn_line a₁ a₂) (h₂ : same_extn_line b₁ b₂) : HEq (fun h => inx_of_extn_line a₁ b₁ h) (fun h => inx_of_extn_line a₂ b₂ h) := by
   have e : (Ray.toProj a₁ ≠ Ray.toProj b₁) = (Ray.toProj a₂ ≠ Ray.toProj b₂) := by
     rw [h₁.1, h₂.1]
-  exact @heq_funext (Ray.toProj a₁ ≠ Ray.toProj b₁) (Ray.toProj a₂ ≠ Ray.toProj b₂) P e (fun h => inx_of_extn_line a₁ b₁ h) (fun h => inx_of_extn_line a₂ b₂ h) (inx_eq_of_same_extn_line h₁ h₂)
+  exact Function.hfunext e fun _ _ _ ↦ heq_of_eq <| inx_eq_of_same_extn_line h₁ h₂ _ _
 
 /-- Given two unparallel lines, this function returns the intersection point of these two lines. -/
 def Line.inx (l₁ l₂ : Line P) (h : ¬ l₁ ∥ l₂) : P := @Quotient.hrecOn₂ (Ray P) (Ray P) same_extn_line.setoid same_extn_line.setoid (fun l l' => (Line.toProj l ≠ Line.toProj l') → P) l₁ l₂ inx_of_extn_line heq_of_inx_of_extn_line h
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
index aa5c8f6d1..ef5da3795 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean
@@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Parallel
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Parallel
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
index f488dea9b..a85328fc9 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
@@ -5,7 +5,7 @@ namespace EuclidGeom
 
 open Line
 
-variable {P : Type _} [EuclideanPlane P] {α β γ : Type*} [ProjObj α] [ProjObj β] [ProjObj γ]
+variable {P : Type*} [EuclideanPlane P] {α β γ : Type*} [ProjObj α] [ProjObj β] [ProjObj γ]
   {l₁ : α} {l₂ : β} {l₃ : γ}
 
 /-- This defines two projective objects to be perpendicular, i.e. their associated projective directions are perpendicular. -/
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean
index 763d87c16..9576df469 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean
@@ -6,6 +6,6 @@ namespace EuclidGeom
 
 open Line
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean
index 88ee7b7f0..de14085cc 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean
@@ -5,7 +5,7 @@ namespace EuclidGeom
 
 open Classical
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section ratio
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean
index 4301cbca9..80d3ab015 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean
@@ -54,7 +54,7 @@ section definition
 
 /-- A \emph{ray} consists of a pair of a point $P$ and a direction; it is the ray that starts at the point and extends in the given direction. -/
 @[ext]
-structure Ray (P : Type _) [EuclideanPlane P] where
+structure Ray (P : Type*) [EuclideanPlane P] where
   /-- returns the source of the ray. -/
   source : P
   /-- returns the direction of the ray. -/
@@ -66,7 +66,7 @@ alias Ray.mk_pt_dir := Ray.mk
 
 /-- A \emph{Segment} consists of a pair of points: the source and the target; it is the segment from the source to the target. (We allow the source and the target to be the same.) -/
 @[ext]
-structure Seg (P : Type _) [EuclideanPlane P] where
+structure Seg (P : Type*) [EuclideanPlane P] where
   /-- returns the source of the segment. -/
   source : P
   /-- returns the target of the segment. -/
@@ -77,17 +77,17 @@ attribute [pp_dot] Seg.source Seg.target
 namespace Seg
 
 /-- Given a segment $AB$, this function returns whether the segment $AB$ is nondegenerate, i.e. whether $A \neq B$. -/
-def IsND {P : Type _} [EuclideanPlane P] (seg : Seg P) : Prop := seg.target ≠ seg.source
+def IsND {P : Type*} [EuclideanPlane P] (seg : Seg P) : Prop := seg.target ≠ seg.source
 
 end Seg
 
 /-- A \emph{nondegenerate segment} is a segment $AB$ that is nondegenerate, i.e. $A \neq B$. -/
-def SegND (P : Type _) [EuclideanPlane P] := {seg : Seg P // seg.IsND}
+def SegND (P : Type*) [EuclideanPlane P] := {seg : Seg P // seg.IsND}
 
 
 end definition
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 
 section make
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean
index 0998cf365..843bce727 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean
@@ -5,7 +5,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P] (seg_nd : SegND P)
+variable {P : Type*} [EuclideanPlane P] (seg_nd : SegND P)
 
 -- theorem same_extn_of_source_lies_int {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd A seg_nd.target ) = seg_nd.extension
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean
index 92dfe8739..39de2ef30 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean
@@ -35,7 +35,7 @@ structure Angle (P : Type*) [EuclideanPlane P] where
 
 attribute [pp_dot] Angle.source Angle.dir₁ Angle.dir₂
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Angle
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean
index 029b11e56..527345c77 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean
@@ -11,7 +11,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Angle
 
@@ -261,7 +261,7 @@ end Angle
 
 section Parallel
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 -- should be stated use mod 2pi first, then back to pi or -pi
 
 structure IsCorrespondingAng (ang₁ ang₂ : Angle P) : Prop where
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean
index d0f0601e8..92401e6f1 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean
@@ -5,7 +5,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean
index b22e6eb74..b7b9b708f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean
@@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem perp_foot_lies_int_ray_of_acute_ang {A B C : P} (b_ne_a : B ≠ A) (c_ne_a : C ≠ A) (acu : Angle.IsAcu (ANG B A C b_ne_a c_ne_a)) : (perp_foot C (LIN A B b_ne_a)) LiesInt (RAY A B b_ne_a) := by sorry
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean
index 6521a3c3f..747b12379 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean
@@ -5,7 +5,7 @@ namespace EuclidGeom
 
 open AngValue
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Angle
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean
index 430552bd0..44a79e62d 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean
@@ -5,7 +5,7 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Quadrilateral
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem cvx_of_inscribed_to_cvx {X Y Z W A B C D : P} (h : (QDR A B C D).IsConvex) (h1 : X LiesInt (SEG A B)) (h2 : Y LiesInt (SEG B C)) (h3 : Z LiesInt (SEG C D)) (h4 : W LiesInt (SEG D A)) : (QDR X Y Z W).IsConvex := by sorry
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean
index e9b18b2ac..f5b9e5499 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean
@@ -5,7 +5,7 @@ import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem pts_are_distinct_of_two_rays_of_angle (ang : Angle P) (nontriv : ang.IsND) (A B : P) (ha : A LiesInt ang.start_ray) (hb : B LiesInt ang.end_ray) : A ≠ B := by sorry
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
index 678443575..0eb4a4ce9 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
@@ -2,7 +2,7 @@ import EuclideanGeometry.Foundation.Axiom.Position.Orientation
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem liesonleft_iff_liesonright_reverse {A : P} {l : DirLine P} : A LiesOnLeft l ↔ A LiesOnRight l.reverse := by
   have : odist A l.reverse = -odist A l := by
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index 1be335db0..334817cc8 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -1,8 +1,6 @@
 import EuclideanGeometry.Foundation.Axiom.Position.Orientation
 import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 
-universe u
-
 noncomputable section
 namespace EuclidGeom
 
@@ -11,14 +9,14 @@ open AngValue
 
 /- Class of generalized triangles -/
 @[ext]
-structure Triangle (P : Type u) [EuclideanPlane P] where
+structure Triangle (P : Type*) [EuclideanPlane P] where
   point₁ : P
   point₂ : P
   point₃ : P
 
 namespace Triangle
 
-variable {P : Type u} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 --implies  1 left of 23, 2 left of 31
 
 -- not is_cclock implies 1 right of 23, ..., ...
@@ -42,11 +40,11 @@ def IsND (tr : Triangle P) : Prop := ¬ Collinear tr.1 tr.2 tr.3
 
 end Triangle
 
-def TriangleND (P : Type u) [EuclideanPlane P] := { tr : Triangle P // tr.IsND }
+def TriangleND (P : Type*) [EuclideanPlane P] := { tr : Triangle P // tr.IsND }
 
 namespace TriangleND
 
-variable {P : Type u} [EuclideanPlane P] (tr_nd : TriangleND P)
+variable {P : Type*} [EuclideanPlane P] (tr_nd : TriangleND P)
 
 @[pp_dot]
 abbrev point₁ : P := tr_nd.1.1
@@ -102,7 +100,7 @@ def angle₃ : Angle P := ANG tr_nd.point₁ tr_nd.point₃ tr_nd.point₂
 
 end TriangleND
 
-variable {P : Type u} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 namespace Triangle
 
@@ -156,7 +154,7 @@ instance : IntFig Triangle where
 
 end TriangleND
 
-variable {P : Type _} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P)
+variable {P : Type*} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P)
 
 namespace Triangle
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
index cc32fc557..79ee4857c 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
@@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P)
+variable {P : Type*} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P)
 --perm and flip is moved to the main file
 
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean
index d546e59dd..96eee676f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean
@@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex
 namespace EuclidGeom
 open AngValue
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 structure TriangleND.IsAcute (tr_nd : TriangleND P) : Prop where
   angle₁ : tr_nd.angle₁.IsAcu
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean
index 2f3ce4f21..0ac9ad38f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean
@@ -11,7 +11,7 @@ namespace EuclidGeom
 
 /- congruences of triangles, separate definitions for reversing orientation or not, (requiring all sides and angles being the same)-/
 
-variable {P : Type _} [EuclideanPlane P] {tr tr₁ tr₂ tr₃ : Triangle P} {tr_nd tr_nd₁ tr_nd₂ tr_nd₃ : TriangleND P}
+variable {P : Type*} [EuclideanPlane P] {tr tr₁ tr₂ tr₃ : Triangle P} {tr_nd tr_nd₁ tr_nd₂ tr_nd₃ : TriangleND P}
 
 open Classical AngValue Angle
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean
index 42524a134..86a556fa2 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean
@@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem Triangle.IsCongr.unique_of_eq_eq {tr₁ tr₂ : Triangle P} (h : tr₁.IsCongr tr₂) (p₁ : tr₁.point₁ = tr₂.point₁) (p₂ : tr₁.point₂ = tr₂.point₂) [hne : PtNe tr₁.point₁ tr₁.point₂] : tr₁.point₃ = tr₂.point₃ := sorry
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean
index ee5762027..5c1a893d0 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean
@@ -9,7 +9,7 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 -- Prefer to define IsIsocelesTriangle than to just state the properties. Isoceles triangle by definition has a prefered orientation
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean
index eed2a4059..442e51272 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean
@@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 lemma isoceles_tri_pts_ne {tri : Triangle P} (h : tri.IsIsoceles) (hne : tri.point₂ ≠ tri.point₃) : (tri.point₁ ≠ tri.point₂) ∧ (tri.point₁ ≠ tri.point₃) := sorry
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean
index e25e8a457..765ede2fb 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean
@@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Angle
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P] {tr₁ tr₂ tr₃ : TriangleND P}
+variable {P : Type*} [EuclideanPlane P] {tr₁ tr₂ tr₃ : TriangleND P}
 
 open TriangleND AngValue
 
diff --git a/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean b/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean
index 5b6da2ab1..1f36b5f28 100644
--- a/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean
+++ b/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean
@@ -8,7 +8,7 @@ open Classical
 
 section Ceva's_converse_theorem
 
-structure Setting (P : Type _) [EuclideanPlane P] where
+structure Setting (P : Type*) [EuclideanPlane P] where
   -- Let $\triangle ABC$ be a nondegenerate triangle.
   A : P
   B : P
@@ -32,7 +32,7 @@ structure Setting (P : Type _) [EuclideanPlane P] where
   -- $\frac{EB}{EC} \cdot \frac{FC}{FA} \cdot \frac{GA}{GB} = -1$.
   ratio_mul_eq_minus_one : (divratio E B C) * (divratio F C A) * (divratio G A B) = -1
 
-theorem Ceva_converse_theorem {P : Type _} [EuclideanPlane P] (e : Setting P) : ∃ (X : P), (X LiesOn (LIN e.A e.E e.E_ne_A)) ∧ (X LiesOn (LIN e.B e.F e.F_ne_B)) ∧ (X LiesOn (LIN e.C e.G e.G_ne_C)) := by
+theorem Ceva_converse_theorem {P : Type*} [EuclideanPlane P] (e : Setting P) : ∃ (X : P), (X LiesOn (LIN e.A e.E e.E_ne_A)) ∧ (X LiesOn (LIN e.B e.F e.F_ne_B)) ∧ (X LiesOn (LIN e.C e.G e.G_ne_C)) := by
   let D := Line.inx (LIN e.A e.E (TriangleND.points_ne_of_collinear_of_not_collinear1 e.not_collinear_ABC e.collinear_EBC)) (LIN e.B e.F (TriangleND.points_ne_of_collinear_of_not_collinear2 e.not_collinear_ABC e.collinear_FCA)) (TriangleND.not_parallel_of_not_collinear_of_collinear_collinear e.not_collinear_ABC e.collinear_EBC e.collinear_FCA)
   have ratiomul : (divratio e.E e.B e.C) * (divratio e.F e.C e.A) * (divratio e.G e.A e.B) = -1 := e.ratio_mul_eq_minus_one
   have E_ne_C : e.E ≠ e.C := by
diff --git a/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean b/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean
index 40a3ee284..d3e476b78 100644
--- a/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean
+++ b/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean
@@ -6,7 +6,7 @@ namespace EuclidGeom
 
 open Classical
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section oarea_method
 
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean b/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean
index 2789a4ad5..d4204cd1c 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean
@@ -6,10 +6,10 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Quadrilateral
 noncomputable section
 namespace EuclidGeom
 
-structure Polygon (P : Type _) [EuclideanPlane P] where
+structure Polygon (P : Type*) [EuclideanPlane P] where
 
-structure ConvexPolygon (P : Type _) [EuclideanPlane P] extends Polygon P where
+structure ConvexPolygon (P : Type*) [EuclideanPlane P] extends Polygon P where
 
-structure RegularPolygon (P : Type _) [EuclideanPlane P] extends ConvexPolygon P where
+structure RegularPolygon (P : Type*) [EuclideanPlane P] extends ConvexPolygon P where
 
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean
index 2154c02e4..cfec47f66 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean
@@ -38,20 +38,20 @@ In this section we define two types of parallelograms. 'parallel_nd' deals with
 
 -- /-- A QuadrilateralND satisfies IsPara if two sets of opposite sides are parallel respectively. -/
 -- @[pp_dot]
--- def QuadrilateralND.IsParaPara {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃)
+-- def QuadrilateralND.IsParaPara {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃)
 
 -- -- scoped postfix : 50 "IsParaPara" => QuadrilateralND.IsParaPara
 
 -- /-- A quadrilateral satisfies IsPara if it is a QuadrilateralND and satisfies IsPara as a QuadrilateralND. -/
 -- @[pp_dot]
--- def Quadrilateral.IsParaPara {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
+-- def Quadrilateral.IsParaPara {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
 --   by_cases h : qdr.IsND
 --   · exact (QuadrilateralND.mk_nd h).IsParaPara
 --   · exact False
 
 /-- A quadrilateral satisfies IsPara if it is a QuadrilateralND and satisfies IsPara as a QuadrilateralND. -/
 @[pp_dot]
-def Quadrilateral.IsParaPara {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
+def Quadrilateral.IsParaPara {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
   by_cases h : qdr.IsND
   · have qdr_nd : QuadrilateralND P := QDR_nd' h
     exact (qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₄₁ ∥ qdr_nd.edgeND₂₃)
@@ -59,67 +59,67 @@ def Quadrilateral.IsParaPara {P : Type _} [EuclideanPlane P] (qdr : Quadrilatera
 
 /-- A quadrilateral is called parallelogram if VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃.-/
 @[pp_dot]
-def Quadrilateral.IsPrg {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃
+def Quadrilateral.IsPrg {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃
 
 scoped postfix : 50 "IsPrg" => Quadrilateral.IsPrg
 
 -- `shall we define this?`
 -- /-- A QuadrilateralND is called parallelogram if VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃.-/
 -- @[pp_dot]
--- def QuadrilateralND.IsPrg {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := VEC qdr_nd.point₁ qdr_nd.point₂ = VEC qdr_nd.point₄ qdr_nd.point₃
+-- def QuadrilateralND.IsPrg {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := VEC qdr_nd.point₁ qdr_nd.point₂ = VEC qdr_nd.point₄ qdr_nd.point₃
 
 -- scoped postfix : 50 "nd_IsPrg" => QuadrilateralND.IsPrg
 
 /-- We define parallelogram as a structure. -/
 @[ext]
-structure Parallelogram (P : Type _) [EuclideanPlane P] extends Quadrilateral P where
+structure Parallelogram (P : Type*) [EuclideanPlane P] extends Quadrilateral P where
   is_parallelogram : toQuadrilateral IsPrg
 
 /-- Make a parallelogram with 4 points on a plane, and using condition IsPrg. -/
-def Parallelogram.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsPrg) : Parallelogram P where
+def Parallelogram.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsPrg) : Parallelogram P where
   toQuadrilateral := (QDR A B C D)
   is_parallelogram := h
 
 scoped notation "PRG" => Parallelogram.mk_pt_pt_pt_pt
 
 /-- Make a parallelogram with a quadrilateral, and using condition IsPrg. -/
-def Parallelogram.mk_isPrg {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrg) : Parallelogram P where
+def Parallelogram.mk_isPrg {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrg) : Parallelogram P where
   toQuadrilateral := qdr
   is_parallelogram := h
 
 scoped notation "PRG'" => Parallelogram.mk_isPrg
 
 /-- Vectors point₁ point₂ and point₄ point₃ in a parallelogram are equal. -/
-theorem Parallelogram.eq_vec_of_isPrg {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₂ = VEC prg.point₄ prg.point₃ := prg.is_parallelogram
+theorem Parallelogram.eq_vec_of_isPrg {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₂ = VEC prg.point₄ prg.point₃ := prg.is_parallelogram
 
 /-- Vectors point₁ point₄ and point₂ point₃ in a parallelogram are equal. -/
-theorem Parallelogram.eq_vec_of_isPrg' {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₄ = VEC prg.point₂ prg.point₃ := by rw [← vec_add_vec prg.point₁ prg.point₂ prg.point₄, ← vec_add_vec prg.point₂ prg.point₄ prg.point₃, prg.is_parallelogram, add_comm]
+theorem Parallelogram.eq_vec_of_isPrg' {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₄ = VEC prg.point₂ prg.point₃ := by rw [← vec_add_vec prg.point₁ prg.point₂ prg.point₄, ← vec_add_vec prg.point₂ prg.point₄ prg.point₃, prg.is_parallelogram, add_comm]
 
 /-- A parallelogram which satisfies Prallelogram.InGPos satisfies IsParaPara. -/
-theorem Parallelogram.parapara_of_gpos {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsParaPara:= by
+theorem Parallelogram.parapara_of_gpos {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsParaPara:= by
   unfold Quadrilateral.IsParaPara
   sorry
 
 /-- A parallelogram which satisfies Prallelogram.InGPos is convex. -/
-theorem Parallelogram.cvx_of_gpos {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsConvex:= by sorry
+theorem Parallelogram.cvx_of_gpos {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsConvex:= by sorry
 
 /-- We define parallelogram_nd as a structure. -/
 @[ext]
-structure ParallelogramND (P : Type _) [EuclideanPlane P] extends Quadrilateral_cvx P, Parallelogram P
+structure ParallelogramND (P : Type*) [EuclideanPlane P] extends Quadrilateral_cvx P, Parallelogram P
 
 /-- A quadrilateral is parallelogram_nd if it is both convex and satisfies qualities of a parallelogram. This definition is in agreement with the structure above. -/
 @[pp_dot]
-def Quadrilateral.IsPrgND {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := qdr IsConvex ∧ qdr IsPrg
+def Quadrilateral.IsPrgND {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := qdr IsConvex ∧ qdr IsPrg
 
 scoped postfix : 50 "IsPrgND" => Quadrilateral.IsPrgND
 
 -- /-- A QuadrilateralND is parallelogram_nd if its toQuadrilateral is both convex and satisfies qualities of a parallelogram. -/
 -- @[pp_dot]
--- def QuadrilateralND.IsPrgND {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := Quadrilateral.IsPrgND qdr_nd.toQuadrilateral
+-- def QuadrilateralND.IsPrgND {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := Quadrilateral.IsPrgND qdr_nd.toQuadrilateral
 
 -- scoped postfix : 50 "nd_IsPrgND" => QuadrilateralND.IsPrgND
 
-theorem QuadrilateralND.parapara_iff_para_para {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : (qdr_nd.IsParaPara) ↔ (qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₄₁ ∥ qdr_nd.edgeND₂₃) := by
+theorem QuadrilateralND.parapara_iff_para_para {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : (qdr_nd.IsParaPara) ↔ (qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₄₁ ∥ qdr_nd.edgeND₂₃) := by
   constructor
   unfold Quadrilateral.IsParaPara
   simp only [dite_true, qdr_nd.nd, and_imp]
@@ -129,10 +129,10 @@ theorem QuadrilateralND.parapara_iff_para_para {P : Type _} [EuclideanPlane P] (
   exact fun a a_1 ↦ { left := a, right := a_1 }
 
 /-- A parallelogram_nd satisfies InGPos. -/
-theorem ParallelogramND.gpos_of_prgnd {P : Type _} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.InGPos := ⟨prg_nd.not_collinear₁₂₃, prg_nd.not_collinear₂₃₄, prg_nd.not_collinear₃₄₁, prg_nd.not_collinear₄₁₂⟩
+theorem ParallelogramND.gpos_of_prgnd {P : Type*} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.InGPos := ⟨prg_nd.not_collinear₁₂₃, prg_nd.not_collinear₂₃₄, prg_nd.not_collinear₃₄₁, prg_nd.not_collinear₄₁₂⟩
 
 /-- A parallelogram_nd satisfies IsParaPara. -/
-theorem ParallelogramND.parapara_of_prgnd {P : Type _} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.IsParaPara := by
+theorem ParallelogramND.parapara_of_prgnd {P : Type*} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.IsParaPara := by
   unfold Quadrilateral.IsParaPara
   simp only [dite_true, prg_nd.nd]
   unfold Parallel
@@ -144,14 +144,14 @@ theorem ParallelogramND.parapara_of_prgnd {P : Type _} [EuclideanPlane P] (prg_n
   sorry
   sorry
 
-def ParallelogramND.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h: (QDR A B C D) IsPrgND) : ParallelogramND P where
+def ParallelogramND.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h: (QDR A B C D) IsPrgND) : ParallelogramND P where
   toQuadrilateral := (QDR A B C D)
   nd := h.left; convex := h.left
   is_parallelogram := h.right
 
 scoped notation "PRG_nd" => ParallelogramND.mk_pt_pt_pt_pt
 
-def ParallelogramND.mk_isPrgND {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrgND) : ParallelogramND P where
+def ParallelogramND.mk_isPrgND {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrgND) : ParallelogramND P where
   toQuadrilateral := qdr
   nd := h.left; convex := h.left
   is_parallelogram := h.right
@@ -160,7 +160,7 @@ scoped notation "PRG_nd'" => ParallelogramND.mk_isPrgND
 
 /-
  Using the property above, we leave such a shortcut in a way people usually sense a parallelogram. A quadrilateral A B C D is parallelogram_nd if it is ND, is a parallelogram, and satisfies InGPos.
-def ParallelogramND.mk_prgND_of_gpos {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} (gpos: prg.InGPos): ParallelogramND P where
+def ParallelogramND.mk_prgND_of_gpos {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} (gpos: prg.InGPos): ParallelogramND P where
   toQuadrilateral := prg.toQuadrilateral
   nd := sorry
   convex := sorry
@@ -170,7 +170,7 @@ def ParallelogramND.mk_prgND_of_gpos {P : Type _} [EuclideanPlane P] {prg : Para
 scoped notation "non_triv_PRG_nd" => ParallelogramND.mk_prgND_of_gpos
 
 A quadrilateral A B C D is parallelogram_nd if it is ND, is a parallelogram, and satisfies IsParaPara.
---def ParallelogramND.mk_prgND_of_para {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsPrg) (IsPara: (QDR_nd A B C D h).IsParaPara): ParallelogramND P where
+--def ParallelogramND.mk_prgND_of_para {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsPrg) (IsPara: (QDR_nd A B C D h).IsParaPara): ParallelogramND P where
   point₁ := A; point₂ := B; point₃ := C; point₄ := D
   nd := h
   convex := sorry
@@ -180,14 +180,14 @@ A quadrilateral A B C D is parallelogram_nd if it is ND, is a parallelogram, and
 scoped notation "IsParaPara_PRG_nd" => ParallelogramND.mk_parallelogram_para
 
 here is two theorem using first version of definition of PRG_nd, may not useful currently.
-theorem Quadrilateral.IsPrg_nd_redef {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsPrg) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h).IsPrgND := sorry
+theorem Quadrilateral.IsPrg_nd_redef {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsPrg) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h).IsPrgND := sorry
 
-theorem Parallelogram.parallelogramIs_nd_redef {P : Type _} [EuclideanPlane P] (prg : Parallelogram P) (h': prg.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h').IsPrgND := sorry
+theorem Parallelogram.parallelogramIs_nd_redef {P : Type*} [EuclideanPlane P] (prg : Parallelogram P) (h': prg.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h').IsPrgND := sorry
 -/
 
 section perm
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable (qdr : Quadrilateral P)
 variable (qdr_nd : QuadrilateralND P)
 variable (qdr_cvx : Quadrilateral_cvx P)
@@ -219,7 +219,7 @@ end perm
 
 section flip
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable (qdr : Quadrilateral P)
 variable (qdr_nd : QuadrilateralND P)
 variable (qdr_cvx : Quadrilateral_cvx P)
@@ -251,7 +251,7 @@ end flip
 
 section criteria_prgND_of_prg
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable (qdr_nd : QuadrilateralND P)
 variable (prg : Parallelogram P)
 
@@ -288,7 +288,7 @@ end criteria_prgND_of_prg
 
 section criteria_prgND_of_qdrND
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable {A B C D : P} (nd : (QDR A B C D).IsND)
 variable (qdr : Quadrilateral P) (qdr_nd : QuadrilateralND P)
 
@@ -330,12 +330,12 @@ end criteria_prgND_of_qdrND
 
 section criteria_prg_of_qdrND
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable {A B C D: P}
 variable (nd : (QDR A B C D).IsND)
 variable (cvx : (QDR A B C D).IsConvex)
-variable {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P)
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
 
 -- `why this theorem used two set of parallel and equal?`
 /-- If edgeND₁₂ and edgeND₃₄ of a QuadrilateralND are equal in value and parallel, and so do edgeND₁₄ and edgeND₂₃, then it is a parallelogram. -/
@@ -354,12 +354,12 @@ end criteria_prg_of_qdrND
 
 section criteria_prgND_of_qdrcvx
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable {A B C D : P}
 variable (nd : (QDR A B C D).IsND)
 variable (cvx : (QDR A B C D).IsConvex)
-variable {P : Type _} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P)
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
 
 /-- If edgeND₁₂ and edgeND₃₄ of a quadrilateral_cvx are parallel, and so do edgeND₁₄ and edgeND₂₃, then it is a parallelogram_nd. -/
 theorem qdrcvx_is_prgND_of_parapara (h₁ : qdr_cvx.IsParaPara) : qdr_cvx.IsPrgND := by sorry
@@ -387,10 +387,10 @@ end criteria_prgND_of_qdrcvx
 
 section property
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable {A B C D : P}
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
-variable {P : Type _} [EuclideanPlane P] (prg : Parallelogram P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (prg : Parallelogram P)
 
 /-- The lengths of segments point₁ point₂ and point₃ point₄ in a parallelogram are equal. -/
 theorem eq_length_of_isPrg : (prg.edge₁₂).length = (prg.edge₃₄).length := by sorry
@@ -415,10 +415,10 @@ end property
 
 section property_nd
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable {A B C D : P}
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
-variable {P : Type _} [EuclideanPlane P] (prg_nd : ParallelogramND P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (prg_nd : ParallelogramND P)
 
 /-- In a parallelogram_nd, edgeND₁₂ and edge₃₄ are parallel. -/
 theorem para_of_isPrgND : prg_nd.edgeND₁₂ ∥ prg_nd.edgeND₃₄ := (prg_nd.parapara_iff_para_para.mp prg_nd.parapara_of_prgnd).left
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean
index afdc5a6d4..a3c62b87f 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean
@@ -34,7 +34,7 @@ In this section we define two types of parallelogram. 'parallel_nd' deals with t
 -/
 
 @[pp_dot]
-structure Quadrilateral_nd.Parallelogram_GPt {P : Type _} [EuclideanPlane P] (qdr_nd : Quadrilateral_nd P) : Prop where
+structure Quadrilateral_nd.Parallelogram_GPt {P : Type*} [EuclideanPlane P] (qdr_nd : Quadrilateral_nd P) : Prop where
   not_collinear₁₂₃: ( ¬ Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃)
   not_collinear₂₃₄: ( ¬ Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄)
   not_collinear₃₄₁: ( ¬ Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁)
@@ -42,18 +42,18 @@ structure Quadrilateral_nd.Parallelogram_GPt {P : Type _} [EuclideanPlane P] (qd
 
 /-- A quadrilateral is called parallelogram if VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃.-/
 @[pp_dot]
-def Quadrilateral.IsParallelogram {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃
+def Quadrilateral.IsParallelogram {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃
 
 /-- A quadrilateral satisfies IsParallelogram_para if two sets of opposite sides are parallel respectively. -/
 @[pp_dot]
-def QuadrilateralND.IsParallelogram_para {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃)
+def QuadrilateralND.IsParallelogram_para {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃)
 
 /-- A quadrilateral satisfies IsParallelogram_nd if it satisfies both IsParallelogram_para and Parallelogram_GPt. It is now what we commonly call parallelogram.-/
 @[pp_dot]
-def QuadrilateralND.IsParallelogram_nd {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := qdr_nd.IsParallelogram_para ∧ qdr_nd.Parallelogram_non_triv
+def QuadrilateralND.IsParallelogram_nd {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := qdr_nd.IsParallelogram_para ∧ qdr_nd.Parallelogram_non_triv
 
 @[pp_dot]
-def Quadrilateral.IsParallelogram_nd {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
+def Quadrilateral.IsParallelogram_nd {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
   by_cases h : qdr.IsND
   · exact (QuadrilateralND.mk_nd h).IsParallelogram_nd
   · exact False
@@ -65,28 +65,28 @@ scoped postfix : 50 "IsParallelogram_nd" => QuadrilateralND.IsParallelogram_nd
 
 /-- We define parallelogram as a structure.-/
 @[ext]
-structure Parallelogram (P : Type _) [EuclideanPlane P] extends Quadrilateral P where
+structure Parallelogram (P : Type*) [EuclideanPlane P] extends Quadrilateral P where
   is_parallelogram : toQuadrilateral IsParallelogram
 
 /-- We define parallelogram_nd as a structure.-/
 @[ext]
-structure Parallelogram_nd (P : Type _) [EuclideanPlane P] extends Quadrilateral_nd P, Parallelogram P where
+structure Parallelogram_nd (P : Type*) [EuclideanPlane P] extends Quadrilateral_nd P, Parallelogram P where
   is_parallelogram_para : toQuadrilateral_nd IsParallelogram_para
   is_parallelogram_GPt : toQuadrilateral_nd IsParallelogram_GPt
 
 /-- We would also like to introduce a shortcut in proving statements concerning parallelograms - that is perm, the same technique used in Quadrilateral.lean. If qdr IsParallelogram, then its perm also IsParallelogram. -/
-theorem qdr_is_parallelogram_perm_iff (P : Type _) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram) ↔ ((qdr.perm).IsParallelogram) := by
+theorem qdr_is_parallelogram_perm_iff (P : Type*) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram) ↔ ((qdr.perm).IsParallelogram) := by
   sorry
 
 /-- If qdr IsParallelogram_nd, then its perm also IsParallelogram_nd. -/
-theorem qdr_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram_nd) ↔ ((qdr.perm).IsParallelogram_nd) := by
+theorem qdr_is_parallelogram_nd_perm_iff (P : Type*) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram_nd) ↔ ((qdr.perm).IsParallelogram_nd) := by
   sorry
 
 /-- If qdr_nd IsParallelogram, then its perm also IsParallelogram. -/
-theorem qdr_nd_is_parallelogram_perm_iff (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram) ↔ ((qdr_nd.perm).IsParallelogram) := by sorry
+theorem qdr_nd_is_parallelogram_perm_iff (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram) ↔ ((qdr_nd.perm).IsParallelogram) := by sorry
 
 /-- If qdr_nd IsParallelogram_nd, then its perm also IsParallelogram. -/
-theorem qdr_nd_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram_nd) ↔ ((qdr_nd.perm).IsParallelogram_nd) := by
+theorem qdr_nd_is_parallelogram_nd_perm_iff (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram_nd) ↔ ((qdr_nd.perm).IsParallelogram_nd) := by
   constructor
   intro h
   unfold QuadrilateralND.IsParallelogram_nd
@@ -149,11 +149,11 @@ theorem qdr_nd_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (qdr
   exact z
 
 /-- If prg IsParallelogram_nd, then its perm also IsParallelogram_nd. -/
-theorem prg_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (prg : Parallelogram P) :(prg.IsParallelogram_nd) ↔ ((prg.perm).IsParallelogram_nd) := by
+theorem prg_is_parallelogram_nd_perm_iff (P : Type*) [EuclideanPlane P] (prg : Parallelogram P) :(prg.IsParallelogram_nd) ↔ ((prg.perm).IsParallelogram_nd) := by
   sorry
 
 /-- If qdr_nd is non-degenerate and is a parallelogram, and its 1st, 2nd and 3rd points are not collinear, then qdr_nd is a parallelogram_nd.-/
-theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃) : qdr_nd IsParallelogram_nd := by
+theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃) : qdr_nd IsParallelogram_nd := by
 
    have hba : qdr_nd.point₂ ≠ qdr_nd.point₁ := by
      unfold collinear at h
@@ -312,24 +312,24 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qd
    simp [Collinear.perm₂₁₃ m₇] at m₆
 
 /-- If qdr_nd is non-degenerate and is a parallelogram, and its 2nd, 3rd and 4th points are not collinear, then qdr_nd is a parallelogram_nd.-/
-theorem Parallelogram_not_collinear₂₃₄ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) : qdr_nd IsParallelogram_nd := by
+theorem Parallelogram_not_collinear₂₃₄ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) : qdr_nd IsParallelogram_nd := by
   sorry
 
 /-- If qdr_nd is non-degenerate and is a parallelogram, and its 3rd, 4th and 1st points are not collinear, then qdr_nd is a parallelogram_nd.-/
-theorem Parallelogram_not_collinear₃₄₁ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁) : qdr_nd IsParallelogram_nd := by
+theorem Parallelogram_not_collinear₃₄₁ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁) : qdr_nd IsParallelogram_nd := by
   sorry
 
 /-- If qdr_nd is non-degenerate and is a parallelogram, and its 4th, 1st and 2nd points are not collinear, then qdr_nd is a parallelogram_nd.-/
-theorem Parallelogram_not_collinear₄₁₂ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₄ qdr_nd.point₁ qdr_nd.point₂) : qdr_nd IsParallelogram_nd := by
+theorem Parallelogram_not_collinear₄₁₂ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₄ qdr_nd.point₁ qdr_nd.point₂) : qdr_nd IsParallelogram_nd := by
   sorry
 
 /-- Make a parallelogram with 4 points on a plane.-/
-def Parallelogram.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsParallelogram) : Parallelogram P where
+def Parallelogram.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsParallelogram) : Parallelogram P where
   toQuadrilateral := (QDR A B C D)
   is_parallelogram := h
 
 /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₁₂₃.-/
-def Parallelogram_nd.mk_pt_pt_pt_pt₄ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₁₂₃: ¬ Collinear A B C) : Parallelogram_nd P where
+def Parallelogram_nd.mk_pt_pt_pt_pt₄ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₁₂₃: ¬ Collinear A B C) : Parallelogram_nd P where
   toQuadrilateral := (QDR A B C D)
   is_parallelogram := h'
   nd := h
@@ -337,7 +337,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₄ {P : Type _} [EuclideanPlane P] (A B C D
   is_parallelogram_GPt := sorry
 
 /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₂₃₄.-/
-def Parallelogram_nd.mk_pt_pt_pt_pt₁ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₂₃₄: ¬ Collinear B C D) : Parallelogram_nd P where
+def Parallelogram_nd.mk_pt_pt_pt_pt₁ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₂₃₄: ¬ Collinear B C D) : Parallelogram_nd P where
   toQuadrilateral := (QDR A B C D)
   is_parallelogram := h'
   nd := h
@@ -345,7 +345,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₁ {P : Type _} [EuclideanPlane P] (A B C D
   is_parallelogram_GPt := sorry
 
 /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₃₄₁.-/
-def Parallelogram_nd.mk_pt_pt_pt_pt₂ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₃₄₁: ¬ Collinear C D A) : Parallelogram_nd P where
+def Parallelogram_nd.mk_pt_pt_pt_pt₂ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₃₄₁: ¬ Collinear C D A) : Parallelogram_nd P where
   toQuadrilateral := (QDR A B C D)
   is_parallelogram := h'
   nd := h
@@ -353,7 +353,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₂ {P : Type _} [EuclideanPlane P] (A B C D
   is_parallelogram_GPt := sorry
 
 /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₄₁₂.-/
-def Parallelogram_nd.mk_pt_pt_pt_pt₃ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₄₁₂: ¬ Collinear D A B) : Parallelogram_nd P where
+def Parallelogram_nd.mk_pt_pt_pt_pt₃ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₄₁₂: ¬ Collinear D A B) : Parallelogram_nd P where
   toQuadrilateral := (QDR A B C D)
   is_parallelogram := h'
   nd := h
@@ -361,7 +361,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₃ {P : Type _} [EuclideanPlane P] (A B C D
   is_parallelogram_GPt := sorry
 
 /-- Make a parallelogram_nd with 4 points on a plane.-/
-def Parallelogram_nd.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear: (QuadrilateralND.mk_nd h) IsParallelogram_non_triv) : Parallelogram_nd P where
+def Parallelogram_nd.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear: (QuadrilateralND.mk_nd h) IsParallelogram_non_triv) : Parallelogram_nd P where
   toQuadrilateral := (QDR A B C D)
   is_parallelogram := h'
   nd := h
@@ -376,12 +376,12 @@ scoped notation "PRG_nd₄" => Parallelogram_nd.mk_pt_pt_pt_pt₄
 scoped notation "PRG_nd" => Parallelogram_nd.mk_pt_pt_pt_pt
 
 /-- Make parallelogram with a quadrilateral.-/
-def mk_parallelogram {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) : Parallelogram P where
+def mk_parallelogram {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) : Parallelogram P where
   toQuadrilateral := qdr
   is_parallelogram := h
 
 /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₁₂₃.-/
-def mk_parallelogram_nd₄ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₁₂₃: ¬ Collinear qdr.1 qdr.2 qdr.3) : Parallelogram_nd P where
+def mk_parallelogram_nd₄ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₁₂₃: ¬ Collinear qdr.1 qdr.2 qdr.3) : Parallelogram_nd P where
   toQuadrilateral := qdr
   is_parallelogram := h
   nd := h'
@@ -389,7 +389,7 @@ def mk_parallelogram_nd₄ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral
   is_parallelogram_GPt := sorry
 
 /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₂₃₄.-/
-def mk_parallelogram_nd₁ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₂₃₄: ¬ Collinear qdr.2 qdr.3 qdr.4) : Parallelogram_nd P where
+def mk_parallelogram_nd₁ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₂₃₄: ¬ Collinear qdr.2 qdr.3 qdr.4) : Parallelogram_nd P where
   toQuadrilateral := qdr
   is_parallelogram := h
   nd := h'
@@ -397,7 +397,7 @@ def mk_parallelogram_nd₁ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral
   is_parallelogram_GPt := sorry
 
 /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₃₁₄.-/
-def mk_parallelogram_nd₂ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₃₄₁: ¬ Collinear qdr.3 qdr.4 qdr.1) : Parallelogram_nd P where
+def mk_parallelogram_nd₂ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₃₄₁: ¬ Collinear qdr.3 qdr.4 qdr.1) : Parallelogram_nd P where
   toQuadrilateral := qdr
   is_parallelogram := h
   nd := h'
@@ -405,7 +405,7 @@ def mk_parallelogram_nd₂ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral
   is_parallelogram_GPt := sorry
 
 /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₄₁₂.-/
-def mk_parallelogram_nd₃ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₄₁₂: ¬ Collinear qdr.4 qdr.1 qdr.2) : Parallelogram_nd P where
+def mk_parallelogram_nd₃ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₄₁₂: ¬ Collinear qdr.4 qdr.1 qdr.2) : Parallelogram_nd P where
   toQuadrilateral := qdr
   is_parallelogram := h
   nd := h'
@@ -413,7 +413,7 @@ def mk_parallelogram_nd₃ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral
   is_parallelogram_GPt := sorry
 
 /-- Make parallelogram_nd with a quadrilateral.-/
-def mk_parallelogram_nd {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear: (QuadrilateralND.mk_nd h') IsParallelogram_non_triv) : Parallelogram_nd P where
+def mk_parallelogram_nd {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear: (QuadrilateralND.mk_nd h') IsParallelogram_non_triv) : Parallelogram_nd P where
   toQuadrilateral := qdr
   is_parallelogram := h
   nd := h'
@@ -421,7 +421,7 @@ def mk_parallelogram_nd {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P}
   is_parallelogram_GPt := sorry
 
 /-- Here is also a quite odd definition of a quadrilateral or parallelogram being parallelogram_nd, concerning angle being positive or negative. As it may be useful when discussing cclocks, it is reserved in form of the two theorems below.-/
-theorem Quadrilateral.IsParallelogram_nd_redef {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsParallelogram) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h) IsParallelogram_nd := sorry
+theorem Quadrilateral.IsParallelogram_nd_redef {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsParallelogram) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h) IsParallelogram_nd := sorry
 
 /--
 
@@ -433,13 +433,13 @@ The route from qdr to parallelogram will not be seperated from the main discussi
 
 -/
 @[pp_dot]
-theorem Parallelogram.ParallelogramIs_nd_redef {P : Type _} [EuclideanPlane P] (qdr_para : Parallelogram P) (h': qdr_para.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h') IsParallelogram_nd := sorry
+theorem Parallelogram.ParallelogramIs_nd_redef {P : Type*} [EuclideanPlane P] (qdr_para : Parallelogram P) (h': qdr_para.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h') IsParallelogram_nd := sorry
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section criteria_prg_nd_of_qdr_nd
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable {A B C D : P} (nd : (QDR A B C D).IsND) (cvx : (QDR A B C D).IsConvex)
 variable (qdr : Quadrilateral P) (qdr_nd : QuadrilateralND P) (qdr_cvx : Quadrilateral_cvx P)
 
@@ -610,8 +610,8 @@ section criteria_prg_of_qdr_nd
 variable {A B C D: P}
 variable (nd : (QDR A B C D).IsND)
 variable (cvx : (QDR A B C D).IsConvex)
-variable {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P)
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
 
 /-- Given QuadrilateralND qdr_nd, and qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄ and (qdr_nd.edgeND₁₂).length = (qdr_nd.edgeND₃₄).length, and qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃ and (qdr_nd.edgeND₁₄).length = (qdr_nd.edgeND₂₃).length, qdr_nd is a Parallelogram. -/
 theorem qdr_nd_is_prg_of_para_eq_length_para_eq_length (h₁ : qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) (h₂ : qdr_nd.edgeND₁₂.length = qdr_nd.edgeND₃₄.length) (H₁ : qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃) (h₂ : qdr_nd.edgeND₁₄.length = qdr_nd.edgeND₂₃.length): qdr_nd.IsParallelogram := by
@@ -636,8 +636,8 @@ section criteria_prg_nd_of_qdr_cvx
 variable {A B C D: P}
 variable (nd : (QDR A B C D).IsND)
 variable (cvx : (QDR_nd A B C D nd).IsConvex)
-variable {P : Type _} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P)
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
 
 /-- Given Quadrilateral_cvx qdr_cvx, qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄ and qdr_cvx.edgeND₁₄ ∥ qdr_cvx.edgeND₂₃, then qdr_cvx is a Parallelogram_nd. -/
 theorem qdr_cvx_is_prg_nd_of_para_para (h₁ : qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄) (h₂ : qdr_cvx.edgeND₁₄ ∥ qdr_cvx.edgeND₂₃) : qdr_cvx.IsParallelogram_nd := by
@@ -1136,7 +1136,7 @@ end criteria_prg_nd_of_qdr_cvx
 
 section property
 variable {A B C D : P}
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
 
 /-- Given Quadrilateral qdr IsPRG_nd, Quadrilateral qdr IsConvex. -/
 theorem is_convex_of_is_prg_nd (h : qdr.IsParallelogram_nd) : qdr.IsConvex := by
@@ -1302,8 +1302,8 @@ end property
 
 section property_nd
 variable {A B C D : P}
-variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P)
-variable {P : Type _} [EuclideanPlane P] (prg_nd : Parallelogram_nd P)
+variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P)
+variable {P : Type*} [EuclideanPlane P] (prg_nd : Parallelogram_nd P)
 
 /-- Given Quadrilateral qdr IsPRG_nd, Quadrilateral qdr IsND. -/
 
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean
index aeaa69960..eb4a71dec 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean
@@ -2,7 +2,7 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Parallelogram
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem vec_eq_of_eq_dir_and_eq_length {A B C D : P} (h1 : B ≠ A) (h2 : D ≠ C) (h3 : (SEG_nd A B h1).toDir = (SEG_nd C D h2).toDir) (h4 : (SEG A B).length = (SEG C D).length) : VEC A B = VEC C D := by sorry
 
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean
index 9259e36d6..83e64e0a6 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean
@@ -32,7 +32,7 @@ open Angle
 
 /-- Class of Quadrilateral: A quadrilateral consists of four points; it is the generalized quadrilateral formed by these four points -/
 @[ext]
-structure Quadrilateral (P : Type _) [EuclideanPlane P] where
+structure Quadrilateral (P : Type*) [EuclideanPlane P] where
   point₁ : P
   point₂ : P
   point₃ : P
@@ -42,7 +42,7 @@ structure Quadrilateral (P : Type _) [EuclideanPlane P] where
 scoped notation "QDR" => Quadrilateral.mk
 
 namespace Quadrilateral
-variable {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P}
+variable {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P}
 
 /-- Given a quadrilateral qdr, qdr.edge₁₂ is the edge from the first point to the second point of a quadrilateral. -/
 @[pp_dot]
@@ -102,7 +102,7 @@ end Quadrilateral
 A quadrilateral is called non-degenerate if the points that adjacent is not same
 -/
 @[pp_dot]
-structure Quadrilateral.IsND {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where
+structure Quadrilateral.IsND {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where
   nd₁₂ : (qdr.2 ≠ qdr.1)
   nd₂₃ : (qdr.3 ≠ qdr.2)
   nd₃₄ : (qdr.4 ≠ qdr.3)
@@ -112,17 +112,17 @@ structure Quadrilateral.IsND {P : Type _} [EuclideanPlane P] (qdr : Quadrilatera
 Class of nd Quadrilateral: A nd quadrilateral is quadrilateral with the property of nd.
 -/
 @[ext]
-structure QuadrilateralND (P : Type _) [EuclideanPlane P] extends Quadrilateral P where
+structure QuadrilateralND (P : Type*) [EuclideanPlane P] extends Quadrilateral P where
   nd : toQuadrilateral.IsND
 
-def QuadrilateralND.mk_pt_pt_pt_pt_nd {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) : QuadrilateralND P where
+def QuadrilateralND.mk_pt_pt_pt_pt_nd {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) : QuadrilateralND P where
   toQuadrilateral := (QDR A B C D)
   nd := h
 
 scoped notation "QDR_nd" => QuadrilateralND.mk_pt_pt_pt_pt_nd
 
 /-- Given a property that a quadrilateral qdr is nd, this function returns qdr itself as an object in the class of nd quadrilateral -/
-def QuadrilateralND.mk_nd {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsND) : QuadrilateralND P where
+def QuadrilateralND.mk_nd {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsND) : QuadrilateralND P where
   toQuadrilateral := qdr
   nd := h
 
@@ -130,7 +130,7 @@ scoped notation "QDR_nd'" => QuadrilateralND.mk_nd
 
 /-- A quadrilateral satisfies InGPos if every 3 vertices are not collinear. -/
 @[pp_dot]
-structure Quadrilateral.InGPos {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where
+structure Quadrilateral.InGPos {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where
   not_collinear₁₂₃: ( ¬ Collinear qdr.point₁ qdr.point₂ qdr.point₃)
   not_collinear₂₃₄: ( ¬ Collinear qdr.point₂ qdr.point₃ qdr.point₄)
   not_collinear₃₄₁: ( ¬ Collinear qdr.point₃ qdr.point₄ qdr.point₁)
@@ -143,7 +143,7 @@ namespace QuadrilateralND
 section property_nd
 -- properties of nd quadrilateral `to be added`
 
-variable {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P)
+variable {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P)
 
 /-- The edge from the first point to the second point of a QuadrilateralND is non-degenerate. -/
 instance nd₁₂ : PtNe qdr_nd.1.2 qdr_nd.1.1 := Fact.mk qdr_nd.nd.nd₁₂
@@ -253,14 +253,14 @@ theorem flip_angle₄_value_eq_neg_angle₂ : qdr_nd.flip.angle₄.value = - qdr
 end property_nd
 
 /-- A Quadrilateral which satisfies InGPos satisfies IsND. -/
-theorem nd_of_gpos {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (InGPos : qdr.InGPos): qdr.IsND:= by
+theorem nd_of_gpos {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (InGPos : qdr.InGPos): qdr.IsND:= by
   constructor
   · exact (ne_of_not_collinear InGPos.not_collinear₁₂₃).right.right
   · exact (ne_of_not_collinear InGPos.not_collinear₂₃₄).right.right
   · exact (ne_of_not_collinear InGPos.not_collinear₃₄₁).right.right
   · exact (ne_of_not_collinear InGPos.not_collinear₄₁₂).right.right.symm
 
-instance {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.InGPos qdr.IsND := {coe := nd_of_gpos}
+instance {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.InGPos qdr.IsND := {coe := nd_of_gpos}
 
 end QuadrilateralND
 
@@ -268,16 +268,16 @@ end QuadrilateralND
 A Quadrilateral is called convex if it's ND and four angles have the same sign.
 -/
 -- @[pp_dot]
--- def QuadrilateralND.IsConvex {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg)
+-- def QuadrilateralND.IsConvex {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg)
 
 -- @[pp_dot]
--- def Quadrilateral.IsConvex {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
+-- def Quadrilateral.IsConvex {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
 --   by_cases h : qdr.IsND
 --   · exact (QuadrilateralND.mk_nd h).IsConvex
 --   · exact False
 
 @[pp_dot]
-def Quadrilateral.IsConvex {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
+def Quadrilateral.IsConvex {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
   by_cases h : qdr.IsND
   · have qdr_nd : QuadrilateralND P := QDR_nd' h
     exact (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg)
@@ -285,51 +285,51 @@ def Quadrilateral.IsConvex {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral
 
 scoped postfix : 50 "IsConvex" => Quadrilateral.IsConvex
 
-theorem Quadrilateral.isND_of_is_convex {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : qdr.IsND := by
+theorem Quadrilateral.isND_of_is_convex {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : qdr.IsND := by
   by_contra g
   unfold Quadrilateral.IsConvex at h
   simp only [g, dite_false] at h
 
-instance {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.IsConvex qdr.IsND := {coe := Quadrilateral.isND_of_is_convex}
+instance {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.IsConvex qdr.IsND := {coe := Quadrilateral.isND_of_is_convex}
 
--- theorem QuadrilateralND.toqdr_cvx_of_cvx {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : qdr_nd.toQuadrilateral.IsConvex := by
+-- theorem QuadrilateralND.toqdr_cvx_of_cvx {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : qdr_nd.toQuadrilateral.IsConvex := by
 --   have k : qdr_nd.toQuadrilateral.IsND := qdr_nd.nd
 --   have l : qdr_nd = (QDR_nd' k) := rfl
 --   rw [l] at h
 --   unfold Quadrilateral.IsConvex
 --   simp only [k, h, dite_eq_ite, ite_true]
 
--- instance {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := QuadrilateralND.toqdr_cvx_of_cvx}
+-- instance {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := QuadrilateralND.toqdr_cvx_of_cvx}
 
-theorem Quadrilateral.nd_cvx_iff_cvx {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) := by
+theorem Quadrilateral.nd_cvx_iff_cvx {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) := by
   unfold Quadrilateral.IsConvex
   have nd : qdr_nd.toQuadrilateral.IsND := qdr_nd.nd
   simp only [nd, dite_true]
   rfl
 
-theorem Quadrilateral_cvx.nd_is_convex_iff_is_convex {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.toQuadrilateral.IsConvex := by
+theorem Quadrilateral_cvx.nd_is_convex_iff_is_convex {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.toQuadrilateral.IsConvex := by
   unfold Quadrilateral.IsConvex
   simp only [qdr_nd.nd, dite_true]
 
-instance {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mp}
+instance {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mp}
 
-instance {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.toQuadrilateral.IsConvex qdr_nd.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mpr}
+instance {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.toQuadrilateral.IsConvex qdr_nd.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mpr}
 
 /--
 Class of Convex Quadrilateral: A convex quadrilateral is quadrilateral with the property of convex.
 -/
 @[ext]
-structure Quadrilateral_cvx (P : Type _) [EuclideanPlane P] extends QuadrilateralND P where
+structure Quadrilateral_cvx (P : Type*) [EuclideanPlane P] extends QuadrilateralND P where
   convex : toQuadrilateral.IsConvex
 
-def Quadrilateral_cvx.mk_pt_pt_pt_pt_convex {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P where
+def Quadrilateral_cvx.mk_pt_pt_pt_pt_convex {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P where
   toQuadrilateral := (QDR A B C D)
   nd := h
   convex := h
 
 scoped notation "QDR_cvx" => Quadrilateral_cvx.mk_pt_pt_pt_pt_convex
 
-def Quadrilateral_cvx.mk_cvx {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : Quadrilateral_cvx P where
+def Quadrilateral_cvx.mk_cvx {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : Quadrilateral_cvx P where
   toQuadrilateralND := QDR_nd' h
   convex := h
 
@@ -337,15 +337,15 @@ scoped notation "QDR_cvx'" => Quadrilateral_cvx.mk_cvx
 
 namespace Quadrilateral_cvx
 
--- def mk_is_convex {P : Type _} [EuclideanPlane P] {A B C D : P} (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P := mk_pt_pt_pt_pt_convex A B C D h
+-- def mk_is_convex {P : Type*} [EuclideanPlane P] {A B C D : P} (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P := mk_pt_pt_pt_pt_convex A B C D h
 
 -- /-- Given a property that a quadrilateral qdr is convex, this function returns qdr itself as an object in the class of convex quadrilateral-/
--- def mk_nd_is_convex {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : Quadrilateral_cvx P where
+-- def mk_nd_is_convex {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : Quadrilateral_cvx P where
 --   toQuadrilateralND := qdr_nd
 --   convex := h
 
 section criteria_cvx
-variable {P : Type _} [EuclideanPlane P] {A B C D : P}
+variable {P : Type*} [EuclideanPlane P] {A B C D : P}
 
 structure is_convex_of_three_sides_of_same_side' where
   qdr_nd : QuadrilateralND P
@@ -389,7 +389,7 @@ end criteria_cvx
 section property_cvx
 -- properties of convex quadrilateral `to be added`
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 variable (qdr : Quadrilateral P)
 variable (qdr_nd : QuadrilateralND P)
 variable (qdr_cvx : Quadrilateral_cvx P)
@@ -573,7 +573,7 @@ end Quadrilateral_cvx
 section criteria
 -- the criteria of a quadrilateral being convex `to be added`
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 end criteria
 
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean
index 7e197a8e8..7f4909710 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean
@@ -7,6 +7,6 @@ noncomputable section
 namespace EuclidGeom
 
 @[ext]
-structure Rectangle (P : Type _) [EuclideanPlane P] extends Parallelogram P where
+structure Rectangle (P : Type*) [EuclideanPlane P] extends Parallelogram P where
 
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean
index 771543700..1019c15b4 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean
@@ -7,6 +7,6 @@ noncomputable section
 namespace EuclidGeom
 
 @[ext]
-structure Rhombus (P : Type _) [EuclideanPlane P] extends Parallelogram P where
+structure Rhombus (P : Type*) [EuclideanPlane P] extends Parallelogram P where
 
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean
index 5f77f8a8f..6041b074c 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean
@@ -8,6 +8,6 @@ noncomputable section
 namespace EuclidGeom
 
 @[ext]
-structure Square (P : Type _) [EuclideanPlane P] extends Rhombus P, Rectangle P
+structure Square (P : Type*) [EuclideanPlane P] extends Rhombus P, Rectangle P
 
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean
index 18037cf42..50bb5529e 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean
@@ -7,6 +7,6 @@ noncomputable section
 namespace EuclidGeom
 
 @[ext]
-structure Trapezoid (P : Type _) [EuclideanPlane P] extends Quadrilateral_cvx P where
+structure Trapezoid (P : Type*) [EuclideanPlane P] extends Quadrilateral_cvx P where
 
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean b/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean
index 544ec0065..117407da4 100644
--- a/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean
+++ b/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean
@@ -14,7 +14,7 @@ namespace EuclidGeom
 
 open AngValue Angle
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 -- Feel free to change the name of the theorems and comments into better ones, or add sections to better organize theorems.
 -- `Currently, the theorems are not well-organized, please follow the plan file to write and add theorems in this file into the plan file if they are not already in the plan`
diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean b/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean
index 58801fa23..85619ccc3 100644
--- a/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean
+++ b/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean
@@ -6,7 +6,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 def TriangleND.Median1 (tr_nd : TriangleND P) : SegND P := sorry
 
diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean b/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean
index f04b18f3b..846da6934 100644
--- a/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean
+++ b/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean
@@ -6,7 +6,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 def TriangleND.Height1 (tr_nd : TriangleND P) : SegND P := sorry
 
diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean b/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean
index a98caa2ef..27238406e 100644
--- a/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean
+++ b/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean
@@ -8,7 +8,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.Basic
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 structure IsPerpBis (seg_nd : SegND P) (line : Line P) : Prop where
 
diff --git a/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean b/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean
index 4f2cedaaf..4c092a989 100644
--- a/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean
+++ b/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean
@@ -4,7 +4,7 @@ namespace EuclidGeom
 
 open Lean Lean.Meta Lean.Elab Lean.Elab.Tactic Qq
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 def extractCollinear (expr : Q(Prop)) : MetaM (Option Expr) :=
   match expr with
diff --git a/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean b/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean
index d7eb079d5..8da84e155 100644
--- a/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean
+++ b/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean
@@ -113,7 +113,7 @@ end acongr
 
 section examples
 
-variable {P : Type _} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P}
+variable {P : Type*} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P}
 
 example (a₁ : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length)
   (e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length) : tr_nd₁.IsCongr tr_nd₂ := by
diff --git a/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean b/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean
index a01acc1e6..442070568 100644
--- a/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean
+++ b/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean
@@ -7,7 +7,7 @@ namespace EuclidGeom
 
 /- congruences of triangles, separate definitions for reversing orientation or not, (requiring all sides and angles being the same)-/
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 
 
diff --git a/EuclideanGeometry/Unused/Class_old.lean b/EuclideanGeometry/Unused/Class_old.lean
index b31ce66fe..3be0bb434 100644
--- a/EuclideanGeometry/Unused/Class_old.lean
+++ b/EuclideanGeometry/Unused/Class_old.lean
@@ -5,24 +5,24 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Plane
 noncomputable section
 namespace EuclidGeom
 
--- class PlaneFigure (P: Type _) [EuclideanPlane P] (α : Type _) where
+-- class PlaneFigure (P: Type*) [EuclideanPlane P] (α : Type*) where
 
-class Carrier (P: Type _) [EuclideanPlane P] (α : Type _) where
+class Carrier (P: Type*) [EuclideanPlane P] (α : Type*) where
   carrier : α → Set P
 
-class Interior (P: Type _) [EuclideanPlane P] (α : Type _) where
+class Interior (P: Type*) [EuclideanPlane P] (α : Type*) where
   interior : α → Set P
 
 
-def lies_on {P : Type _} [EuclideanPlane P] {α : Type _} [Carrier P α] (A : P) (F : α) := A ∈ (Carrier.carrier F)
+def lies_on {P : Type*} [EuclideanPlane P] {α : Type*} [Carrier P α] (A : P) (F : α) := A ∈ (Carrier.carrier F)
 
-def lies_int {P : Type _} [EuclideanPlane P] {α : Type _} [Interior P α] (A : P) (F : α) := A ∈ (Interior.interior F)
+def lies_int {P : Type*} [EuclideanPlane P] {α : Type*} [Interior P α] (A : P) (F : α) := A ∈ (Interior.interior F)
 
--- def lies_in {P : Type _} [EuclideanPlane P] {α : Type _} [Carrier P α] [Interior P α] (A : P) (F : α) : Prop := lies_int A F ∨ lies_on A F
+-- def lies_in {P : Type*} [EuclideanPlane P] {α : Type*} [Carrier P α] [Interior P α] (A : P) (F : α) : Prop := lies_int A F ∨ lies_on A F
 
-def is_inx {P : Type _} [EuclideanPlane P] {α β: Type _} [Carrier P α] [Carrier P β] (A : P) (F : α) (G : β) := A ∈ (Carrier.carrier F) ∧ A ∈ (Carrier.carrier G)
+def is_inx {P : Type*} [EuclideanPlane P] {α β: Type*} [Carrier P α] [Carrier P β] (A : P) (F : α) (G : β) := A ∈ (Carrier.carrier F) ∧ A ∈ (Carrier.carrier G)
 
-theorem is_inx.symm {P : Type _} [EuclideanPlane P] {α β: Type _} [Carrier P α] [Carrier P β] {A : P} {F : α} {G : β} (h : is_inx A F G) : is_inx A G F := And.symm h
+theorem is_inx.symm {P : Type*} [EuclideanPlane P] {α β: Type*} [Carrier P α] [Carrier P β] {A : P} {F : α} {G : β} (h : is_inx A F G) : is_inx A G F := And.symm h
 
 scoped infix : 50 " LiesOn " => lies_on
 scoped infix : 50 " LiesInt " => lies_int
@@ -31,21 +31,21 @@ scoped infix : 50 " LiesInt " => lies_int
 
 section compatibility
 
-theorem ne_of_lieson_and_not_lieson {P : Type _} [EuclideanPlane P] {α : Type _} [Carrier P α] {F : α} {X Y : P} (hx : X LiesOn F) (hy : ¬ Y LiesOn F) : X ≠ Y := by
+theorem ne_of_lieson_and_not_lieson {P : Type*} [EuclideanPlane P] {α : Type*} [Carrier P α] {F : α} {X Y : P} (hx : X LiesOn F) (hy : ¬ Y LiesOn F) : X ≠ Y := by
   by_contra h
   rw [h] at hx
   tauto
 
-theorem ne_of_liesint_and_not_liesint {P : Type _} [EuclideanPlane P] {α : Type _} [Interior P α] {F : α} {X Y : P} (hx : X LiesInt F) (hy : ¬ Y LiesInt F) : X ≠ Y := by
+theorem ne_of_liesint_and_not_liesint {P : Type*} [EuclideanPlane P] {α : Type*} [Interior P α] {F : α} {X Y : P} (hx : X LiesInt F) (hy : ¬ Y LiesInt F) : X ≠ Y := by
   by_contra h
   rw [h] at hx
   tauto
 end compatibility
 
 /- Three figures concurrent at a point -/
-def concurrent {P : Type _} [EuclideanPlane P] {α β γ: Type _} [Carrier P α] [Carrier P β] [Carrier P γ] (A : P) (F : α) (G : β) (H : γ) : Prop := A LiesOn F ∧ A LiesOn G ∧ A LiesOn H
+def concurrent {P : Type*} [EuclideanPlane P] {α β γ: Type*} [Carrier P α] [Carrier P β] [Carrier P γ] (A : P) (F : α) (G : β) (H : γ) : Prop := A LiesOn F ∧ A LiesOn G ∧ A LiesOn H
 
-class Convex2D (P: Type _) [EuclideanPlane P] (α : Type _) extends (Carrier P α), (Interior P α) where
+class Convex2D (P: Type*) [EuclideanPlane P] (α : Type*) extends (Carrier P α), (Interior P α) where
   convexity : ∀ (F : α) (A B : P), (A LiesOn F) → (B LiesOn F) → ∃ (t : ℝ), t • (B -ᵥ A) +ᵥ A LiesOn F
   int_of_carrier : ∀ (F : α) (A : P), (A LiesInt F) → ∃ (B₁ B₂ B₃ : P) (t₁ t₂ t₃ : ℝ), (B₁ LiesOn F) ∧ (B₂ LiesOn F) ∧ (B₃ LiesOn F) ∧ (0 < t₁) ∧ (0 < t₂) ∧ (0 < t₃) ∧ (t₁ • VEC A B₁ + t₂ • VEC A B₂ + t₃ • VEC A B₃ = 0)
 
diff --git a/EuclideanGeometry/Unused/Congruence.lean b/EuclideanGeometry/Unused/Congruence.lean
index af52f3cac..a46c32ea7 100644
--- a/EuclideanGeometry/Unused/Congruence.lean
+++ b/EuclideanGeometry/Unused/Congruence.lean
@@ -13,7 +13,7 @@ namespace EuclidGeom
 
 /- congruences of triangles, separate definitions for reversing orientation or not, (requiring all sides and angles being the same)-/
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 -- only define congrence for TriangleND
 --def IsCongr (tr_nd₁ tr_nd₂: TriangleND P) : Prop := (tr_nd₁.1.edge₁.length = tr_nd₂.1.edge₁.length ∧ tr_nd₁.1.edge₂.length = tr_nd₂.1.edge₂.length ∧ tr_nd₁.1.edge₃.length = tr_nd₂.1.edge₃.length ∧ tr_nd₁.angle₁.value = tr_nd₂.angle₁.value ∧ tr_nd₁.angle₂.value = tr_nd₂.angle₂.value ∧ tr_nd₁.angle₃.value = tr_nd₂.angle₃.value)
 def IsCongr (tr₁ tr₂: Triangle P) : Prop := by
diff --git a/EuclideanGeometry/Unused/Line.lean b/EuclideanGeometry/Unused/Line.lean
index 186216a78..93e0afafb 100644
--- a/EuclideanGeometry/Unused/Line.lean
+++ b/EuclideanGeometry/Unused/Line.lean
@@ -4,7 +4,7 @@ noncomputable section
 namespace EuclidGeom
 
 @[ext]
-class Line (P : Type _) [EuclideanPlane P] where
+class Line (P : Type*) [EuclideanPlane P] where
   carrier : Set P
   linear : ∀ (A B C : P), (A ∈ carrier) → (B ∈ carrier) → (C ∈ carrier) → Collinear A B C
   maximal : ∀ (A B : P), (A ∈ carrier) → (B ∈ carrier) → (B ≠ A) → (∀ (C : P), Collinear A B C → (C ∈ carrier))
@@ -12,7 +12,7 @@ class Line (P : Type _) [EuclideanPlane P] where
 
 namespace Line
 
-variable  {P : Type _} [EuclideanPlane P]
+variable  {P : Type*} [EuclideanPlane P]
 
 -- define a line from two points
 
@@ -71,7 +71,7 @@ scoped notation "LIN" => Line.mk_pt_pt
 
 namespace Line
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 /- Def of point lies on a line, LiesInt is not defined -/
 protected def IsOn (a : P) (l : Line P) : Prop :=
@@ -83,7 +83,7 @@ instance : Carrier P (Line P) where
 end Line
 
 -- Now we introduce useful theorems to avoid using more unfolds in further proofs.
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section Compaitiblity_of_coercions_of_mk_pt_pt
 
diff --git a/EuclideanGeometry/Unused/Parallel.lean b/EuclideanGeometry/Unused/Parallel.lean
index 70a113509..b8e39c674 100644
--- a/EuclideanGeometry/Unused/Parallel.lean
+++ b/EuclideanGeometry/Unused/Parallel.lean
@@ -3,14 +3,14 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Line
 noncomputable section
 namespace EuclidGeom
 
-inductive LinearObj (P : Type _) [EuclideanPlane P] where
+inductive LinearObj (P : Type*) [EuclideanPlane P] where
   | vec_nd (v : VecND)
   | dir (v : Dir)
   | ray (r : Ray P)
   | seg_nd (s : SegND P)
   | line (l : Line P)
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 section coercion
 
@@ -61,9 +61,9 @@ scoped infix : 50 " LiesOnarObj " => LinearObj.IsOnLinearObj
 
 -- Our definition of parallel for LinearObj is very general. Not only can it apply to different types of Objs, but also include degenerate cases, such as ⊆(inclusions), =(equal).
 
-def Parallel' {α β: Type _} (l₁ : α) (l₂ : β) [Coe α (LinearObj P)] [Coe β (LinearObj P)] : Prop :=  LinearObj.toProj (P := P) (Coe.coe l₁) = LinearObj.toProj (P := P) (Coe.coe l₂)
+def Parallel' {α β: Type*} (l₁ : α) (l₂ : β) [Coe α (LinearObj P)] [Coe β (LinearObj P)] : Prop :=  LinearObj.toProj (P := P) (Coe.coe l₁) = LinearObj.toProj (P := P) (Coe.coe l₂)
 
--- class PlaneFigure' (P : Type _) [EuclideanPlane P] {α : Type _} where
+-- class PlaneFigure' (P : Type*) [EuclideanPlane P] {α : Type*} where
 
 -- instance : PlaneFigure' P (LinearObj P) where
 
diff --git a/EuclideanGeometry/Unused/Parallelogram.lean b/EuclideanGeometry/Unused/Parallelogram.lean
index 319900a3c..9252bcfef 100644
--- a/EuclideanGeometry/Unused/Parallelogram.lean
+++ b/EuclideanGeometry/Unused/Parallelogram.lean
@@ -6,14 +6,14 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Quadrilateral
 noncomputable section
 namespace EuclidGeom
 
-class Parallelogram (P : Type _) [EuclideanPlane P] extends Quadrilateral_cvx P where
+class Parallelogram (P : Type*) [EuclideanPlane P] extends Quadrilateral_cvx P where
   para : LinearObj.seg_nd toQuadrilateral_cvx.edgeND₁₂ ∥ toQuadrilateral_cvx.edgeND₃₄
   para' : LinearObj.seg_nd toQuadrilateral_cvx.edgeND₂₃ ∥ toQuadrilateral_cvx.edgeND₄₁
 
 /-
 section make
 namespace Parallelogram
-/- 
+/-
 construct parallelgram from (protected def)
 1. a point and 2 VecND that is not parallel
 2. 3 point that is not collinear
@@ -23,19 +23,19 @@ end Parallelogram
 end make
 -/
 
-def Quadrilateral_cvx.is_parallelogram {P : Type _} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) : Prop := (LinearObj.seg_nd qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄) ∧ (LinearObj.seg_nd qdr_cvx.edgeND₂₃ ∥ qdr_cvx.edgeND₄₁)
+def Quadrilateral_cvx.is_parallelogram {P : Type*} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) : Prop := (LinearObj.seg_nd qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄) ∧ (LinearObj.seg_nd qdr_cvx.edgeND₂₃ ∥ qdr_cvx.edgeND₄₁)
 
-def Quadrilateral.is_parallelogram {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
-  by_cases qdr.IsConvex 
+def Quadrilateral.is_parallelogram {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by
+  by_cases qdr.IsConvex
   · exact (Quadrilateral_cvx.mk_is_convex h).is_parallelogram
-  · exact False 
+  · exact False
 
 theorem Parallelogram.is_parallelgram : sorry := sorry
 
-def Parallelogram.mk_is_parallelgram {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.is_parallelogram) : Parallelogram P := sorry
+def Parallelogram.mk_is_parallelgram {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.is_parallelogram) : Parallelogram P := sorry
 
 section criteria
-/- 
+/-
 
 -/
 
@@ -48,7 +48,7 @@ end property
 end EuclidGeom
 
   /-
-  nd₁₃ : point₃ ≠ point₁ 
+  nd₁₃ : point₃ ≠ point₁
   nd₂₄ : point₄ ≠ point₂
   diag_not_para : ¬ SEG_nd point₂ point₄ nd₂₄ ∥ (LinearObj.seg_nd (SEG_nd point₁ point₃ nd₁₃))
   diag_intx : Line.inx (SEG_nd point₁ point₃ nd₁₃).toLine (SEG_nd point₂ point₄ nd₂₄).toLine diag_not_para LiesInt (SEG point₁ point₃) ∧ Line.inx (SEG_nd point₁ point₃ nd₁₃).toLine (SEG_nd point₂ point₄ nd₂₄).toLine diag_not_para LiesInt (SEG point₂ point₄)
diff --git a/EuclideanGeometry/Unused/Tactic.Congruence.lean b/EuclideanGeometry/Unused/Tactic.Congruence.lean
index 293416911..4cb1204f9 100644
--- a/EuclideanGeometry/Unused/Tactic.Congruence.lean
+++ b/EuclideanGeometry/Unused/Tactic.Congruence.lean
@@ -59,7 +59,7 @@ def evalCongrSa : Tactic := fun stx =>
       logInfo "`congr_sa` doesn't close any goals"
   | _ => throwUnsupportedSyntax
 
-example {P : Type _} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P}
+example {P : Type*} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P}
   (e₂ : tr_nd₁.1.edge₂.length = tr_nd₂.1.edge₂.length)
   (a₁ : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value)
   (e₃ : tr_nd₁.1.edge₃.length = tr_nd₂.1.edge₃.length)
diff --git a/EuclideanGeometry/Unused/Unused.lean b/EuclideanGeometry/Unused/Unused.lean
index 97a83b27e..79376a0d7 100644
--- a/EuclideanGeometry/Unused/Unused.lean
+++ b/EuclideanGeometry/Unused/Unused.lean
@@ -8,12 +8,12 @@ namespace EuclidGeom
 /- Another way of defining 2DVecSpace before define EuclideanPlane，-/
 section Cartesian2dVectorSpace
 /- -/
-class Cartesian2dVectorSpace (V : Type _)  extends  NormedAddCommGroup V, InnerProductSpace ℝ V where
+class Cartesian2dVectorSpace (V : Type*)  extends  NormedAddCommGroup V, InnerProductSpace ℝ V where
   dim_two : FiniteDimensional.finrank ℝ V = 2
   basis : Basis (Fin 2) ℝ V
   orthonormal : Orthonormal ℝ basis
 
-variable {V : Type _} [h : Cartesian2dVectorSpace V]
+variable {V : Type*} [h : Cartesian2dVectorSpace V]
 
 def x_coordinate (v : V) := (Basis.coord h.basis 0).toFun v
 
@@ -85,7 +85,7 @@ end Pythagoras
 
 section Pythagoras
 
-theorem Pythagoras_of_ne_ne_perp' (P : Type _) [EuclideanPlane P] {A B C : P} (hab : B ≠ A) (hac : C ≠ A) (h : (SegND.toProj ⟨SEG A B, hab⟩).perp = (SegND.toProj ⟨SEG A C, hac⟩)) : (SEG A B).length ^ 2 + (SEG A C).length ^ 2 = (SEG B C).length ^ 2 := by
+theorem Pythagoras_of_ne_ne_perp' (P : Type*) [EuclideanPlane P] {A B C : P} (hab : B ≠ A) (hac : C ≠ A) (h : (SegND.toProj ⟨SEG A B, hab⟩).perp = (SegND.toProj ⟨SEG A C, hac⟩)) : (SEG A B).length ^ 2 + (SEG A C).length ^ 2 = (SEG B C).length ^ 2 := by
   have i : Vec.InnerProductSpace.Core.inner (VEC A B) (VEC A C) = 0 := inner_eq_zero_of_toProj_perp_eq_toProj (SegND.toVecND ⟨SEG A B, hab⟩) (SegND.toVecND ⟨SEG A C, hac⟩) h
   rw [Seg.length_sq_eq_inner_toVec_toVec (SEG A B), Seg.length_sq_eq_inner_toVec_toVec (SEG A C), Seg.length_sq_eq_inner_toVec_toVec (SEG B C)]
   simp only [seg_toVec_eq_vec]
@@ -97,7 +97,7 @@ theorem Pythagoras_of_ne_ne_perp' (P : Type _) [EuclideanPlane P] {A B C : P} (h
   rw [← zero_add ((VEC A B).fst * (VEC A B).fst), ← zero_add ((VEC A B).fst * (VEC A B).fst), ← neg_zero, ← i]
   ring
 
-theorem Pythagoras_of_perp_foot' (P : Type _) [EuclideanPlane P] (A B : P) {l : Line P} (h : B LiesOn l) : (SEG A (perp_foot A l)).length ^ 2 + (SEG B (perp_foot A l)).length ^ 2 = (SEG A B).length ^ 2 := by
+theorem Pythagoras_of_perp_foot' (P : Type*) [EuclideanPlane P] (A B : P) {l : Line P} (h : B LiesOn l) : (SEG A (perp_foot A l)).length ^ 2 + (SEG B (perp_foot A l)).length ^ 2 = (SEG A B).length ^ 2 := by
   sorry
 
 end Pythagoras
@@ -106,23 +106,23 @@ end Pythagoras
 /- unused sketch of undirected lines, segments-/
 section undirected
 
-class Line' (P : Type _) [EuclideanPlane P] where
+class Line' (P : Type*) [EuclideanPlane P] where
 -- What is a line??? to be affine subspaces of dimension 1, citing affine vector spaces?
 -- carrier : Set P
 -- linearity
 
-class GSeg' (P : Type _) [EuclideanPlane P] where
+class GSeg' (P : Type*) [EuclideanPlane P] where
 -- a multiset of 2 points? or just never mention this?
 
-class Seg' (P : Type _) [EuclideanPlane P] where
+class Seg' (P : Type*) [EuclideanPlane P] where
 -- a multiset of 2 diff points? or just never mention this?
 -- carrier
 
-def IsOnLine' {P : Type _} [EuclideanPlane P] (a : P) (l : Line' P) : Prop := sorry
+def IsOnLine' {P : Type*} [EuclideanPlane P] (a : P) (l : Line' P) : Prop := sorry
 
 infixl : 50 "LiesOn" => IsOnLine'
 
-instance {P : Type _} [EuclideanPlane P] : Coe (Ray P) (Line' P) where
+instance {P : Type*} [EuclideanPlane P] : Coe (Ray P) (Line' P) where
   coe := sorry
 
 end undirected
@@ -131,19 +131,19 @@ section angle
 namespace Angle
 open Classical
 
-noncomputable def angle_of_three_points' {P : Type _} [h : EuclideanPlane P] (A O B : P) : ℝ := if ((A = O) ∨ (B = O)) then 0 else AngValue.toReal (value (mk_pt_pt_pt A O B sorry sorry))
+noncomputable def angle_of_three_points' {P : Type*} [h : EuclideanPlane P] (A O B : P) : ℝ := if ((A = O) ∨ (B = O)) then 0 else AngValue.toReal (value (mk_pt_pt_pt A O B sorry sorry))
 end Angle
 end angle
 
 section nondeg
 
 /- Directed segment -/
-class DSeg (P : Type _) [EuclideanPlane P] extends Ray P, Seg P where
+class DSeg (P : Type*) [EuclideanPlane P] extends Ray P, Seg P where
   on_ray : IsOnRay target toRay
   non_triv : target ≠ source
 
 /- Define a point lies on an oriented segment, a line, a segment, immediate consequences -/
-def IsOnDSeg {P : Type _} [EuclideanPlane P] (a : P) (l : DSeg P) : Prop :=
+def IsOnDSeg {P : Type*} [EuclideanPlane P] (a : P) (l : DSeg P) : Prop :=
   ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ a = t • (l.target -ᵥ l.source) +ᵥ l.source
 
 end nondeg
@@ -152,12 +152,12 @@ scoped infix : 50 " LiesOnDSeg " => IsOnDSeg
 
 section nondeg
 
-instance {P : Type _} [EuclideanPlane P] : Coe (DSeg P) (Seg P) where
+instance {P : Type*} [EuclideanPlane P] : Coe (DSeg P) (Seg P) where
   coe := fun _ => DSeg.toSeg
 
 /- def of DirSeg from GDirSeg if length ≠ 0 -/
 
--- def Seg.toDSeg_of_nontriv {P : Type _} [EuclideanPlane P] (l : Seg P) (nontriv : l.target ≠ l.source): DSeg P where
+-- def Seg.toDSeg_of_nontriv {P : Type*} [EuclideanPlane P] (l : Seg P) (nontriv : l.target ≠ l.source): DSeg P where
 --   source := l.source
 --   target := l.target
 --   toDir := Vec.toDir (l.target -ᵥ l.source) (vsub_ne_zero.mpr nontriv)
@@ -166,16 +166,16 @@ instance {P : Type _} [EuclideanPlane P] : Coe (DSeg P) (Seg P) where
 
 -- theorems "if p LiesOnDSeg l, then p LiesOn l.toRay and p LiesOn l.toSeg"
 
--- theorem DSeg.pt_on_toRay_of_pt_on_DSeg {P : Type _} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toRay := sorry
+-- theorem DSeg.pt_on_toRay_of_pt_on_DSeg {P : Type*} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toRay := sorry
 
-theorem DSeg.pt_on_toseg_of_pt_on_DSeg {P : Type _} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toSeg := sorry
+theorem DSeg.pt_on_toseg_of_pt_on_DSeg {P : Type*} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toSeg := sorry
 
 -- mk method of DirSeg giving 2 distinct point
-def DSeg.mk_pt_pt {P : Type _} [EuclideanPlane P] (A B : P) (h : B ≠ A) : DSeg P := sorry
+def DSeg.mk_pt_pt {P : Type*} [EuclideanPlane P] (A B : P) (h : B ≠ A) : DSeg P := sorry
 
 namespace DSeg
 
-variable {P: Type _} [EuclideanPlane P] (seg : DSeg P) (gseg : Seg P)
+variable {P: Type*} [EuclideanPlane P] (seg : DSeg P) (gseg : Seg P)
 
 -- source and targets are on generalized directed segments
 theorem source_lies_on_seg : seg.source LiesOnDSeg seg := by sorry
@@ -202,7 +202,7 @@ theorem DSeg.rev_toseg_eq_toseg_rev : seg.reverse.toSeg = (seg.toSeg).reverse :=
 
 -- theorem Seg.rev_toDSeg_eq_toDSeg_rev (nontriv : gseg.target ≠ gseg.source) : (gseg.reverse).toDSeg_of_nontriv (Seg.nontriv_of_rev_of_nontriv gseg nontriv) = (gseg.toDSeg_of_nontriv nontriv).reverse := sorry
 
-variable {P: Type _} [EuclideanPlane P] (v : ℝ × ℝ) (seg : DSeg P)
+variable {P: Type*} [EuclideanPlane P] (v : ℝ × ℝ) (seg : DSeg P)
 
 -- parallel translate a directed segments
 
@@ -220,7 +220,7 @@ end nondeg
 
 
 section pos_neg_ray
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 def IsOnPosSide (A : P) (ray : Ray P) : Prop := by
   by_cases A = ray.source
@@ -246,7 +246,7 @@ open Classical
 
 /- Class of generalized triangles -/
 /-
-class Triangle' (P : Type _) [EuclideanPlane P] where
+class Triangle' (P : Type*) [EuclideanPlane P] where
   point₁ : P
   point₂ : P
   point₃ : P
@@ -254,7 +254,7 @@ class Triangle' (P : Type _) [EuclideanPlane P] where
 
 namespace Triangle
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 def nontriv₁ (tr : Triangle P) := (ne_of_not_collinear tr.nontriv).1
 
@@ -288,7 +288,7 @@ end nondeg_tri
 
 section Collinear
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 theorem collinear_ACB_of_collinear_ABC {A B C : P} (h : Collinear A B C): Collinear A C B := sorry
 
@@ -304,11 +304,11 @@ end Collinear
 /-!
 section HasFallsOn
 
-class HasFallsOn (α β : Type _) [HasLiesOn P α] [HasLiesOn P β] where
+class HasFallsOn (α β : Type*) [HasLiesOn P α] [HasLiesOn P β] where
   falls_on : α → β → Prop
   lies_on_falls_on : ∀ (p : P) (A : α) (B : β), HasLiesOn.lies_on p A → falls_on A B → HasLiesOn.lies_on p B
 
-class HasFallsIn (α β : Type _) [HasLiesIn P α] [HasLiesIn P β] where
+class HasFallsIn (α β : Type*) [HasLiesIn P α] [HasLiesIn P β] where
   falls_in : α → β → Prop
   lies_in_falls_in : ∀ (p : P) (A : α) (B : β), HasLiesIn.lies_in p A → falls_in A B → HasLiesIn.lies_in p B
 
@@ -322,9 +322,9 @@ end HasFallsOn
 
 -- scoped notation A "LiesInt" F => HasLiesInt.lies_int A F
 
-def IsFallsOn {α β : Type _} (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] : Prop := ∀ (A : P), (A LiesOn A) → (A LiesOn B)
+def IsFallsOn {α β : Type*} (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] : Prop := ∀ (A : P), (A LiesOn A) → (A LiesOn B)
 
-def IsFallsIn {α β : Type _} (A : α) (B : β) [HasLiesIn P α] [HasLiesIn P β] : Prop := ∀ (A : P), (A LiesIn A) → (A LiesIn B)
+def IsFallsIn {α β : Type*} (A : α) (B : β) [HasLiesIn P α] [HasLiesIn P β] : Prop := ∀ (A : P), (A LiesIn A) → (A LiesIn B)
 
 -- LiesOn → LiesInt is FallsInt ?
 
@@ -333,60 +333,60 @@ scoped notation A "FallsIn" B "Over" P => IsFallsIn P A B
 
 namespace IsFallsOn
 
-protected theorem refl {P : Type _} {α : Type _} (A : α) [HasLiesOn P α] : A FallsOn A Over P := by tauto
+protected theorem refl {P : Type*} {α : Type*} (A : α) [HasLiesOn P α] : A FallsOn A Over P := by tauto
 
-protected theorem trans {P : Type _} {α β γ : Type _} (A : α) (B : β) (C : γ) [HasLiesOn P α] [HasLiesOn P β] [HasLiesOn P γ] : (A FallsOn B Over P) → (B FallsOn C Over P) → (A FallsOn C Over P)   := by tauto
+protected theorem trans {P : Type*} {α β γ : Type*} (A : α) (B : β) (C : γ) [HasLiesOn P α] [HasLiesOn P β] [HasLiesOn P γ] : (A FallsOn B Over P) → (B FallsOn C Over P) → (A FallsOn C Over P)   := by tauto
 
 end IsFallsOn
 
 namespace IsFallsIn
 
-protected theorem refl {P : Type _} {α : Type _} (A : α) [HasLiesIn P α] : A FallsIn A Over P := by tauto
+protected theorem refl {P : Type*} {α : Type*} (A : α) [HasLiesIn P α] : A FallsIn A Over P := by tauto
 
-protected theorem trans {P : Type _} {α β γ : Type _} (A : α) (B : β) (C : γ) [HasLiesIn P α] [HasLiesIn P β] [HasLiesIn P γ] : (A FallsIn B Over P) → (B FallsIn C Over P) → (A FallsIn C Over P)   := by tauto
+protected theorem trans {P : Type*} {α β γ : Type*} (A : α) (B : β) (C : γ) [HasLiesIn P α] [HasLiesIn P β] [HasLiesIn P γ] : (A FallsIn B Over P) → (B FallsIn C Over P) → (A FallsIn C Over P)   := by tauto
 
 end IsFallsIn
 
-def IsIntersectionPoint {P : Type _} {α β : Type _} (A : P) (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] := (A LiesOn A) ∧ (A LiesOn B)
+def IsIntersectionPoint {P : Type*} {α β : Type*} (A : P) (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] := (A LiesOn A) ∧ (A LiesOn B)
 
 scoped notation p "IsIntersectionOf" A B => IsIntersectionPoint p A B
 
 /-
-class HasProj (α : Type _) where
+class HasProj (α : Type*) where
   toProj : (α → Proj)
 
-def Parallel {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := HasProj.toProj A = HasProj.toProj B
+def Parallel {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := HasProj.toProj A = HasProj.toProj B
 
 scoped notation A "IsParallelTo" B => Parallel A B
 scoped notation A "∥" B => Parallel A B
 
 namespace Parallel
 
-protected theorem refl {α : Type _} (A : α) [HasProj α] : A ∥ A := rfl
+protected theorem refl {α : Type*} (A : α) [HasProj α] : A ∥ A := rfl
 
-protected theorem symm {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : (A ∥ B) → (B ∥ A) := Eq.symm
+protected theorem symm {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : (A ∥ B) → (B ∥ A) := Eq.symm
 
-protected theorem trans {α β γ : Type _} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ]: (A ∥ B) → (B ∥ C) → (A ∥ C) := Eq.trans
+protected theorem trans {α β γ : Type*} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ]: (A ∥ B) → (B ∥ C) → (A ∥ C) := Eq.trans
 
 end Parallel
 
-def Perpendicular {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := sorry
+def Perpendicular {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := sorry
 
 scoped notation A "IsPerpendicularTo" B => Perpendicular A B
 scoped notation A "⟂" B => Perpendicular A B
 
 namespace Perpendicular
 
-protected theorem irrefl {α : Type _} (A : α) [HasProj α] : ¬ (A ⟂ A) := by sorry
+protected theorem irrefl {α : Type*} (A : α) [HasProj α] : ¬ (A ⟂ A) := by sorry
 
-protected theorem symm {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : (A ⟂ B) → (B ⟂ A) := sorry
+protected theorem symm {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : (A ⟂ B) → (B ⟂ A) := sorry
 
 end Perpendicular
 
-theorem parallel_of_perp_perp {α β γ : Type _} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ] : (A ⟂ B) → (B ⟂ C) → (A ∥ C)  := sorry
+theorem parallel_of_perp_perp {α β γ : Type*} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ] : (A ⟂ B) → (B ⟂ C) → (A ∥ C)  := sorry
 -/ -/
 
-structure IsAngBis {P : Type _} [EuclideanPlane P] (ang : Angle P) (ray : Ray P) : Prop where intro ::
+structure IsAngBis {P : Type*} [EuclideanPlane P] (ang : Angle P) (ray : Ray P) : Prop where intro ::
   eq_vtx : ang.source = ray.source
   bisect_ang : 2 * (Angle.mk ang.start_ray ray eq_vtx).value = ang.value
 
diff --git a/Plan_files/Memo/AngValue.lean b/Plan_files/Memo/AngValue.lean
index ab115d5eb..8e0a2e706 100644
--- a/Plan_files/Memo/AngValue.lean
+++ b/Plan_files/Memo/AngValue.lean
@@ -32,7 +32,7 @@ Note that `ℝ` is also used for representing the value of an angle (Algeraic Va
 -- The following suggestions may be bad. They are postponed.
 * `Dir` + `DirObj` + `P` to `DirObj` : Rotation of `DirObj`
 * `Proj` + `ProjObj` + `P` to `DirObj` : Rotation of `ProjObj`
-* `Rotation` : the general rotation's type is `{P : Type _} [EuclideanPlane P] (O : P) (dir : Dir) [Figure α] (F : α P) : α P`  `Maybe wrap outside a theorem use AngValue instead of Dir is better?`
+* `Rotation` : the general rotation's type is `{P : Type*} [EuclideanPlane P] (O : P) (dir : Dir) [Figure α] (F : α P) : α P`  `Maybe wrap outside a theorem use AngValue instead of Dir is better?`
 
 ### Detailed Sections
 
diff --git a/Plan_files/Memo/LinearObjects.lean b/Plan_files/Memo/LinearObjects.lean
index ab783dc6b..0edb58e74 100644
--- a/Plan_files/Memo/LinearObjects.lean
+++ b/Plan_files/Memo/LinearObjects.lean
@@ -60,21 +60,21 @@ toDirLine toLine carrier compatibility can be shown in general
 -- Experiments of classes
 
 namespace EuclidGeom
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
-class ProjObj (P : Type _) [EuclideanPlane P] (α : Type _)where
+class ProjObj (P : Type*) [EuclideanPlane P] (α : Type*)where
   toProj : α → Proj
 
 instance : ProjObj P (Line P) where
   toProj := Line.toProj
 
-def to_Proj {P: Type _} [EuclideanPlane P] (l : Line P) : Proj := ProjObj.toProj P l
+def to_Proj {P: Type*} [EuclideanPlane P] (l : Line P) : Proj := ProjObj.toProj P l
 
-def toProj' ⦃P : Type _⦄ {α: Type _} [EuclideanPlane P] [ProjObj P α] (l : α) : Proj := ProjObj.toProj P l
+def toProj' ⦃P : Type*⦄ {α: Type*} [EuclideanPlane P] [ProjObj P α] (l : α) : Proj := ProjObj.toProj P l
 
-example {P : Type _} [EuclideanPlane P] (l : Line P) : l.toProj = to_Proj l := rfl
+example {P : Type*} [EuclideanPlane P] (l : Line P) : l.toProj = to_Proj l := rfl
 
-def to_Line {P : Type _ } {α: Type _} [EuclideanPlane P] ⦃h : ProjObj P α⦄ (l : α) : Line P := sorry
+def to_Line {P : Type* } {α: Type*} [EuclideanPlane P] ⦃h : ProjObj P α⦄ (l : α) : Line P := sorry
 
 variable (l : Line P)
 -- same name enables both writing style without overload
@@ -96,8 +96,8 @@ macro_rules
 #check Seg.carrier
 
 -- This is Plane Figure
-class PlaneFig (F : (P : Type _) -> [ EuclideanPlane P] -> Type _) where
-  carrier : {P : Type _} -> [EuclideanPlane P] -> F P -> Set P
+class PlaneFig (F : (P : Type*) -> [ EuclideanPlane P] -> Type*) where
+  carrier : {P : Type*} -> [EuclideanPlane P] -> F P -> Set P
 
 instance : PlaneFig Seg where
   carrier := Seg.carrier