Merge branch 'master' into master

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean

@@ -0,0 +1,133 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+namespace Congruence_Exercise_ygr
+
+namespace Problem_1
+/-
+$C, D$ lies in segment $BF$, $AB \parallel DE$, $AB = DF$, $BC = DE$.
+
+Prove that $∠ BAC = ∠ EFD$.
+-/
+structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
+  -- $C, D$ lies in segment $BF$, they lies on the same line $l$.
+  B : Plane
+  C : Plane
+  D : Plane
+  F : Plane
+  B_ne_F : PtNe B F
+  C_int : C LiesInt (SEG_nd B F)
+  D_int : D LiesInt (SEG_nd B F)
+  -- $A, E$ do not lie on $l$.
+  A : Plane
+  E : Plane
+  ABC_nd : ¬colinear A B C
+  EDF_nd : ¬colinear 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)
+  -- $AB = DF$
+  h₁ : (SEG A B).length = (SEG D F).length
+  -- $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
+  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
+  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 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
+  -- $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
+  /-
+  $\angle ABC$ and $\angle EDF$ are corresponding angles,thus equal.
+  In $\triangle BAC \congr_a \triangle DFE$.
+  $\cdot CB = ED$
+  $\cdot \angle ABC = -\angle FDE$
+  $\cdot BA = DF$
+  We have $\triangle BAC \congr_a \triangle DFE$.
+  Thus $\angle CAB = -\angle EFD$
+  By anti-symm we proven.
+  -/
+  -- $CB = BC = DE = ED$.
+  have e₂ : (SEG e.C e.B).length = (SEG e.E e.D).length := by
+    simp only [length_of_rev_eq_length', e.h₂, length_of_rev_eq_length']
+  --$\angle ABC$ = -$\angle FDE$
+  have a₁ : ∠ e.A e.B e.C  = -∠ e.F e.D e.E := by
+    -- $\angle ABC$ and $\angle EDF$ are corresponding angles.
+    have hCrsp : IsCorrespondingAng (ANG e.A e.B e.C) (ANG e.E e.D e.F) := by
+      constructor
+      --same Dir for start ray and same DirLine for end ray
+      · show (RAY e.B e.A).toDir = (RAY e.D e.E).toDir
+        --by $A,E$ are on the same side of line $B F$ and $AB \parallel DE$
+        apply eq_toDir_of_parallel_and_same_side
+        ·exact e.hpr
+        ·show IsOnSameSide e.A e.E (SEG_nd e.B e.D)
+         have hA : odist e.A (SEG_nd e.B e.D) > 0 := by
+          calc
+            odist e.A (SEG_nd e.B e.D) = odist e.A (SEG_nd e.B e.D).toDirLine := by rfl
+            _=odist e.A (SEG_nd e.B e.F).toDirLine := by
+              have : (SEG_nd e.B e.D).toDirLine = (SEG_nd e.B e.F).toDirLine := by
+                apply eq_toDirLine_of_source_to_pt_lies_int (e.D_int)
+              congr
+            _=odist e.A (SEG_nd e.B e.F) := by rfl
+            _>0 := by exact e.A_side
+         have hE : odist e.E (SEG_nd e.B e.D) > 0 := by
+          calc
+            odist e.E (SEG_nd e.B e.D) = odist e.E (SEG_nd e.B e.D).toDirLine := by rfl
+            _=odist e.E (SEG_nd e.B e.F).toDirLine := by
+              have : (SEG_nd e.B e.D).toDirLine = (SEG_nd e.B e.F).toDirLine := by
+                apply eq_toDirLine_of_source_to_pt_lies_int (e.D_int)
+              congr
+            _=odist e.E (SEG_nd e.B e.F) := by rfl
+            _>0 := by exact e.E_side
+         have hA' : e.A LiesOnLeft (SEG_nd e.B e.D) := by exact hA
+         have hE' : e.E LiesOnLeft (SEG_nd e.B e.D) := by exact hE
+         unfold IsOnSameSide
+         unfold IsOnSameSide'
+         show e.A LiesOnLeft (SEG_nd e.B e.D) ∧ e.E LiesOnLeft (SEG_nd e.B e.D) ∨ e.A LiesOnRight (SEG_nd e.B e.D) ∧ e.E LiesOnRight (SEG_nd e.B e.D)
+         simp only [hA', hE', and_self, true_or]
+        ·exact D_ne_B.out.symm
+      · show (RAY e.B e.C).toDirLine = (RAY e.D e.F).toDirLine
+        calc
+          _=(SEG_nd e.B e.F).toDirLine := by
+            apply eq_toDirLine_of_source_to_pt_lies_int (e.C_int)
+          _=(SEG_nd e.D e.F).toDirLine := by
+            symm
+            apply eq_toDirLine_of_pt_lies_int_to_target (e.D_int)
+    -- Then $∠ ABC = ∠ EDF = -∠ FDE$.
+    calc
+      _ = ∠ e.E e.D e.F := eq_value_of_iscorrespondingang hCrsp --corresponding angle
+      _ = _ := by apply neg_value_of_rev_ang --anti-symm
+  --$BA = DF$
+  have e₃ : (SEG e.B e.A).length = (SEG e.D e.F).length := by
+    rw [length_of_rev_eq_length']
+    exact e.h₁
+  -- We have $\triangle BAC \congr_a \triangle DFE$.
+  have h :  (TRI_nd e.B e.A e.C hnd₁) ≅ₐ (TRI_nd e.D e.F e.E hnd₂) := by
+    apply TriangleND.acongr_of_SAS
+    · exact e₂
+    · exact a₁
+    · exact e₃
+  calc
+    _ = - ∠ e.C e.A e.B := by apply neg_value_of_rev_ang
+    _ = ∠ e.E e.F e.D  := by
+      have : ∠ e.C e.A e.B  = - ∠ e.E e.F e.D := h.angle₂
+      rw [this, neg_neg]
+end Problem_1
+end Congruence_Exercise_ygr

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean

@@ -0,0 +1,70 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+namespace Congruence_Exercise_ygr
+
+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
+  -- $AB = DC$, $DB = AC$.
+  A : Plane
+  B : Plane
+  C : Plane
+  D : Plane
+  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
+  -- $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
+-- 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$.
+  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
+    · calc
+        _ = (SEG e.A e.B).length := length_of_rev_eq_length'
+        _ = (SEG e.D e.C).length := e.h₁
+        _ = _ := length_of_rev_eq_length'
+    · exact length_of_rev_eq_length'
+    · exact e.h₂
+    · have clock : ¬ (TRI_nd e.D e.B e.A e.hnd₁).is_cclock := by
+        have : (IsOnLeftSide e.B (SEG_nd e.A e.D e.D_ne_A)) ↔ (TRI_nd e.D e.B e.A e.hnd₁).is_cclock := by
+          simp [TriangleND.iscclock_iff_liesonleft₂]
+          rfl
+        apply this.not.mp
+        unfold IsOnLeftSide
+        have hb : odist e.B (SEG_nd e.A e.D e.D_ne_A) < 0 := by exact e.B_side
+        linarith
+      have cclock : (TRI_nd e.A e.C e.D e.hnd₂).is_cclock := by
+        have : (IsOnLeftSide e.C (SEG_nd e.D e.A e.D_ne_A.symm)) ↔ (TRI_nd e.A e.C e.D e.hnd₂).is_cclock := by
+          simp [TriangleND.iscclock_iff_liesonleft₂]
+          rfl
+        apply this.mp
+        have rev : odist e.C (SEG_nd e.D e.A e.D_ne_A.symm) = - odist e.C (SEG_nd e.A e.D e.D_ne_A) := by
+          have : (SEG_nd e.D e.A e.D_ne_A.symm) = (SEG_nd e.A e.D e.D_ne_A).reverse := by rfl
+          simp only [this]
+          apply odist_reverse_eq_neg_odist (df := (SEG_nd e.A e.D e.D_ne_A))
+        unfold IsOnLeftSide
+        simp only [rev, Left.neg_pos_iff, gt_iff_lt]
+        exact e.C_side
+      simp only [clock, cclock, not_true_eq_false]
+  · exact h.angle₂
+
+
+
+end Problem_2
+end Congruence_Exercise_ygr

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean

@@ -0,0 +1,87 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+namespace Congruence_Exercise_ygr
+
+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
+  --In (convex) quadrilateral $A B D C$,$AB = AC$, $BD = CD$.
+  A : Plane
+  B : Plane
+  C : Plane
+  D : Plane
+  cvx_ABDC : (QDR A B D C).IsConvex
+  AB_eq_AC : (SEG A B).length = (SEG A C).length
+  BD_eq_CD : (SEG B D).length = (SEG C D).length
+  --$A \ne B$ and $D \ne B$ for $\angle A B D$
+  A_ne_B : A ≠ B := (Quadrilateral_cvx.nd₁₂ (QDR_cvx A B D C cvx_ABDC)).symm
+  D_ne_B : D ≠ B := (Quadrilateral_cvx.nd₂₃ (QDR_cvx A B D C cvx_ABDC))
+  --$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
+  /-
+  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$
+  $\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 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$.
+  have isoc_ABC_ang : ∠ e.C e.B e.A (C_ne_B) (e.A_ne_B) = ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm) := by
+    have isoc_ABC : (▵ e.A e.B e.C).IsIsoceles := by
+      unfold Triangle.IsIsoceles
+      show (SEG e.C e.A).length = (SEG e.A e.B).length
+      calc
+        (SEG e.C e.A).length = (SEG e.A e.C).length := length_of_rev_eq_length'
+        _= (SEG e.A e.B).length := e.AB_eq_AC.symm
+    apply (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (tri_nd := ⟨▵ e.A e.B e.C, h₁⟩)).mp
+    exact isoc_ABC
+  --Because $DB = DC$ ,we have $\angle D B C = -\angle D C B$
+  have isoc_DBC_ang : ∠ e.C e.B e.D (C_ne_B) (e.D_ne_B) = ∠ e.D e.C e.B (e.D_ne_C) (C_ne_B.symm) := by
+    have isoc_DBC : (▵ e.D e.B e.C).IsIsoceles := by
+      unfold Triangle.IsIsoceles
+      show (SEG e.C e.D).length = (SEG e.D e.B).length
+      calc
+        (SEG e.C e.D).length = (SEG e.B e.D).length := e.BD_eq_CD.symm
+        _= (SEG e.D e.B).length := length_of_rev_eq_length'
+    apply (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (tri_nd := ⟨▵ e.D e.B e.C, h₂⟩)).mp
+    exact isoc_DBC
+  --$\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 : ∠  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
+    have triv₁ : (RAY e.B e.C C_ne_B) = (RAY e.B e.C C_ne_B) := by rfl
+    have triv₂ : (RAY e.C e.B C_ne_B.symm) = (RAY e.C e.B C_ne_B.symm) := by rfl
+    have h' : ∠ e.D e.B e.A (e.D_ne_B) (e.A_ne_B) = ∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C) := by
+      calc
+        _=∠ e.D e.B e.C (e.D_ne_B) (C_ne_B) + ∠ e.C e.B e.A (C_ne_B) (e.A_ne_B)  := by
+          apply Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang (ANG  e.D e.B e.C (e.D_ne_B) (C_ne_B)) (ANG e.C e.B e.A (C_ne_B) (e.A_ne_B)) (triv₁)
+        _=-∠ e.C e.B e.D (C_ne_B) (e.D_ne_B) + ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm):= by
+          simp only [isoc_ABC_ang]
+          simp only [neg_value_of_rev_ang (e.D_ne_B) (C_ne_B)]
+        _=-∠ e.D e.C e.B (e.D_ne_C) (C_ne_B.symm) + ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm):= by
+          simp only [isoc_DBC_ang]
+        _=∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm) + ∠ e.B e.C e.D (C_ne_B.symm) (e.D_ne_C) := by
+          simp only[neg_value_of_rev_ang (e.D_ne_C) (C_ne_B.symm)]
+          abel
+        _=∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C) := by
+          symm
+          apply Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang (ANG  e.A e.C e.B (e.A_ne_C) (C_ne_B.symm)) (ANG e.B e.C e.D (C_ne_B.symm) (e.D_ne_C)) (triv₂)
+    simp only [← h']
+    simp only[neg_value_of_rev_ang (e.A_ne_B) (e.D_ne_B)]
+  exact h
+end Problem_3
+end Congruence_Exercise_ygr