Merge pull request #287 from negiizhao/collinear

colinear -> collinear

EuclideanGeometry/Check.lean

@@ -90,24 +90,24 @@ theorem let_test_prop (α : Prop) (a : α) (p : α → Prop) : (let x := a; p x)
     intro x
     exact x _
 
-def main_theorem (A B C : P) (h : ¬ colinear A B C) : Prop := by
-  let hAB : B≠A := by exact (ne_of_not_colinear h).2.2
-  let hCB : C ≠ B := by exact (ne_of_not_colinear h).1
+def main_theorem (A B C : P) (h : ¬ collinear A B C) : Prop := by
+  let hAB : B≠A := by exact (ne_of_not_collinear h).2.2
+  let hCB : C ≠ B := by exact (ne_of_not_collinear h).1
   let l₁ := LIN A B hAB
   let l₂ := LIN B C hCB
   let h' : ¬ l₁ ∥ l₂ := sorry
   let E := Line.inx l₁ l₂ h'
   exact (E = B)
 
-example (A B C : P) (h : ¬ colinear A B C) : main_theorem A B C h := by
+example (A B C : P) (h : ¬ collinear A B C) : main_theorem A B C h := by
   unfold main_theorem
-  -- rw [let_test (α := B≠A) (a := (ne_of_not_colinear h).2.2) (p := fun x => let hCB := (_ : C ≠ B);
+  -- rw [let_test (α := B≠A) (a := (ne_of_not_collinear h).2.2) (p := fun x => let hCB := (_ : C ≠ B);
 -- let l₁ := LIN A B x;
 -- let l₂ := LIN B C hCB;
 -- let h' := (_ : ¬LIN A B (_ : B ≠ A)∥LIN B C (_ : C ≠ B));
 -- let E := LineInx l₁ l₂ h';
 -- E = B) ]
-  rw [let_test_prop (B≠A) (ne_of_not_colinear h).2.2 (fun x => let hCB := (_ : C ≠ B);
+  rw [let_test_prop (B≠A) (ne_of_not_collinear h).2.2 (fun x => let hCB := (_ : C ≠ B);
  let l₁ := LIN A B x;
  let l₂ := LIN B C hCB;
  let h' := (_ : ¬LIN A B (_ : B ≠ A)∥LIN B C (_ : C ≠ B));

EuclideanGeometry/Example/AOPS/Chap3.lean

@@ -15,10 +15,10 @@ Theorem: We have $BX = CY$ and $MX = MY$.
 -/
 
 -- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
-variable {A B C : P} {hnd : ¬ colinear A B C} {isoceles_ABC : (▵ A B C).IsIsoceles}
+variable {A B C : P} {hnd : ¬ collinear A B C} {isoceles_ABC : (▵ A B C).IsIsoceles}
 -- Claim: $A \ne B$ and $A \neq C$. This is because vertices of nondegenerate triangles are distinct.
-lemma A_ne_B : A ≠ B := (ne_of_not_colinear hnd).2.2.symm
-lemma A_ne_C : A ≠ C := (ne_of_not_colinear hnd).2.1
+lemma A_ne_B : A ≠ B := (ne_of_not_collinear hnd).2.2.symm
+lemma A_ne_C : A ≠ C := (ne_of_not_collinear hnd).2.1
 -- Let $X$ and $Y$ be points on the interior of the segments of $AC$ and $AB$, respectively.
 variable {X Y : P} {hx : X LiesInt (SEG A C)} {hy : Y LiesInt (SEG A B)}
 -- Claim: $X \neq B$ and $Y \neq C$. This is because: $X$ is an interior point of an edge of a triangle, so it is not equal to a vertex $B$ of the triangle; similarly, $Y$ is an interior point of an edge of a triangle, so it is not equal to a vertex $C$ of the triangle.

EuclideanGeometry/Example/AOPS/Chap5.lean

@@ -12,7 +12,7 @@ namespace AOPS_Problem_5_7
 Prove that $\frac{EY}{EX}=\frac{AD}{DB} -/
 
 --Triangle A B C
-variable {A B C : P} {hnd : ¬ colinear A B C}
+variable {A B C : P} {hnd : ¬ collinear A B C}
 lemma b_ne_a : B ≠ A := sorry
 lemma c_ne_a : C ≠ A := sorry
 lemma c_ne_b : C ≠ B := sorry
@@ -60,7 +60,7 @@ Prove that $IJ\prar BC$-/
 --It is simpler to use vectors but I think we should avoid vectors.
 
 --Nontrivial triangle A B C
-variable {A B C : P} {hnd : ¬ colinear A B C}
+variable {A B C : P} {hnd : ¬ collinear A B C}
 lemma b_ne_a : B ≠ A := sorry
 lemma c_ne_a : C ≠ A := sorry
 lemma c_ne_b : C ≠ B := sorry
@@ -82,7 +82,7 @@ namespace AOPS_Problem_5_14
 Prove that AX^2 = BX \codt CX. -/
 
 -- In right triangle $\triangle PQR$, $\angle QPR = 90^{\circ}$
-variable {A B C : P} {hnd : ¬ colinear A B C}
+variable {A B C : P} {hnd : ¬ collinear A B C}
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
 lemma a_ne_b : A ≠ B := sorry
 lemma b_ne_c : B ≠ C := sorry
@@ -102,7 +102,7 @@ $M$ is the midpoint of $AB$
 Prove that $MQ \parallel BC$ -/
 
 -- We have triangle $\triangle ABC$ with $AC \ne BC$
-variable {A B C : P} {hnd : ¬ colinear A B C} {hne : (SEG A C).length ≠ (SEG B C).length}
+variable {A B C : P} {hnd : ¬ collinear A B C} {hne : (SEG A C).length ≠ (SEG B C).length}
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
 lemma a_ne_b : A ≠ B := sorry
 lemma b_ne_c : B ≠ C := sorry

EuclideanGeometry/Example/AOPS/Chap5a.lean

@@ -18,18 +18,18 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
-  not_colinear_ABC : ¬ colinear A B C
+  not_collinear_ABC : ¬ collinear A B C
   -- Claim :$C \ne A$
   B_ne_A : B ≠ A :=
     -- This is because vertices $B, C$ of a nondegenerate triangle are distinct.
-    (ne_of_not_colinear not_colinear_ABC).2.2
+    (ne_of_not_collinear not_collinear_ABC).2.2
   C_ne_A : C ≠ A :=
     -- This is because vertices $A, C$ of a nondegenerate triangle are distinct.
-    (ne_of_not_colinear not_colinear_ABC).2.1.symm
+    (ne_of_not_collinear not_collinear_ABC).2.1.symm
   -- Claim $B \ne C$
   C_ne_B : C ≠ B :=
     -- This is because vertices $B, C$ of a nondegenerate triangle are distinct.
-    (ne_of_not_colinear not_colinear_ABC).1
+    (ne_of_not_collinear not_collinear_ABC).1
 
   --D lies in AB and E lies in AE
   D : Plane
@@ -86,18 +86,18 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
-  not_colinear_ABC : ¬ colinear A B C
+  not_collinear_ABC : ¬ collinear A B C
   -- Claim :$C \ne A$
   B_ne_A : B ≠ A :=
     -- This is because vertices $B, C$ of a nondegenerate triangle are distinct.
-    (ne_of_not_colinear not_colinear_ABC).2.2
+    (ne_of_not_collinear not_collinear_ABC).2.2
   C_ne_A : C ≠ A :=
     -- This is because vertices $A, C$ of a nondegenerate triangle are distinct.
-    (ne_of_not_colinear not_colinear_ABC).2.1.symm
+    (ne_of_not_collinear not_collinear_ABC).2.1.symm
   -- Claim $B \ne C$
   C_ne_B : C ≠ B :=
     -- This is because vertices $B, C$ of a nondegenerate triangle are distinct.
-    (ne_of_not_colinear not_colinear_ABC).1
+    (ne_of_not_collinear not_collinear_ABC).1
   --E lies on the extension of CA
   E : Plane
   hE₁ : E LiesInt (SEG_nd C A C_ne_A.symm).extension

EuclideanGeometry/Example/ArefWernick/Chap1.lean

@@ -14,7 +14,7 @@ In other words, let $\triangle A_1B_1C_1$ and $\triangle A_2B_2C_2$ be two trian
 Prove that $\triangle A_1B_1C_1$ is congruent to $\triangle A_2B_2C_2$. -/
 
 -- We have two triangles $\triangle A_1B_1C_1,A_2B_2C_2$ .
-variable {A₁ B₁ C₁ A₂ B₂ C₂ : P} {hnd₁ : ¬ colinear A₁ B₁ C₁} {hnd₂ : ¬ colinear A₂ B₂ C₂}
+variable {A₁ B₁ C₁ A₂ B₂ C₂ : P} {hnd₁ : ¬ collinear A₁ B₁ C₁} {hnd₂ : ¬ collinear A₂ B₂ C₂}
 -- $M_1,M_2$ are midpoints of $B_1C_1,B_2,C_2$
 variable {M₁ M₂ : P} {hm₁ : M₁ = (SEG B₁ C₁).midpoint} {hm₂ : M₂ = (SEG B₂ C₂).midpoint}
 -- We have $A_1B_1 = A_2B_2$, $A_1C_1 = A_2C_2$, and $A_1M_1 = A_2M_2$.
@@ -32,12 +32,12 @@ namespace Aref_Wernick_Exercise_1_2
 Prove that $\angle BFD = \pi / 2 - \angle CAB$. -/
 
 -- We have triangle $\triangle ABC$
-variable {A B C : P} {hnd : ¬ colinear A B C}
+variable {A B C : P} {hnd : ¬ collinear A B C}
 -- Claim: $B \ne A$ and $C \ne A$ and $B \ne C$.
 --This is because vertices of nondegenerate triangles are distinct.
-lemma B_ne_a : B ≠ A := (ne_of_not_colinear hnd).2.2
-lemma c_ne_a : C ≠ A := (ne_of_not_colinear hnd).2.1.symm
-lemma B_ne_C : B ≠ C := (ne_of_not_colinear hnd).1.symm
+lemma B_ne_a : B ≠ A := (ne_of_not_collinear hnd).2.2
+lemma c_ne_a : C ≠ A := (ne_of_not_collinear hnd).2.1.symm
+lemma B_ne_C : B ≠ C := (ne_of_not_collinear hnd).1.symm
 -- Let $D$ and $E$ be points lies on the nondegenerate segments of $AB$ and $AC$
 variable{D E : P} {hd : D LiesInt SEG A B} {he : E LiesInt SEG A C}
 -- We have $BD=BC$ and $BC=CE$
@@ -51,17 +51,17 @@ lemma e_ne_B : E ≠ B := sorry
 variable {F : P} {hf : is_inx F (SEG B E) (SEG C D)}
 -- Claim: $B \ne f$ and $D \ne F$.
 lemma B_ne_f : B ≠ F := by
-  have d_not_lies_on_bc : ¬ D LiesOn (LIN B C (ne_of_not_colinear hnd).1) := by
+  have d_not_lies_on_bc : ¬ D LiesOn (LIN B C (ne_of_not_collinear hnd).1) := by
     by_contra not
-    have line_neq : (LIN A B (b_ne_a (hnd := hnd))).toProj ≠ (LIN B C (b_ne_c (hnd := hnd)).symm).toProj := (edge_toLine_not_para_of_not_colinear hnd).1
+    have line_neq : (LIN A B (b_ne_a (hnd := hnd))).toProj ≠ (LIN B C (b_ne_c (hnd := hnd)).symm).toProj := (edge_toLine_not_para_of_not_collinear hnd).1
     have aa : D LiesOn (SegND A B (b_ne_a (hnd := hnd))).1 := Seg.lies_on_of_lies_int hd
-    have inxd : is_inx D (LIN B C (ne_of_not_colinear hnd).1) (LIN A B (ne_of_not_colinear hnd).2.2) := by
+    have inxd : is_inx D (LIN B C (ne_of_not_collinear hnd).1) (LIN A B (ne_of_not_collinear hnd).2.2) := by
       exact ⟨not, SegND.lies_on_toLine_of_lie_on aa⟩
-    have inxb : is_inx B (LIN B C (ne_of_not_colinear hnd).1) (LIN A B (ne_of_not_colinear hnd).2.2) := by
-      exact ⟨(SegND B C (ne_of_not_colinear hnd).1).source_lies_on_toLine , (SegND A B (ne_of_not_colinear hnd).2.2).target_lies_on_toLine ⟩
+    have inxb : is_inx B (LIN B C (ne_of_not_collinear hnd).1) (LIN A B (ne_of_not_collinear hnd).2.2) := by
+      exact ⟨(SegND B C (ne_of_not_collinear hnd).1).source_lies_on_toLine , (SegND A B (ne_of_not_collinear hnd).2.2).target_lies_on_toLine ⟩
     exact d_ne_b (unique_of_inx_of_line_of_not_para line_neq inxb.symm inxd.symm)
-  have bcd_notcoli : ¬ colinear B C D := (Line.lies_on_line_of_pt_pt_iff_colinear (b_ne_c (hnd := hnd)).symm D).mpr.mt d_not_lies_on_bc
-  have b_not_lies_on_cd : ¬ B LiesOn (LIN C D d_ne_c) := (Line.lies_on_line_of_pt_pt_iff_colinear d_ne_c B).mp.mt (flip_colinear_snd_trd.mt (flip_colinear_fst_snd.mt bcd_notcoli))
+  have bcd_notcoli : ¬ collinear B C D := (Line.lies_on_line_of_pt_pt_iff_collinear (b_ne_c (hnd := hnd)).symm D).mpr.mt d_not_lies_on_bc
+  have b_not_lies_on_cd : ¬ B LiesOn (LIN C D d_ne_c) := (Line.lies_on_line_of_pt_pt_iff_collinear d_ne_c B).mp.mt (flip_collinear_snd_trd.mt (flip_collinear_fst_snd.mt bcd_notcoli))
   have f_lies_on_seg_cd : F LiesOn (SegND C D d_ne_c).1 := hf.2
   exact (ne_of_lieson_and_not_lieson (SegND.lies_on_toLine_of_lie_on f_lies_on_seg_cd) b_not_lies_on_cd).symm
 lemma d_ne_f : D ≠ F := sorry

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean

@@ -24,8 +24,8 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   -- $A, E$ do not lie on $l$.
   A : Plane
   E : Plane
-  ABC_nd : ¬colinear A B C
-  EDF_nd : ¬colinear E D F
+  ABC_nd : ¬collinear A B C
+  EDF_nd : ¬collinear E D F
   -- need A and E be at the same side of l!!
   A_side : IsOnLeftSide A (SEG_nd B F)
   E_side : IsOnLeftSide E (SEG_nd B F)
@@ -34,18 +34,18 @@ 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}: ¬ colinear e.B e.A e.C := by
-  apply flip_colinear_fst_snd.mt
+lemma hnd₁ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ collinear e.B e.A e.C := by
+  apply flip_collinear_fst_snd.mt
   exact e.ABC_nd
-lemma hnd₂ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ colinear e.D e.F e.E := by
-  apply perm_colinear_trd_fst_snd.mt
+lemma hnd₂ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ collinear e.D e.F e.E := by
+  apply perm_collinear_trd_fst_snd.mt
   exact e.EDF_nd
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.B := ⟨(ne_of_not_colinear hnd₁).2.2⟩
-instance D_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.E := ⟨(ne_of_not_colinear hnd₂).2.1⟩
-instance A_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.C := ⟨(ne_of_not_colinear hnd₁).1.symm⟩
-instance E_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.E e.F := ⟨(ne_of_not_colinear hnd₂).1⟩
-instance D_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.F := ⟨(ne_of_not_colinear hnd₂).2.2.symm⟩
-instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.B e.C := ⟨(ne_of_not_colinear hnd₁).2.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

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean

@@ -20,16 +20,16 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   h₁ : (SEG A B).length = (SEG D C).length
   h₂ : (SEG D B).length = (SEG A C).length
   -- nondegenerate
-  hnd₁ : ¬ colinear D B A
-  hnd₂ : ¬ colinear A C D
-  D_ne_A : D ≠ A :=(ne_of_not_colinear hnd₁).2.1
+  hnd₁ : ¬ collinear D B A
+  hnd₂ : ¬ collinear A C D
+  D_ne_A : D ≠ A :=(ne_of_not_collinear hnd₁).2.1
   -- $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_colinear e.hnd₁).1
-lemma a_ne_c {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.C := (ne_of_not_colinear e.hnd₂).2.2.symm
-lemma b_ne_d {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.D :=  (ne_of_not_colinear e.hnd₁).2.2
-lemma c_ne_d {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.C ≠ e.D :=(ne_of_not_colinear 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
   -- Use SSS to prove that $\triangle DBA \congr \triangle ACD$ or $\triangle DBA \congr_a \triangle ACD$.

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean

@@ -33,12 +33,12 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠
   Because $DB = DC$ ,we have $\angle D B C = -\angle D C B$
   $\angle A B D = \angle A B C - \angle D B C = \angle D C B - \angle A C B = --\angle A C D$
   -/
-  have h₁ : ¬ colinear e.A e.B e.C := by
-    exact (Quadrilateral_cvx.not_colinear₁₂₄ (QDR_cvx e.A e.B e.D e.C e.cvx_ABDC))
-  have h₂ : ¬ colinear e.D e.B e.C := by
-    have h₂' : ¬ colinear e.B e.D e.C := by
-      exact (Quadrilateral_cvx.not_colinear₂₃₄ (QDR_cvx e.A e.B e.D e.C e.cvx_ABDC))
-    apply flip_colinear_fst_snd.mt h₂'
+  have h₁ : ¬ collinear e.A e.B e.C := by
+    exact (Quadrilateral_cvx.not_collinear₁₂₄ (QDR_cvx e.A e.B e.D e.C e.cvx_ABDC))
+  have h₂ : ¬ collinear e.D e.B e.C := by
+    have h₂' : ¬ collinear e.B e.D e.C := by
+      exact (Quadrilateral_cvx.not_collinear₂₃₄ (QDR_cvx e.A e.B e.D e.C e.cvx_ABDC))
+    apply flip_collinear_fst_snd.mt h₂'
   have C_ne_B : e.C ≠ e.B := by
     exact (Quadrilateral_cvx.nd₂₄ (QDR_cvx e.A e.B e.D e.C e.cvx_ABDC))
   --Because $AB = AC$ ,we have $\angle A B C = -\angle A C B$.

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean

@@ -18,13 +18,13 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   C : Plane
   D : Plane
   --some nondegenerate
-  hnd₁ : ¬ colinear B C A
-  hnd₂ : ¬ colinear B C D
+  hnd₁ : ¬ collinear B C A
+  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_colinear e.hnd₁).2.2.symm⟩
-instance D_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.D e.B := ⟨(ne_of_not_colinear e.hnd₂).2.1.symm⟩
-instance A_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.C := ⟨(ne_of_not_colinear 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
   --$BD \para CA$
@@ -36,10 +36,10 @@ 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}: ¬ colinear 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_colinear hnd₃).1.symm⟩
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.B := ⟨(ne_of_not_colinear e.hnd₁).2.1.symm⟩
-instance B_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.E := ⟨(ne_of_not_colinear 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
   /-
@@ -52,8 +52,8 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : 
   We have $\triangle B E D \congr_a \triangle C A B$
   Thus $\angle B D E = -\angle C B A $.
   -/
-  have hnd₁' : ¬ colinear e.C e.A e.B := by
-    apply perm_colinear_trd_fst_snd.mt
+  have hnd₁' : ¬ collinear e.C e.A e.B := by
+    apply perm_collinear_trd_fst_snd.mt
     exact e.hnd₁
   --$DB = BC$
   have e₂ : (SEG e.D e.B).length = (SEG e.B e.C).length := by