fix

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean

@@ -38,7 +38,7 @@ lemma hnd₁ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Co
   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 Collinear.perm₂₃₁.mt
+  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_4.lean

@@ -53,7 +53,7 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : 
   Thus $\angle B D E = -\angle C B A $.
   -/
   have hnd₁' : ¬ Collinear e.C e.A e.B := by
-    apply Collinear.perm₂₃₁.mt
+    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/Foundation/Axiom/Circle/Basic.lean

@@ -183,7 +183,7 @@ lemma pts_lieson_circle_vec_eq {A B : P} {ω : Circle P} [hne : PtNe B A] (hl₁
   apply vec_eq_dist_eq_of_lies_on_line_pt_pt_of_ptNe
   · have : (perp_foot ω.center (LIN A B)) LiesOn (LIN A B) := perp_foot_lies_on_line _ _
     have : Collinear A B (perp_foot ω.center (LIN A B)) := Line.pt_pt_linear this
-    have : Collinear (perp_foot ω.center (LIN A B)) A B := Collinear.perm₂₃₁ this
+    have : Collinear (perp_foot ω.center (LIN A B)) A B := Collinear.perm₃₁₂ this
     apply Line.pt_pt_maximal this
   apply (sq_eq_sq dist_nonneg dist_nonneg).mp
   calc

EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean

@@ -161,7 +161,7 @@ theorem antipode_iff_collinear (A B : P) {ω : Circle P} [h : PtNe B A] (h₁ :
 
 theorem mk_pt_pt_diam_isantipode {A B : P} [h : PtNe A B] : Arc.IsAntipode A B (Circle.mk_pt_pt_diam_fst_lieson) (Circle.mk_pt_pt_diam_snd_lieson) := by
   have hc : Collinear (SEG A B).midpoint A B := by
-    apply Collinear.perm₂₃₁
+    apply Collinear.perm₃₁₂
     apply Line.pt_pt_linear
     show (SEG A B).midpoint LiesOn (SEG_nd A B).toLine
     apply SegND.lies_on_toLine_of_lie_on

EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean

@@ -119,14 +119,14 @@ theorem Collinear.perm₂₁₃ {A B C : P} (c : collinear A B C) : collinear B
       rw [← vec_sub_vec A B C, e, ← neg_vec A B, smul_neg, sub_smul, neg_sub, one_smul]
     exact collinear_of_vec_eq_smul_vec e'
 
-theorem Collinear.perm₃₁₂ {A B C : P} (h : collinear A B C) : collinear B C A :=
-  flip_collinear_snd_trd (flip_collinear_fst_snd h)
+theorem Collinear.perm₂₃₁ {A B C : P} (h : collinear A B C) : collinear B C A :=
+  Collinear.perm₁₃₂ (Collinear.perm₂₁₃ h)
 
-theorem Collinear.perm₂₃₁ {A B C : P} (h : collinear A B C) : collinear C A B :=
-  perm_collinear_snd_trd_fst (perm_collinear_snd_trd_fst h)
+theorem Collinear.perm₃₁₂ {A B C : P} (h : collinear A B C) : collinear C A B :=
+  Collinear.perm₂₃₁ (Collinear.perm₂₃₁ h)
 
 theorem Collinear.perm₃₂₁ {A B C : P} (h : collinear A B C) : collinear C B A :=
-  perm_collinear_snd_trd_fst (flip_collinear_snd_trd h)
+  Collinear.perm₂₃₁ (Collinear.perm₁₃₂ h)
 
 -- the proof of this theorem using def of line seems to be easier
 /-- Given four points $A$, $B$, $C$, $D$ with $B \neq A$, if $A$, $B$, $C$ are collinear, and if $A$, $B$, $D$ are collinear, then $A$, $C$, $D$ are collinear. -/

EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean

@@ -12,7 +12,7 @@ section ratio
 /-
 Below is the definition of divratio using ddist, which I think might not be a good idea.
 
-def divratio (A B C : P) (colin : Collinear A B C) (cnea : C ≠ A) : ℝ := (DirLine.ddist (B := B) (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ (triv_collinear₁₂ A C))) (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ colin))) / (DirLine.ddist (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ (triv_collinear₁₂ A C))) (DirLine.pt_pt_maximal cnea (Collinear.perm₂₃₁ (triv_collinear₁₂ C A))))
+def divratio (A B C : P) (colin : Collinear A B C) (cnea : C ≠ A) : ℝ := (DirLine.ddist (B := B) (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ (triv_collinear₁₂ A C))) (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ colin))) / (DirLine.ddist (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ (triv_collinear₁₂ A C))) (DirLine.pt_pt_maximal cnea (Collinear.perm₃₁₂ (triv_collinear₁₂ C A))))
 -/
 
 def divratio (A B C : P) : ℝ := ((VEC A B)/(VEC A C)).1

EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean

@@ -326,7 +326,7 @@ theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr
         exact Seg.length_eq_norm_toVec
       rcases SameRay.exists_pos g h₁ h₂ with ⟨_, ⟨_, ⟨_, ⟨_, g⟩⟩⟩⟩
       rw [← neg_vec C B, ← neg_one_smul ℝ, ← mul_smul, mul_neg_one, ← eq_inv_smul_iff₀ (by linarith), ← mul_smul] at g
-      exact Collinear.perm₃₁₂ (collinear_of_vec_eq_smul_vec g)
+      exact Collinear.perm₂₃₁ (collinear_of_vec_eq_smul_vec g)
 
 theorem triangle_ineq' (nontriv : tr.IsND) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := by
   have ne : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length := by

EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva.lean

@@ -49,7 +49,7 @@ attribute [instance] a_ne_b b_ne_c c_ne_a d_ne_a d_ne_b d_ne_c
 --$D,C,A$ are not collinear
 lemma ncolin_dca : ¬ Collinear D C A := by
   intro h0
-  exact cad_nd (Collinear.perm₃₁₂ h0)
+  exact cad_nd (Collinear.perm₂₃₁ h0)
 
 --$E,B,C$ are collinear
 lemma colin_ebc : Collinear E B C := by
@@ -79,7 +79,7 @@ lemma dratio_ebc_eq_wedge_div_wedge : divratio E B C = (wedge D B A) / (wedge D
 --$D,A,B$ are not collinear
 lemma ncolin_dab : ¬ Collinear D A B := by
   intro h0
-  exact abd_nd (Collinear.perm₃₁₂ h0)
+  exact abd_nd (Collinear.perm₂₃₁ h0)
 
 --$F,C,A$ are collinear
 lemma colin_fca : Collinear F C A := by
@@ -109,7 +109,7 @@ lemma dratio_fca_eq_wedge_div_wedge : divratio F C A = (wedge D C B) / (wedge D
 --$D,B,C$ are not collinear
 lemma ncolin_dbc : ¬ Collinear D B C := by
   intro h0
-  exact bcd_nd (Collinear.perm₃₁₂ h0)
+  exact bcd_nd (Collinear.perm₂₃₁ h0)
 
 --$G,A,B$ are collinear
 lemma colin_gab : Collinear G A B := by

EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean

@@ -41,7 +41,7 @@ theorem odist_eq_divratio_mul_odist (A B C : P) (dl : DirLine P) (colin : Collin
   simp only [map_smul, smul_eq_mul]
 
 theorem  wedge_eq_divratio_mul_wedge_of_collinear_collinear (A B C D E : P) (colin : Collinear A B C) [cnea : PtNe C A] (colin' : Collinear A D E) : wedge D B E = (divratio A B C) * wedge D C E := by
-  rw[← wedge312 D B E, wedge_eq_wedge_add_wedge_of_collinear E A D B (Collinear.perm₂₃₁ colin'), ← wedge312 D C E, wedge_eq_wedge_add_wedge_of_collinear E A D C (Collinear.perm₂₃₁ colin'), wedge213 A B D, wedge312 A B E, wedge213 A C D, wedge312 A C E,wedge_eq_divratio_mul_wedge_of_collinear A B C D colin,wedge_eq_divratio_mul_wedge_of_collinear A B C E colin]
+  rw[← wedge312 D B E, wedge_eq_wedge_add_wedge_of_collinear E A D B (Collinear.perm₃₁₂ colin'), ← wedge312 D C E, wedge_eq_wedge_add_wedge_of_collinear E A D C (Collinear.perm₃₁₂ colin'), wedge213 A B D, wedge312 A B E, wedge213 A C D, wedge312 A C E,wedge_eq_divratio_mul_wedge_of_collinear A B C D colin,wedge_eq_divratio_mul_wedge_of_collinear A B C E colin]
   ring
 
 theorem ratio_eq_wedge_div_wedge_of_collinear_collinear_notcoliear (A B C D E : P) (colin : Collinear A B C) [cnea : PtNe C A] (colin' : Collinear A D E) (ncolin : ¬ Collinear D C E) : divratio A B C = (wedge D B E) / (wedge D C E) := by

EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean

@@ -184,7 +184,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qd
          simp only [neg_smul, one_smul, neg_vec]
          rw[o]
        exact collinear_of_vec_eq_smul_vec' ooo
-     simp only [flip_collinear_fst_snd oo, not_true_eq_false] at h
+     simp only [Collinear.perm₂₁₃ oo, not_true_eq_false] at h
    have hcd : qdr_nd.point₃ ≠ qdr_nd.point₄ := by
      by_contra k₂
      have k₂₂ : VEC qdr_nd.point₄ qdr_nd.point₃=0 := by
@@ -196,7 +196,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qd
      simp only [k₂₃.symm, ne_eq, not_true_eq_false] at hba
    have t : ¬ Collinear qdr_nd.point₂ qdr_nd.point₁ qdr_nd.point₃ := by
      by_contra k
-     simp only [flip_collinear_fst_snd k, not_true_eq_false] at h
+     simp only [Collinear.perm₂₁₃ k, not_true_eq_false] at h
    have x : ¬ collinear_of_nd (A := qdr_nd.point₂) (B := qdr_nd.point₁) (C := qdr_nd.point₃) := by
      unfold collinear at t
      simp only [hca, hbc, hba.symm, or_self, dite_false] at t
@@ -287,7 +287,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qd
        rw[l₂',l₃]
        exact k₁
      simp[p₄] at s₂
-   simp [flip_collinear_fst_snd m₃] at m₂
+   simp [Collinear.perm₂₁₃ m₃] at m₂
    by_contra m₅
    have m₄ :  ¬ Collinear qdr_nd.point₄ qdr_nd.point₃ qdr_nd.point₁ := by
      by_contra k₂
@@ -298,7 +298,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qd
        rw[l₄',l₃']
        exact k₂
      simp[p₅] at s₃
-   simp [flip_collinear_fst_snd m₅] at m₄
+   simp [Collinear.perm₂₁₃ m₅] at m₄
    by_contra m₇
    have m₆ :  ¬ Collinear qdr_nd.point₁ qdr_nd.point₄ qdr_nd.point₂ := by
      by_contra k₃
@@ -309,7 +309,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qd
        rw[l₄,l₁]
        exact k₃
      simp [p₆] at s₄
-   simp [flip_collinear_fst_snd m₇] at m₆
+   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
@@ -492,12 +492,12 @@ theorem qdr_nd_is_prg_nd_of_para_para_not_collinear₁₂₃ (h₁ : qdr_nd.edge
     rw [(smul_smul (- r) c (VEC qdr_nd.point₁ qdr_nd.point₂)).symm,eq''.symm,neg_smul,eq.symm]
     exact (neg_vec qdr_nd.point₃ qdr_nd.point₁).symm
   by_contra iscollinear
-  apply flip_collinear_fst_trd at iscollinear
+  apply Collinear.perm₃₂₁ at iscollinear
   rw [collinear_iff_eq_smul_vec_of_ne] at iscollinear
   rcases iscollinear with ⟨r,eq⟩
   apply notcollinear
   have para : qdr_nd.edge_nd₃₄.toVecND ∥ qdr_nd.edge_nd₁₂.toVecND := by sorry
-  apply flip_collinear_fst_trd
+  apply Collinear.perm₃₂₁
   rw [collinear_iff_eq_smul_vec_of_ne]
   rcases (para_vec qdr_nd.edge_nd₃₄.toVecND qdr_nd.edge_nd₁₂.toVecND para) with ⟨c,eq'⟩
   have eq'' : (VEC qdr_nd.point₃ qdr_nd.point₄) = c • (VEC qdr_nd.point₁ qdr_nd.point₂) := eq'

EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean

@@ -47,13 +47,13 @@ def evalPerm_collinear : Tactic := fun stx =>
       catch
         _ => pure ()
       try
-        let t <- `(tactic| refine Collinear.perm₂₃₁ $x0)
+        let t <- `(tactic| refine Collinear.perm₃₁₂ $x0)
         evalTactic t
         return
       catch
         _ => pure ()
       try
-        let t <- `(tactic| refine Collinear.perm₃₁₂ $x0)
+        let t <- `(tactic| refine Collinear.perm₂₃₁ $x0)
         evalTactic t
         return
       catch