example

EuclideanGeometry/Example/SCHAUM/Probelm1.13.lean

@@ -0,0 +1,38 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {Plane : Type _} [EuclideanPlane Plane]
+
+namespace SCHAUM_Problem_1_13
+/-
+Let $ABCD$ be a parallelogram in which the diagonals $AC$ and $BD$ meet at $M$. Let $P$ and $Q$ be points on $AM$ and $MC$, respectively, such that $MP = MQ$.
+
+Prove that $PBQD$ is a parallelogram.
+-/
+
+-- Let $ABCD$ be a parallelogram.
+variable {A B C D : Plane} {hprg : Quadrilateral.IsParallelogram (QDR A B C D)}
+-- The diagonals $AC$ and $BD$ meet at $M$.
+variable {M : Plane} {hm : M = Quadrilateral_cvx.diag_inx (QDR_cvx A B C D (is_convex_of_is_prg hprg))}
+-- Let $P$ and $Q$ be points on $AM$ and $MC$, respectively, such that $MP = MQ$.
+variable {P Q : Plane} {hp : Seg.IsInt P (SEG A M)} {hq : Seg.IsInt Q (SEG M C)} {hpq : (SEG P M).length = (SEG M Q).length}
+-- State the main goal.
+theorem SCHAUM_Problem_1_13 : Quadrilateral.IsParallelogram (QDR P B Q D) := by
+  have m1 : M = (SEG B D).midpoint := by
+    rw [hm]
+    apply eq_midpt_of_diag_inx_of_is_prg'
+    · sorry
+    · exact hprg
+  have m2 : M = (SEG P Q).midpoint := by
+    apply (eq_midpoint_iff_in_seg_and_dist_target_eq_dist_source M (SEG P Q)).mpr
+    constructor
+    · sorry
+    · simp
+      exact hpq
+  apply is_prg_of_diag_inx_eq_mid_eq_mid
+  rw [← m1, ← m2]
+
+end SCHAUM_Problem_1_13

EuclideanGeometry/Example/SCHAUM/Problem1.1.lean

@@ -0,0 +1,79 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {P : Type _} [EuclideanPlane P]
+
+namespace Problem_1_1
+/-Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.Let $D$ be a point on $AB$.
+Let $E$ be a point on $AC$ such that $AE = AD$. Let $M$ be the midpoint of $BC$.
+
+Prove that $DM = EM$.
+-/
+--Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
+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 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 Problem_1_1 : (SEG D M).length = (SEG E M).length := by
+  have h₀ : (SEG A B).length = (SEG A C).length := by
+    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
+  have d_ne_b : D ≠ B := (ne_of_not_colinear h₁).2.2
+  have m_ne_b : M ≠ B := (ne_of_not_colinear h₁).2.1.symm
+  have e_ne_c : E ≠ C := (ne_of_not_colinear h₂).2.2
+  have m_ne_c : M ≠ C := (ne_of_not_colinear h₂).2.1.symm
+  have a_ne_b : A ≠ B := (ne_of_not_colinear hnd).2.2.symm
+  have c_ne_b : C ≠ B := (ne_of_not_colinear hnd).1
+  have a_ne_c : A ≠ C := (ne_of_not_colinear hnd).2.1
+  have b_ne_c : B ≠ C := (ne_of_not_colinear hnd).1.symm
+  --the second edge of congruence
+  have h₃ : (SEG B D).length = (SEG C E).length := by
+    calc
+      (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 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 := 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
+    rw [h₅₁]
+    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
+      exact hisoc
+    rw [h₅₃]
+  have h₆ :  TRI_nd B D M h₁ ≅ₐ TRI_nd C E M h₂ := by
+    apply Triangle_nd.acongr_of_SAS
+    · exact h₄
+    · exact h₅
+    · exact h₃
+
+  exact h₆.edge₁
+end Problem_1_1

EuclideanGeometry/Example/SCHAUM/Problem1.10.lean

@@ -0,0 +1,27 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {Plane : Type _} [EuclideanPlane Plane]
+
+namespace SCHAUM_Problem_1_10
+/-
+Let $ABCD$ be a parallelogram. Let $P$ be the foot of the perpendicular from $A$ to the line $CD$,and let $Q$ be the foot of the perpendicular from $C$ to the line $AB$.
+
+Prove that $APCQ$ is a rectangle.
+-/
+
+-- Let $ABCD$ be a parallelogram.
+variable {A B C D : Plane} {hprg : Quadrilateral.IsParallelogram (QDR A B C D)}
+-- Let $P$ be the foot of the perpendicular from $A$ to the line $CD$.
+lemma d_ne_c : D ≠ C := sorry
+variable {P : Plane} {hppf : P = perp_foot A (LIN C D d_ne_c)}
+-- Let $Q$ be the foor of the perpendicular from $C$ to the line $AB$.
+lemma b_ne_a : B ≠ A := sorry
+variable {Q : Plane} {hqpf : Q = perp_foot C (LIN A B b_ne_a)}
+-- State the main goal.
+-------- theorem SCHAUM_Problem_1_10 : Quadrilateral.IsRectangle (QDR A P C Q) := by sorry
+
+end SCHAUM_Problem_1_10

EuclideanGeometry/Example/SCHAUM/Problem1.11.lean

@@ -0,0 +1,22 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {Plane : Type _} [EuclideanPlane Plane]
+
+namespace SCHAUM_Problem_1_11
+/-
+If $ABCD$ is a parallelogram and $CDEF$ is a parallelogram, then $ABFE$ is a parallelogram.
+-/
+
+-- $ABCD$ is a parallelogram.
+variable {A B C D : Plane} {hprg1 : Quadrilateral.IsParallelogram (QDR A B C D)}
+-- $CDEF$ is a parallelogram.
+variable {E F : Plane} {hprg2 : Quadrilateral.IsParallelogram (QDR C D E F)}
+-- State the main goal.
+theorem SCHAUM_Problem_1_11 : Quadrilateral.IsParallelogram (QDR A B F E) := by
+  sorry
+
+end SCHAUM_Problem_1_11

EuclideanGeometry/Example/SCHAUM/Problem1.12.lean

@@ -0,0 +1,45 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {Plane : Type _} [EuclideanPlane Plane]
+
+namespace SCHAUM_Problem_1_12
+/-
+Let $ABCD$ is a convex quadrilateral. Assume that the diagonal $BD \perp BC$ and $BD \perp DA$.
+Suppose that $BC = DA$.
+
+Prove that $ABCD$ is a parallelogram.
+-/
+
+-- Let $ABCD$ is a convex quadrilateral.
+variable {A B C D : Plane} {hconv : Quadrilateral.IsConvex (QDR A B C D)}
+-- The diagonal $BD \perp BC$.
+lemma d_ne_b : D ≠ B := Quadrilateral_cvx.nd₂₄ (Quadrilateral_cvx.mk_is_convex hconv)
+lemma c_ne_b : C ≠ B := Quadrilateral_cvx.nd₂₃ (Quadrilateral_cvx.mk_is_convex hconv)
+variable {hperp1 : (SEG_nd B D (d_ne_b (hconv := hconv))) ⟂ (SEG_nd B C (c_ne_b (hconv := hconv)))}
+-- The diagonal $BD \perp DA$.
+lemma a_ne_d : A ≠ D := (Quadrilateral_cvx.nd₁₄ (Quadrilateral_cvx.mk_is_convex hconv)).symm
+variable {hperp2 : (SEG_nd B D (d_ne_b (hconv := hconv))) ⟂ (SEG_nd A D (a_ne_d (hconv := hconv)).symm)}
+-- $BC = DA$.
+variable {heq : (SEG B C).length = (SEG A D).length}
+-- State the main goal.
+theorem SCHAUM_Problem_1_12 : Quadrilateral.IsParallelogram (QDR A B C D) := by
+  apply is_prg_of_para_eq_length'
+  · unfold perpendicular at *
+    unfold parallel
+    have h : toProj (SEG_nd B C (c_ne_b (hconv := hconv))) = toProj (SEG_nd A D (a_ne_d (hconv := hconv)).symm) := by
+      calc
+        _ = (toProj (SEG_nd B C (c_ne_b (hconv := hconv)))).perp.perp := by simp
+        _ = (toProj (SEG_nd B D (d_ne_b (hconv := hconv)))).perp := by
+          congr
+          exact hperp1.symm
+        _ = (toProj (SEG_nd A D (a_ne_d (hconv := hconv)).symm)).perp.perp := by congr
+        _ = toProj (SEG_nd A D (a_ne_d (hconv := hconv)).symm) := by simp
+    exact h.symm
+  · exact heq.symm
+  · exact hconv
+
+end SCHAUM_Problem_1_12

EuclideanGeometry/Example/SCHAUM/Problem1.14.lean

@@ -0,0 +1,48 @@
+import EuclideanGeometry.Foundation.Index
+import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular_trash
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {Plane : Type _} [EuclideanPlane Plane]
+
+namespace SCHAUM_Problem_1_14
+/-
+Let $ABCD$ be a parallelogram. Let $P$ and $Q$ be points on the segments $AB$ and $CD$, respectively, such that $BP = DQ$. Let $M$ be the foot of the perpendicular from $P$ to the diagonal $BD$, and let $N$ be the foot of the perpendicular from $Q$ to the diagonal $BD$
+
+Prove that $PM = QN$ and $PM \parallel QN$.
+-/
+
+-- Let $ABCD$ be a parallelogram.
+variable {A B C D : Plane} {hprg : Quadrilateral.IsParallelogram (QDR A B C D)}
+-- Let $P$ and $Q$ be points on the segments $AB$ and $CD$, respectively, such that $BP = DQ$.
+variable {P Q : Plane} {hp : Seg.IsInt P (SEG A B)} {hq : Seg.IsInt Q (SEG C D)} {hpq : (SEG B P).length = (SEG D Q).length}
+-- Let $M$ be the foot of the perpendicular from $P$ to the diagonal $BD$.
+lemma d_ne_b : D ≠ B := Quadrilateral_cvx.nd₂₄ (Quadrilateral_cvx.mk_is_convex (is_convex_of_is_prg hprg))
+lemma hp1 : ¬ (P LiesOn (LIN B D (d_ne_b (hprg := hprg)))) := by sorry
+variable {M : Plane} {hm : M = perp_foot P (LIN B D d_ne_b)}
+-- Let $N$ be the foot of the perpendicular from $Q$ to the diagonal $BD$.
+lemma hp2 : ¬ (Q LiesOn (LIN B D (d_ne_b (hprg := hprg)))) := by sorry
+variable {N : Plane} {hn : N = perp_foot Q (LIN B D d_ne_b)}
+-- State the main goal.
+lemma m_ne_p : M ≠ P := by sorry
+lemma n_ne_q : N ≠ Q := by sorry
+theorem SCHAUM_Problem_1_14 : (SEG P M).length = (SEG Q N).length ∧ ((SEG_nd P M m_ne_p) ∥ (SEG_nd Q N n_ne_q)) := by
+  constructor
+  · sorry
+  · unfold parallel
+    have h₁ : (LIN P M m_ne_p) ⟂ (LIN B D (d_ne_b (hprg := hprg))) := by
+      rw [hm]
+      apply pt_to_perp_foot_perp_line (hp1 (hprg := hprg))
+      · sorry
+      · sorry
+      · sorry
+    have h₂ : (LIN Q N m_ne_p) ⟂ (LIN B D (d_ne_b (hprg := hprg))) := by sorry
+    calc
+      _ = toProj (LIN P M m_ne_p) := by sorry
+      _ = (toProj (LIN B D (d_ne_b (hprg := hprg)))).perp := by sorry
+      _ = toProj (LIN Q N n_ne_q) := by sorry
+      _ = toProj (SEG_nd Q N n_ne_q) := by sorry
+
+end SCHAUM_Problem_1_14

EuclideanGeometry/Example/SCHAUM/Problem1.2.lean

@@ -0,0 +1,74 @@
+import EuclideanGeometry.Foundation.Index
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {Plane : Type _} [EuclideanPlane Plane]
+
+namespace Problem1_2_
+/-Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.Let $D$ be a point on $AB$.
+Let $E$ be a point on $AC$ such that $AE = AD$.Let $P$ be the foot of perpendicular from $D$ to $BC$.
+Let $Q$ be the foot of perpendicular from $E$ to $BC$.
+
+Prove that $DP = EQ$.
+-/
+
+--Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.
+variable {A B C : Plane} {hnd: ¬ colinear A B C} {hisoc: (▵ A B C).IsIsoceles}
+--Let $D$ be a point on $AB$.
+variable {D : Plane} {D_on_seg: D LiesInt (SEG A B)}
+--Let $E$ be a point on $AC$
+variable {E : Plane} {E_on_seg: E LiesInt (SEG A C)}
+--such that $AE = AD$.
+variable {E_ray_position : (SEG A E).length = (SEG A D).length}
+-- Claim:$B \ne C$.
+-- This is because vertices  B C of nondegenerate triangles are distinct.
+lemma b_ne_c : B ≠ C := (ne_of_not_colinear hnd).1.symm
+-- Let $P$ be the foot of perpendicular from $D$ to $BC$.
+variable {P : Plane} {hd : P = perp_foot D (LIN B C b_ne_c.symm)}
+-- Let $Q$ be the foot of perpendicular from $E$ to $BC$.
+variable {Q : Plane} {hd : Q = perp_foot E (LIN B C b_ne_c.symm)}
+-- Prove that $DP = EQ$.
+theorem Problem1_2_ : (SEG D P).length = (SEG E Q).length := by
+  have hisoc' : (SEG A B).length = (SEG A C).length := by
+    calc
+      _ = (SEG C A).length := hisoc.symm
+      _ = (SEG A C).length := length_eq_length_of_rev (SEG C A)
+  have seg1 : (SEG B D).length = (SEG C E).length := by
+    calc
+      _ = (SEG D B).length := by sorry
+      _ = (SEG A B).length - (SEG A D).length := by
+        rw [← eq_sub_of_add_eq']
+        exact (length_eq_length_add_length (SEG A B) D (D_on_seg)).symm
+      _ = (SEG A C).length - (SEG A E).length := by rw [E_ray_position, ← hisoc']
+      _ = (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 a_ne_b : A ≠ B := (ne_of_not_colinear hnd).2.2.symm
+  have a_ne_c : A ≠ C := (ne_of_not_colinear hnd).2.1
+  have c_ne_b : C ≠ B := (ne_of_not_colinear hnd).1
+  have hnd1 : ¬ colinear P B D := by sorry
+  have b_ne_d : B ≠ D := (ne_of_not_colinear hnd1).1.symm
+  have p_ne_d : P ≠ D := (ne_of_not_colinear hnd1).2.1
+  have p_ne_b : P ≠ B := (ne_of_not_colinear hnd1).2.2.symm
+  have hnd2 : ¬ colinear Q C E := by sorry
+  have c_ne_e : C ≠ E := (ne_of_not_colinear hnd2).1.symm
+  have q_ne_e : Q ≠ E := (ne_of_not_colinear hnd2).2.1
+  have q_ne_c : Q ≠ C := (ne_of_not_colinear hnd2).2.2.symm
+  have ang2 : (∠ D B P b_ne_d.symm p_ne_b) = - (∠ E C Q c_ne_e.symm q_ne_c) := by
+    calc
+      _ = ∠ A B C a_ne_b c_ne_b := by sorry
+      _ = ∠ B C A c_ne_b.symm a_ne_c := by sorry
+      _ = - ∠ A C B a_ne_c c_ne_b.symm := by sorry
+      _ = - ∠ E C Q c_ne_e.symm q_ne_c := by sorry
+  have ang1 : (∠ B P D p_ne_b.symm p_ne_d.symm) = - (∠ C Q E q_ne_c.symm q_ne_e.symm) := by sorry
+  have h : IsACongr (TRI_nd P B D hnd1).1 (TRI_nd Q C E hnd2).1 := by
+    apply acongr_of_AAS
+    · exact ang1
+    · exact ang2
+    · exact seg1
+  exact h.edge₂
+
+end Problem1_2_