Updated Tactic Congruence

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_11.lean

@@ -54,16 +54,16 @@ lemma E_ne_F' {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.E
   _< ⟨e.C, e.C_on_l⟩ := e.E_lt_C_on_l
   _< ⟨e.F, e.F_on_l⟩ := e.C_lt_F_on_l
 instance E_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.E e.F := ⟨E_ne_F'⟩
-lemma not_colinear_ACB {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : ¬ colinear e.A e.C e.B := by sorry
-lemma not_colinear_DEF {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : ¬ colinear e.D e.E e.F := by sorry
-instance B_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.B e.A := ⟨(ne_of_not_colinear not_colinear_ACB).2.1.symm⟩
-instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.C e.A := ⟨(ne_of_not_colinear not_colinear_ACB).2.2⟩
-instance F_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.F e.D := ⟨(ne_of_not_colinear not_colinear_DEF).2.1.symm⟩
-instance E_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.E e.D := ⟨(ne_of_not_colinear not_colinear_DEF).2.2⟩
+lemma not_collinear_ACB {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : ¬ Collinear e.A e.C e.B := by sorry
+lemma not_collinear_DEF {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : ¬ Collinear e.D e.E e.F := by sorry
+instance B_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.B e.A := ⟨(ne_of_not_collinear not_collinear_ACB).2.1.symm⟩
+instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear not_collinear_ACB).2.2⟩
+instance F_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.F e.D := ⟨(ne_of_not_collinear not_collinear_DEF).2.1.symm⟩
+instance E_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.E e.D := ⟨(ne_of_not_collinear not_collinear_DEF).2.2⟩
 
 structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting Plane where
-  not_colinear_ACB : ¬ Collinear A C B := not_colinear_ACB
-  not_colinear_DEF : ¬ Collinear D E F := not_colinear_DEF
+  not_colinear_ACB : ¬ Collinear A C B := not_collinear_ACB
+  not_colinear_DEF : ¬ Collinear D E F := not_collinear_DEF
 
 -- Prove that $\angle BAC = - \angle FDE$.
 theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (∠ e.B e.A e.C) = - (∠ e.F e.D e.E) := by
@@ -98,6 +98,7 @@ theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (
     · exact BA_eq_FD
     · exact e.AC_eq_DE
     · exact clockwise_ACB_eq_neg_clockwise_DEF
+
 end Problem_11
 
 end EuclidGeom

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_25.lean

@@ -0,0 +1,40 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+namespace Problem_25
+
+/-
+Let $\triangle ABC$ be an isoceles triangle with $AB = AC$. Let $D, E$ be two points lying on segment $BC$ such that $B, D, E, C$ lies on segment $BC$ in this order and that $AD = AE$.
+Prove that $\triangle ABD \cong \triangle ACE$
+-/
+
+structure Setting (Plane : Type _) [EuclideanPlane Plane] where
+-- Let $\triangle ABC$ be an isoceles triangle with $AB = AC$.
+  A : Plane
+  B : Plane
+  C : Plane
+  not_collinear_ABC : ¬ Collinear A B C
+  ABC_isoceles : (▵ A B C).IsIsoceles
+-- Let $D, E$ be two points lying on segment $BC$ such that $B, D, E, C$ lies on segment $BC$ in this order
+  D : Plane
+  E : Plane
+  D_int_BE : D LiesInt (SEG B E)
+  E_int_DC : E LiesInt (SEG D C)
+-- such that $AD = AE$
+  AD_eq_AE : (SEG A D).length = (SEG A E).length
+
+abbrev lelem {P : Type _} [EuclideanPlane P] (A : P) {l : DirLine P} (ha : A LiesOn l) : l.carrier.Elem := ⟨A, ha⟩
+
+theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (▵ e.A e.B e.D) ≅ₐ (▵ e.A e.C e.E) := by
+  haveI : PtNe e.A e.C := ⟨(ne_of_not_collinear e.not_collinear_ABC).2.1⟩
+  haveI : PtNe e.B e.A := ⟨(ne_of_not_collinear e.not_collinear_ABC).2.2⟩
+  haveI : PtNe e.D e.B := ⟨e.D_int_BE.2⟩
+  haveI : PtNe e.E e.C := ⟨(Seg.lies_int_rev_iff_lies_int.mpr e.E_int_DC).2⟩
+  sorry
+
+end Problem_25
+
+end EuclidGeom

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_5.lean

@@ -1,5 +1,6 @@
 import EuclideanGeometry.Foundation.Index
 import EuclideanGeometry.Foundation.Axiom.Linear.Order
+import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex_trash
 
 noncomputable section
 
@@ -51,7 +52,7 @@ lemma D_ne_F' {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.D
   _< ⟨e.C, e.C_on_l⟩ := e.F_lt_C_on_l
   _< ⟨e.D, e.D_on_l⟩ := e.C_lt_D_on_l
 instance D_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.D e.F := ⟨D_ne_F'⟩
-lemma not_colinear_BCA {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ colinear e.B e.C e.A := by
+lemma not_collinear_BCA {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ Collinear e.B e.C e.A := by
   have h : IsOnOppositeSide e.B e.E (RAY e.C e.A) := by
     have h3 : (RAY e.C e.A).toLine = e.l.toLine := by
       calc
@@ -69,10 +70,10 @@ lemma not_colinear_BCA {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Pla
         _=_ := by congr
     simp only [this]
     exact e.B_E_IsOnOppositeSide_l
-  have h1 : ¬ colinear e.C e.A e.B := (not_colinear_of_IsOnOppositeSide e.C e.A e.B e.E h).1
+  have h1 : ¬ Collinear e.C e.A e.B := (not_collinear_of_IsOnOppositeSide e.C e.A e.B e.E h).1
   by_contra h2; absurd h1
-  exact perm_colinear_snd_trd_fst h2
-lemma not_colinear_EFD {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ colinear e.E e.F e.D := by
+  perm_collinear
+lemma not_collinear_EFD {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ Collinear e.E e.F e.D := by
   have h : IsOnOppositeSide e.B e.E (RAY e.F e.D) := by
     have h3 : (RAY e.F e.D).toLine = e.l.toLine := by
       calc
@@ -90,21 +91,21 @@ lemma not_colinear_EFD {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Pla
         _=_ := by congr
     simp only [this]
     exact e.B_E_IsOnOppositeSide_l
-  have h1 : ¬ colinear e.F e.D e.E := (not_colinear_of_IsOnOppositeSide e.F e.D e.B e.E h).2
+  have h1 : ¬ Collinear e.F e.D e.E := (not_collinear_of_IsOnOppositeSide e.F e.D e.B e.E h).2
   by_contra h2; absurd h1
-  exact perm_colinear_snd_trd_fst h2
+  perm_collinear
 -- Claim : $C \ne B$.
-instance C_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.B := ⟨(ne_of_not_colinear not_colinear_BCA).2.2⟩
+instance C_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.B := ⟨(ne_of_not_collinear not_collinear_BCA).2.2⟩
 -- Claim : $A \ne B$.
-instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_colinear not_colinear_BCA).2.1.symm⟩
+instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear not_collinear_BCA).2.1.symm⟩
 -- Claim : $E \ne F$.
-instance E_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.E e.F := ⟨(ne_of_not_colinear not_colinear_EFD).2.2.symm⟩
+instance E_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.E e.F := ⟨(ne_of_not_collinear not_collinear_EFD).2.2.symm⟩
 -- Claim : $E \ne D$.
-instance E_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.E e.D := ⟨(ne_of_not_colinear not_colinear_EFD).2.1⟩
+instance E_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.E e.D := ⟨(ne_of_not_collinear not_collinear_EFD).2.1⟩
 
 structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
-  not_colinear_BCA : ¬ colinear B C A := not_colinear_BCA
-  not_colinear_EFD : ¬ colinear E F D := not_colinear_EFD
+  not_collinear_BCA : ¬ Collinear B C A := not_collinear_BCA
+  not_collinear_EFD : ¬ Collinear E F D := not_collinear_EFD
 -- and that $CB \parallel FE$,
   CB_parallel_FE : (LIN C B) ∥ (LIN F E)
 -- If $\angle BAC = - \angle EDF$,
@@ -115,11 +116,11 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
 
 theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (SEG e.A e.B).length = (SEG e.D e.E).length := by
   have F_int_AC : e.F LiesInt (SEG e.A e.C) := by
-    apply DirLine.lies_int_of_lt_and_lt e.A_on_l e.F_on_l e.C_on_l
+    apply DirLine.lies_int_seg_of_lt_and_lt e.A_on_l e.F_on_l e.C_on_l
     simp only [e.A_lt_F_on_l]
     simp only [e.F_lt_C_on_l]
   have C_int_DF : e.C LiesInt (SEG e.D e.F) := by
-    apply DirLine.lies_int_of_gt_and_gt e.D_on_l e.C_on_l e.F_on_l
+    apply DirLine.lies_int_seg_of_gt_and_gt e.D_on_l e.C_on_l e.F_on_l
     simp only [e.C_lt_D_on_l]
     simp only [e.F_lt_C_on_l]
   have C_ne_F' : e.C ≠ e.F := by
@@ -176,10 +177,10 @@ theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (S
       apply neg_toDir_of_parallel_and_IsOnOppositeSide
       · exact e.CB_parallel_FE
       · exact h
-    apply ang_eq_ang_of_toDir_rev_toDir
+    apply ang_eq_ang_of_toDir_eq_neg_toDir
     · exact dir_CA_eq_neg_dir_FD
     · exact dir_CB_eq_neg_dir_FE
-  have triangle_BCA_congr_triangle_EFD : (TRI_nd e.B e.C e.A e.not_colinear_BCA) ≅ (TRI_nd e.E e.F e.D e.not_colinear_EFD) := by
+  have triangle_BCA_congr_triangle_EFD : (TRI_nd e.B e.C e.A e.not_collinear_BCA) ≅ (TRI_nd e.E e.F e.D e.not_collinear_EFD) := by
     apply TriangleND.congr_of_ASA
     · exact angle_ACB_eq_angle_DFE
     · exact CA_eq_FD

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean

@@ -18,11 +18,11 @@ structure Setting1 (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 : $B \ne A$.
-  B_ne_A : PtNe B A := ⟨(ne_of_not_colinear not_colinear_ABC).2.2⟩
+  B_ne_A : PtNe B A := ⟨(ne_of_not_collinear not_collinear_ABC).2.2⟩
 -- Claim : $C \ne A$.
-  C_ne_A : PtNe C A := ⟨(ne_of_not_colinear not_colinear_ABC).2.1.symm⟩
+  C_ne_A : PtNe C A := ⟨(ne_of_not_collinear not_collinear_ABC).2.1.symm⟩
 -- Let $D$ be a point on the segment $BC$.
   D : Plane
   D_int_BC : D LiesInt (SEG B C)
@@ -31,37 +31,37 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where
   E_int_BC : E LiesInt (SEG B C)
   E_ne_D : PtNe E D
 -- Claim : $E \ne B$.
-  E_ne_B : PtNe E B := ⟨ne_source_of_lies_int_seg B C E E_int_BC⟩
+  E_ne_B : PtNe E B := ⟨E_int_BC.2⟩
 -- Claim : $D \ne C$.
-  D_ne_C : PtNe D C := ⟨ne_source_of_lies_int_seg C B D (Seg.lies_int_rev_iff_lies_int.mp D_int_BC)⟩
+  D_ne_C : PtNe D C := ⟨(Seg.lies_int_rev_iff_lies_int.mpr D_int_BC).2⟩
 -- such that the points on segment $BC$ are arranged in the order $B, D, E, C$
   D_int_BE : D LiesInt (SEG_nd B E)
   E_int_DC : E LiesInt (SEG_nd D C)
 
 
 attribute [instance] Setting1.B_ne_A Setting1.C_ne_A Setting1.E_ne_D Setting1.E_ne_B Setting1.D_ne_C
 instance D_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.D e.A := by
-  have h1 : ¬ colinear e.A e.B e.C := e.not_colinear_ABC
+  have h1 : ¬ Collinear e.A e.B e.C := e.not_collinear_ABC
   have : e.D ≠ e.A := by
     by_contra h
-    have h2 : ¬ colinear e.D e.B e.C := by simp only [h]; exact h1
+    have h2 : ¬ Collinear e.D e.B e.C := by simp only [h]; exact h1
     absurd h2
     have h3 : e.D LiesOn (SEG e.B e.C) := by apply Seg.lies_on_of_lies_int e.D_int_BC
     have h4 : e.B LiesOn (SEG e.B e.C) := by apply Seg.source_lies_on
     have h5 : e.C LiesOn (SEG e.B e.C) := by apply Seg.target_lies_on
-    exact Seg.colinear_of_lies_on h3 h4 h5
+    exact Seg.collinear_of_lies_on h3 h4 h5
   exact ⟨this⟩
 
 instance E_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.E e.A := by
-  have h1 : ¬ colinear e.A e.B e.C := e.not_colinear_ABC
+  have h1 : ¬ Collinear e.A e.B e.C := e.not_collinear_ABC
   have : e.E ≠ e.A := by
     by_contra h
-    have h2 : ¬ colinear e.E e.B e.C := by simp only [h]; exact h1
+    have h2 : ¬ Collinear e.E e.B e.C := by simp only [h]; exact h1
     absurd h2
     have h3 : e.E LiesOn (SEG e.B e.C) := by apply Seg.lies_on_of_lies_int e.E_int_BC
     have h4 : e.B LiesOn (SEG e.B e.C) := by apply Seg.source_lies_on
     have h5 : e.C LiesOn (SEG e.B e.C) := by apply Seg.target_lies_on
-    exact Seg.colinear_of_lies_on h3 h4 h5
+    exact Seg.collinear_of_lies_on h3 h4 h5
   exact ⟨this⟩
 
 structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
@@ -72,41 +72,41 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan
 
 -- Prove that $AB = AC$.
 theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (SEG e.A e.B).length = (SEG e.A e.C).length := by
-  haveI D_ne_B : PtNe e.D e.B := ⟨ne_source_of_lies_int_seg e.B e.C e.D e.D_int_BC⟩
-  haveI E_ne_C : PtNe e.E e.C := ⟨ne_source_of_lies_int_seg e.C e.B e.E (Seg.lies_int_rev_iff_lies_int.mp e.E_int_BC)⟩
-  have not_colinear_BAD : ¬ colinear e.B e.A e.D := by sorry
-  have not_colinear_CAE : ¬ colinear e.C e.A e.E := by sorry
-  have not_colinear_ADE : ¬ colinear e.A e.D e.E := by sorry
+  haveI D_ne_B : PtNe e.D e.B := ⟨e.D_int_BC.2⟩
+  haveI E_ne_C : PtNe e.E e.C := ⟨(Seg.lies_int_rev_iff_lies_int.mpr e.E_int_BC).2⟩
+  have not_collinear_BAD : ¬ Collinear e.B e.A e.D := by sorry
+  have not_collinear_CAE : ¬ Collinear e.C e.A e.E := by sorry
+  have not_collinear_ADE : ¬ Collinear e.A e.D e.E := by sorry
   have isoceles_ADE : (TRI e.A e.D e.E).IsIsoceles := by
     calc
     (SEG e.E e.A).length = (SEG e.A e.E).length := by apply length_of_rev_eq_length'
     _= (SEG e.A e.D).length := e.AD_eq_AE.symm
   have angle_DAB_eq_neg_angle_EAC : ∠ e.D e.A e.B = - (∠ e.E e.A e.C) := by
     calc
-    ∠ e.D e.A e.B = - (∠ e.B e.A e.D) := by apply neg_value_of_rev_ang
+    ∠ e.D e.A e.B = - (∠ e.B e.A e.D) := by apply Angle.neg_value_of_rev_ang
     _= ∠ e.C e.A e.E := by simp only [e.angle_BAD_eq_neg_angle_CAE, neg_neg]
-    _= - (∠ e.E e.A e.C) := by apply neg_value_of_rev_ang
+    _= - (∠ e.E e.A e.C) := by apply Angle.neg_value_of_rev_ang
   have angle_BDA_eq_neg_angle_CEA : ∠ e.B e.D e.A = - (∠ e.C e.E e.A) := by
     calc
     (∠ e.B e.D e.A)
     _= ((∠ e.B e.D e.A) + (∠ e.A e.D e.E)) - (∠ e.A e.D e.E) := by abel
     _= (∠ e.B e.D e.E) - (∠ e.A e.D e.E) := by
       congr 1; exact ang_value_eq_ang_value_add_ang_value e.B e.A e.E e.D
     _= ↑ (π) - (∠ e.A e.D e.E) := by
-      congr 1; exact liesint_segnd_value_eq_pi' e.D_int_BE
+      congr 1; exact Angle.value_eq_pi_of_lies_int_seg_nd e.D_int_BE
     _= ↑ (π) + (- ∠ e.A e.D e.E) := by abel
     _= ↑ (π) + (∠ e.E e.D e.A) := by
       congr 1; symm;
-      apply neg_value_of_rev_ang
+      apply Angle.neg_value_of_rev_ang
     _= ↑ (π) + (∠ e.A e.E e.D) := by
       congr 1;
       exact (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (TRI_nd e.A e.D e.E not_colinear_ADE)).mp isoceles_ADE
     _= (∠ e.D e.E e.C) + (∠ e.A e.E e.D) := by
-      congr 1; symm; exact liesint_segnd_value_eq_pi' e.E_int_DC
+      congr 1; symm; exact Angle.value_eq_pi_of_lies_int_seg_nd e.E_int_DC
     _= (∠ e.A e.E e.D) + (∠ e.D e.E e.C) := by abel
     _= (∠ e.A e.E e.C) := by exact ang_value_eq_ang_value_add_ang_value e.A e.D e.C e.E
-    _= - (∠ e.C e.E e.A) := by apply neg_value_of_rev_ang
-  have triangle_BAD_acongr_triangle_CAE : (TRI_nd e.B e.A e.D not_colinear_BAD) ≅ₐ (TRI_nd e.C e.A e.E not_colinear_CAE) := by
+    _= - (∠ e.C e.E e.A) := by apply Angle.neg_value_of_rev_ang
+  have triangle_BAD_acongr_triangle_CAE : (TRI_nd e.B e.A e.D not_collinear_BAD) ≅ₐ (TRI_nd e.C e.A e.E not_collinear_CAE) := by
     apply TriangleND.acongr_of_ASA
     · exact angle_DAB_eq_neg_angle_EAC
     · exact e.AD_eq_AE