Merge pull request #2 from Thmoas-Guan/master

angle_trash

EuclideanGeometry/Example/SCHAUM/Problem1.1.lean

@@ -17,16 +17,17 @@ variable {A B C : P} {hnd: ¬ colinear A B C} {hisoc: (▵ 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$
-variable {E : P} {E_on_seg: E LiesInt (SEG A B)}
+variable {E : P} {E_on_seg: E LiesInt (SEG A C)}
 --such that $AE = AD$.
 variable {E_ray_position : (SEG A E).length = (SEG A D).length}
 --Let $M$ be the midpoint of $BC$.
 variable {M : P} {median_M_position : M = (SEG B C).midpoint}
 --Prove that $DM = EM$.
 theorem Problem1_1_ : (SEG D M).length = (SEG E M).length := by
-  --the first edge of congruence
   have h₀ : (SEG A B).length = (SEG A C).length := by
-    sorry
+    calc
+      _ = (SEG C A).length := hisoc.symm
+      _ = (SEG A C).length := length_eq_length_of_rev (SEG C A)
   have h₁ : ¬ colinear B D M := by sorry
   have h₂ : ¬ colinear C E M := by sorry
   --to confirm the definition of angle is not invalid
@@ -41,21 +42,28 @@ theorem Problem1_1_ : (SEG D M).length = (SEG E M).length := by
   --the second edge of congruence
   have h₃ : (SEG B D).length = (SEG C E).length := by
     calc
-      (SEG B D).length = (SEG A B).length - (SEG A D).length := by
-        sorry
+      (SEG B D).length = (SEG D B).length := length_eq_length_of_rev (SEG B D)
+      _=(SEG A B).length - (SEG A D).length := by
+        rw [← eq_sub_of_add_eq']
+        rw []
+        exact (length_eq_length_add_length (SEG A B) D (D_on_seg)).symm
       _= (SEG A C).length - (SEG A D).length := by rw [h₀]
       _= (SEG A C).length - (SEG A E).length := by rw [E_ray_position]
-      _= (SEG C E).length := by
-        sorry
+      _= (SEG E C).length := by
+        rw [← eq_sub_of_add_eq']
+        exact (length_eq_length_add_length (SEG A C) E (E_on_seg)).symm
+      _= (SEG C E).length := length_eq_length_of_rev (SEG E C)
   have h₄ : (SEG M B).length = (SEG M C).length := by
-    have h₄₁ : (SEG M B).length = (SEG B M).length := by sorry
+    have h₄₁ : (SEG M B).length = (SEG B M).length := length_eq_length_of_rev (SEG M B)
     rw[h₄₁]
     rw [median_M_position]
     apply dist_target_eq_dist_source_of_midpt
   have h₅ : ∠ D B M (d_ne_b) (m_ne_b) = -∠ E C M (e_ne_c) (m_ne_c) := by
-    have h₅₁ : -∠ E C M (e_ne_c) (m_ne_c) = -∠ A C B (a_ne_c) (b_ne_c) := by sorry
+    have h₅₁ : -∠ E C M (e_ne_c) (m_ne_c) = -∠ A C B (a_ne_c) (b_ne_c) := by
+      sorry
     rw [h₅₁]
-    have h₅₂ : ∠ D B M (d_ne_b) (m_ne_b) = -∠ C B A (c_ne_b) (a_ne_b) := by sorry
+    have h₅₂ : ∠ D B M (d_ne_b) (m_ne_b) = -∠ C B A (c_ne_b) (a_ne_b) := by
+      sorry
     rw [h₅₂]
     have h₅₃ : ∠ C B A (c_ne_b) (a_ne_b) = ∠ A C B (a_ne_c) (b_ne_c) := by
       apply (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (tri_nd := ⟨▵ A B C, hnd⟩)).mp

EuclideanGeometry/Example/SCHAUM/Problem1.3.lean

@@ -23,10 +23,41 @@ variable {D_E_seg_position : (SEG B D).length = (SEG C E).length}
 --B ≠ A and C ≠ A by hnd
 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 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 b_ne_c : B ≠ C := (ne_of_not_colinear hnd).1.symm
+lemma c_ne_b : C ≠ B := (ne_of_not_colinear hnd).1
 --D ≠ A and E ≠ A
 lemma d_ne_a : D ≠ A := sorry
 lemma e_ne_a : E ≠ A := sorry
+lemma d_ne_b : D ≠ B := sorry
+lemma e_ne_c : E ≠ C := sorry
 --Prove that $DM = EM$.
-theorem Problem1_3_ : ∠ D A B (d_ne_a) (b_ne_a (hnd := hnd))= ∠ C A E (c_ne_a (hnd := hnd)) (e_ne_a) := sorry
-
+theorem Problem1_3_ : ∠ D A B (d_ne_a) (b_ne_a (hnd := hnd))= ∠ C A E (c_ne_a (hnd := hnd)) (e_ne_a) := by
+  --the first edge of congruence
+  have h₀ : (SEG B A).length = (SEG C A).length := by
+    calc
+      _= (SEG A B).length := length_eq_length_of_rev (SEG B A)
+      _= (SEG C A).length := hisoc.symm
+  have hnd₁ : ¬ colinear B A D := by sorry
+  have hnd₂ : ¬ colinear C A E := by sorry
+  have h₁ : (SEG D B).length = (SEG E C).length := by
+    calc
+      _= (SEG B D).length := length_eq_length_of_rev (SEG D B)
+      _= (SEG C E).length := D_E_seg_position
+      _= (SEG E C).length := length_eq_length_of_rev (SEG C E)
+  have h₂ : ∠ A B D (a_ne_b (hnd := hnd)) (d_ne_b) = -∠ A C E (a_ne_c (hnd := hnd)) (e_ne_c) := by
+    have h₂₁ : ∠ A B D (a_ne_b (hnd := hnd)) (d_ne_b) = -∠ C B A (c_ne_b (hnd := hnd)) (a_ne_b (hnd := hnd)) := by sorry
+    have h₂₂ : ∠ A C E (a_ne_c (hnd := hnd)) (e_ne_c) = ∠ A C B (a_ne_c (hnd := hnd)) (b_ne_c (hnd := hnd)) := by sorry
+    rw[h₂₁]
+    rw[h₂₂]
+    have h₂₀ : ∠ C B A (c_ne_b (hnd := hnd)) (a_ne_b (hnd := hnd)) = ∠ A C B (a_ne_c (hnd := hnd)) (b_ne_c (hnd := hnd)) := by
+      apply (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (tri_nd := ⟨▵ A B C, hnd⟩)).mp
+      exact hisoc
+    rw[← h₂₀]
+  have h₃ : TRI_nd B A D hnd₁ ≅ₐ TRI_nd C A E hnd₂ := by
+    apply Triangle_nd.acongr_of_SAS
+    · exact h₁
+    · exact h₂
+    · exact h₀
 end Problem1_3_

EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean

@@ -12,6 +12,8 @@ theorem start_ray_todir_rev_todir_of_ang_rev_ang {ang₁ ang₂ : Angle P} (hs :
 
 theorem angle_value_eq_angle (A : P) (ray : Ray P) (h : A ≠ ray.1) : (Angle.mk_ray_pt ray A h).value = Vec_nd.angle ray.2.toVec_nd (VEC_nd ray.source A h) := sorry
 
-theorem angle_slide_vertice (A A' B B' O: P) (h₁ : A ≠ O) (h₂ : B ≠ O) (h₁' : A' ≠ O) (h₂' : B' ≠ O) (LiesInt1 : A' LiesInt (RAY O A h₁) )  (LiesInt2 :  B' LiesInt (RAY O B h₂) ) : ANG A O B h₁ h₂ = ANG A' O B' h₁' h₂' := sorry
+theorem eq_ang_of_lieson_lieson {A A' B B' O: P} (h₁ : A ≠ O) (h₂ : B ≠ O) (h₁' : A' ≠ O) (h₂' : B' ≠ O) (LiesInt1 : A' LiesInt (RAY O A h₁) )  (LiesInt2 :  B' LiesInt (RAY O B h₂) ) : ANG A O B h₁ h₂ = ANG A' O B' h₁' h₂' := sorry
+
+theorem neg_value_of_rev_ang {A B O: P} (h₁ : A ≠ O) (h₂ : B ≠ O) : ∠ A O B h₁ h₂ = -∠ B O A h₂ h₁ := sorry
 
 end EuclidGeom