Type _ -> Type* (#297)

* `Type _` -> `Type*`

* fix

* Revert "fix"

This reverts commit 208bdd1.

* fix

* more

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,15 +64,15 @@ 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)
 #check l.toVec
 
 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
 
 

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
 

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
 

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

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$

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

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.

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.

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$.

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

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$

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.

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
 /-

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
 /-

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
 /-

EuclideanGeometry/Example/ExerciseXT8.lean

@@ -5,7 +5,7 @@ noncomputable section
 
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P]
 
 
 

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$.

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
 /-

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}$.