redefine collinear & lemmas & naming

EuclideanGeometry/Check.lean

@@ -90,7 +90,7 @@ 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 : ¬ collinear A B C) : Prop := by
+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
@@ -99,7 +99,7 @@ def main_theorem (A B C : P) (h : ¬ collinear A B C) : Prop := by
   let E := Line.inx l₁ l₂ h'
   exact (E = B)
 
-example (A B C : P) (h : ¬ collinear 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_collinear h).2.2) (p := fun x => let hCB := (_ : C ≠ B);
 -- let l₁ := LIN A B x;

EuclideanGeometry/Example/AOPS/Chap3.lean

@@ -15,7 +15,7 @@ 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 : ¬ collinear 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_collinear hnd).2.2.symm
 lemma A_ne_C : A ≠ C := (ne_of_not_collinear hnd).2.1

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 : ¬ collinear 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 : ¬ collinear 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 : ¬ collinear 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 : ¬ collinear 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,7 +18,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
-  not_collinear_ABC : ¬ collinear 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.
@@ -86,7 +86,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
-  not_collinear_ABC : ¬ collinear 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.

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₁ : ¬ collinear A₁ B₁ C₁} {hnd₂ : ¬ collinear 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,7 +32,7 @@ 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 : ¬ collinear 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_collinear hnd).2.2
@@ -60,8 +60,8 @@ lemma B_ne_f : B ≠ F := by
     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 : ¬ 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 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 (Collinear.perm₁₃₂.mt (Collinear.perm₂₁₃.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 : ¬collinear A B C
-  EDF_nd : ¬collinear 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,11 +34,11 @@ 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
-  apply flip_collinear_fst_snd.mt
+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
-  apply perm_collinear_trd_fst_snd.mt
+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⟩

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean

@@ -20,8 +20,8 @@ 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₁ : ¬ collinear D B A
-  hnd₂ : ¬ collinear A C D
+  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)

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₁ : ¬ collinear e.A e.B e.C := by
+  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
+  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₂'
+    apply Collinear.perm₂₁₃.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,8 +18,8 @@ structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
   C : Plane
   D : Plane
   --some nondegenerate
-  hnd₁ : ¬ collinear B C A
-  hnd₂ : ¬ collinear 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_collinear e.hnd₁).2.2.symm⟩
@@ -36,7 +36,7 @@ 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
+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⟩
@@ -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₁' : ¬ collinear e.C e.A e.B := by
-    apply perm_collinear_trd_fst_snd.mt
+  have hnd₁' : ¬ Collinear e.C e.A e.B := by
+    apply Collinear.perm₃₁₂.mt
     exact e.hnd₁
   --$DB = BC$
   have e₂ : (SEG e.D e.B).length = (SEG e.B e.C).length := by

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean

@@ -13,11 +13,11 @@ In $▵ ABC$, $D, E$ are two different points on side $BC$, $AD = AE$, $∠ BAD
 Prove that $AB = AC$.
 -/
 -- Define $▵ ABC$.
-variable {A B C : P} {hnd1 : ¬ collinear A B C}
+variable {A B C : P} {hnd1 : ¬ Collinear A B C}
 -- $D, E$ are two different points on side $BC$.
 variable {D E : P} {hd : D LiesInt SEG B C} {he : E LiesInt SEG B C}
 -- nondegenerate
-lemma hnd2 : ¬ collinear A D E := by sorry
+lemma hnd2 : ¬ Collinear A D E := by sorry
 lemma a_ne_b : A ≠ B := by sorry
 lemma a_ne_d : A ≠ D := by sorry
 lemma a_ne_c : A ≠ C := by sorry
@@ -29,8 +29,8 @@ variable {hang : ∠ B A D a_ne_b a_ne_d = -∠ C A E a_ne_c a_ne_e}
 -- State the main goal.
 theorem Wuwowuji_Problem_1_6 : (SEG A B).length = (SEG A C).length := by
   -- nondegenerate
-  have hnd3 : ¬ collinear B D A := by sorry
-  have hnd4 : ¬ collinear C E A := by sorry
+  have hnd3 : ¬ Collinear B D A := by sorry
+  have hnd4 : ¬ Collinear C E A := by sorry
   -- Use ASA to prove $▵ BDA ≅ₐ ▵ CEA$.
   have h : (TRI_nd B D A hnd3) ≅ₐ (TRI_nd C E A hnd4) := by
     apply TriangleND.acongr_of_ASA

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean

@@ -15,7 +15,7 @@ Prove that $AD = BC$.
 -- $AD$ and $BC$ intersect at $O$.
 variable {A B C D O: P} {h1 : O LiesInt (SEG A D)} {h2 : O LiesInt (SEG B C)}
 -- nondegenerate
-variable {hnd1 : ¬ collinear C B A} {hnd2 : ¬ collinear D A B}
+variable {hnd1 : ¬ Collinear C B A} {hnd2 : ¬ Collinear D A B}
 lemma a_ne_b : A ≠ B := by sorry
 lemma a_ne_c : A ≠ C := by sorry
 lemma a_ne_d : A ≠ D := by sorry
@@ -33,7 +33,7 @@ theorem Wuwowuji_Problem_1_7 : (SEG A D).length = (SEG B C).length := by
   have o_ne_b : O ≠ B := by sorry
   have o_ne_c : O ≠ C := by sorry
   have o_ne_d : O ≠ D := by sorry
-  have hnd3 : ¬ collinear O A B := by sorry
+  have hnd3 : ¬ Collinear O A B := by sorry
   -- $▵ OAB$ is isoceles because $OA = OB$.
   have hisoc : (TRI_nd O A B hnd3).1.IsIsoceles := by
     calc

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean

@@ -14,7 +14,7 @@ Prove that $▵ OPD ≅ₐ ▵ OPE$.
 -/
 
 -- Define $A, B, C, O$ on the plane.
-variable {A B C O : Plane} {hnd1 : ¬ collinear O A B} {hnd2 : ¬ collinear O B C} {hnd3 : ¬ collinear O C A}
+variable {A B C O : Plane} {hnd1 : ¬ Collinear O A B} {hnd2 : ¬ Collinear O B C} {hnd3 : ¬ Collinear O C A}
 -- nondegenerate
 lemma o_ne_a : O ≠ A:= by sorry
 lemma o_ne_b : O ≠ B := by sorry
@@ -26,8 +26,8 @@ variable {P : Plane} {hp : P LiesInt (SEG O C)}
 -- $D, E$ is the perpendicular foot from $P$ to line $OA, OB$.
 variable {D E : Plane} {hd : D = perp_foot P (LIN O A o_ne_a.symm)} {he : E = perp_foot P (LIN O B o_ne_b.symm)}
 -- State the main goal.
-lemma hnd4 : ¬ collinear O P D := by sorry
-lemma hnd5 : ¬ collinear O P E := by sorry
+lemma hnd4 : ¬ Collinear O P D := by sorry
+lemma hnd5 : ¬ Collinear O P E := by sorry
 theorem Wuwowuji_Problem_1_8 : (TRI_nd O P D hnd4) ≅ₐ (TRI_nd O P E hnd5) := by
   sorry
 

EuclideanGeometry/Example/ExerciseXT8.lean

@@ -16,7 +16,7 @@ Prove that $\angle AY_1Z_2 + \angle BZ_1X_2 + \angle CX_1Y_2 + \angle Y_1Z_2A +
 -/
 
 -- Let $\triangle ABC$ be a nondegenerate triangle.
-variable {A B C : P} {hnd : ¬ collinear A B C}
+variable {A B C : P} {hnd : ¬ Collinear A B C}
 
 lemma c_ne_B : C ≠ B := sorry
 lemma B_ne_a : B ≠ A := sorry

EuclideanGeometry/Example/SCHAUM/Problem1.1.lean

@@ -16,7 +16,7 @@ Prove that $DM = EM$.
 -/
 /--/
 --Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
-variable {A B C : P} {not_collinear_ABC: ¬ collinear A B C} {isoceles_ABC: (▵ A B C).IsIsoceles}
+variable {A B C : P} {not_collinear_ABC: ¬ Collinear A B C} {isoceles_ABC: (▵ A B C).IsIsoceles}
 --Let $D$ be a point on $AB$.
 variable {D : P} {D_on_seg: D LiesInt (SEG A B)}
 --Let $E$ be a point on $AC$
@@ -31,7 +31,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
-  not_collinear_ABC : ¬ collinear A B C
+  not_collinear_ABC : ¬ Collinear A B C
   isoc_ABC : (▵ A B C).IsIsoceles
   --Let $D$ be a point on $AB$.
   D : Plane
@@ -66,9 +66,9 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SE
       _ = (SEG e.C e.A).length := e.isoc_ABC.symm
       _ = (SEG e.A e.C).length := length_of_rev_eq_length'
   --Triangle B D M nondegenerate.
-  have h₁ : ¬ collinear e.B e.D e.M := by sorry
+  have h₁ : ¬ Collinear e.B e.D e.M := by sorry
   --Triangle C E M nondegenerate.
-  have h₂ : ¬ collinear e.C e.E e.M := by sorry
+  have h₂ : ¬ Collinear e.C e.E e.M := by sorry
   --Points not equal for the definition of angle is not invalid.
   --$D \ne B$ and $M \ne B$ for ∠ D B M.
   haveI d_ne_b : PtNe e.D e.B := ⟨ (ne_of_not_collinear h₁).2.2⟩

EuclideanGeometry/Example/SCHAUM/Problem1.12.lean

@@ -54,7 +54,7 @@ theorem SCHAUM_Problem_1_12 : Quadrilateral.IsParallelogram (QDR A B C D) := by
   sorry
   /-
   apply is_prg_of_para_eq_length'
-  · unfold perpendicular at *
+  · unfold Perpendicular at *
     unfold parallel
     have h : toProj (SegND B C (c_ne_B (hconv := hconv))) = toProj (SegND A D (A_ne_d (hconv := hconv)).symm) := by
       calc

EuclideanGeometry/Example/SCHAUM/Problem1.14.lean

@@ -64,8 +64,8 @@ theorem result1 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (
   Thus $\triangle MBP \congr \triangle NCQ$ (by AAS),
   which implies $PM = QN$.
   -/
-  have not_collinear_MBP : ¬ collinear e.M e.B e.P := by sorry
-  have not_collinear_NDQ : ¬ collinear e.N e.D e.Q := by sorry
+  have not_collinear_MBP : ¬ Collinear e.M e.B e.P := by sorry
+  have not_collinear_NDQ : ¬ Collinear e.N e.D e.Q := by sorry
   have B_ne_M : e.B ≠ e.M := by sorry
   have P_ne_M : e.P ≠ e.M := by sorry
   have D_ne_N : e.D ≠ e.N := by sorry
@@ -85,7 +85,7 @@ theorem result2 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (
   -- We have $BD \perp QN$ because $N$ is the perpendicular foot from $Q$ to $BD$.
   have BD_perp_QN : LIN e.B e.D e.D_ne_B ⟂ LIN e.Q e.N e.N_ne_Q := by
     simp only [e.perp_foot_N]
-    exact perpendicular.symm (line_of_self_perp_foot_perp_line_of_not_lies_on e.not_Q_lieson_BD)
+    exact Perpendicular.symm (line_of_self_perp_foot_perp_line_of_not_lies_on e.not_Q_lieson_BD)
   -- then $PM \perp QN$ because $PM \perp BD$ and $BD \perp QN$.
   exact parallel_of_perp_perp (l₂ := (LIN e.B e.D e.D_ne_B)) PM_perp_BD BD_perp_QN
 

EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean

@@ -19,7 +19,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
-  not_collinear_ABC : ¬ collinear A B C
+  not_collinear_ABC : ¬ Collinear A B C
   isoceles_ABC : (▵ A B C).IsIsoceles
   --Let $D$ be a point on $AB$.
   D : Plane
@@ -46,7 +46,7 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
   A : Plane
   B : Plane
   C : Plane
-  not_collinear_ABC : ¬ collinear A B C
+  not_collinear_ABC : ¬ Collinear A B C
   hisoc : (▵ A B C).IsIsoceles
   --Let $D$ be a point on $AB$.
   D : Plane
@@ -118,15 +118,15 @@ theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SE
   -- We have $C \ne B$.
   have C_ne_B : e.C ≠ e.B := (ne_of_not_collinear e.not_collinear_ABC).1
   -- We have $\triangle PBD$ is nondegenerate
-  have not_collinear_PBD : ¬ collinear e.P e.B e.D := by sorry
+  have not_collinear_PBD : ¬ Collinear e.P e.B e.D := by sorry
   -- We have $B \ne D$.
   have B_ne_D : e.B ≠ e.D := (ne_of_not_collinear not_collinear_PBD).1.symm
   -- We have $P \ne D$.
   have P_ne_D : e.P ≠ e.D := (ne_of_not_collinear not_collinear_PBD).2.1
   -- We have $P \ne B$.
   have P_ne_B : e.P ≠ e.B := (ne_of_not_collinear not_collinear_PBD).2.2.symm
   -- We have $\triangle QCE$ is nondegenerate
-  have not_collinear_QCE : ¬ collinear e.Q e.C e.E := by sorry
+  have not_collinear_QCE : ¬ Collinear e.Q e.C e.E := by sorry
   -- We have $C \ne E$.
   have C_ne_E : e.C ≠ e.E := (ne_of_not_collinear not_collinear_QCE).1.symm
   -- We have $Q \ne E$.

EuclideanGeometry/Example/SCHAUM/Problem1.2.lean

@@ -15,7 +15,7 @@ Prove that $DP = EQ$.
 -/
 
 --Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
-variable {A B C : Plane} {not_collinear_ABC: ¬ collinear A B C} {isoceles_ABC: (▵ A B C).IsIsoceles}
+variable {A B C : Plane} {not_collinear_ABC: ¬ Collinear A B C} {isoceles_ABC: (▵ A B C).IsIsoceles}
 --Let $D$ be a point on $AB$.
 variable {D : Plane} {D_int_AB: D LiesInt (SEG A B)}
 --Let $E$ be a point on $AC$
@@ -96,15 +96,15 @@ theorem Problem1_2_ : (SEG D P).length = (SEG E Q).length := by
   -- We have $C \ne B$.
   have c_ne_b : C ≠ B := (ne_of_not_collinear not_collinear_ABC).1
   -- We have $\triangle PBD$ is nondegenerate
-  have not_collinear_ABC1 : ¬ collinear P B D := by sorry
+  have not_collinear_ABC1 : ¬ Collinear P B D := by sorry
   -- We have $B \ne D$.
   have b_ne_d : B ≠ D := (ne_of_not_collinear not_collinear_ABC1).1.symm
   -- We have $P \ne D$.
   have p_ne_d : P ≠ D := (ne_of_not_collinear not_collinear_ABC1).2.1
   -- We have $P \ne B$.
   have p_ne_b : P ≠ B := (ne_of_not_collinear not_collinear_ABC1).2.2.symm
   -- We have $\triangle QCE$ is nondegenerate
-  have not_collinear_ABC2 : ¬ collinear Q C E := by sorry
+  have not_collinear_ABC2 : ¬ Collinear Q C E := by sorry
   -- We have $C \ne E$.
   have c_ne_e : C ≠ E := (ne_of_not_collinear not_collinear_ABC2).1.symm
   -- We have $Q \ne E$.