From 905e90a9e7a0bb78216edb34589d0772c717b1c2 Mon Sep 17 00:00:00 2001 From: xyzw12345 <148849549+xyzw12345@users.noreply.github.com> Date: Mon, 22 Jan 2024 11:19:25 +0800 Subject: [PATCH] added Linear.Order (#300) * upd congr_ex_6&7 * Update Congruence_exercise_ygr_7.lean * finished prove of congr_exercise_ygr_6 * modify several thm in trash * upd proof of 7 * upd on Congr_ex_ygr_7 * merge from upstream and lean upd 20240112 * upd problem_5 line_trash add theorems about linear order into line_trash * Update Problem_5.lean * upd on problem 5 and open Order.lean * Update Order.lean * Update Problem_5.lean * upd 20240115 * upd on problem_11 and Order.lean * Update Order.lean * upd order.lean * Update Order.lean * Update Order.lean deleted theorems starting with MEOW * Update Order.lean updated theorems on linear order and LiesInt/LiesOn ray * Update Order.lean updated corollaries OVO and QWQ * update Order.lean added corollaries OVO_1 OVO_2 QWQ_1 QWQ_2 * Update Order.lean * Update Order.lean updated proofs of corollaries * Update Order.lean renamed theorems with HAHAHA, HOHOHO, QAQ and QWQ * Update Order.lean added several theorems to prove according to the plan * Update Order.lean added theorems to prove according to plan * Update Order.lean updated a part of the proof for lies_int_seg_nd_ext_iff_lies_int * Update Order.lean proved theorem lies_int_seg_nd_ext_iff_lies_int and lies_on_seg_nd_ext_iff_lies_on * Update Order.lean finished Order.lean * upd before PR updated Angle_ex_trash and moved two theorems to IsocelesTriangle_trash moved lemmas about collinearity in Linear.Order to Linear.Line updated Index * Update Line.lean --- .../Congruence_Exercise_ygr/Problem_11.lean | 103 +++ .../Congruence_Exercise_ygr/Problem_5.lean | 190 ++++ .../Congruence_Exercise_ygr/Problem_6.lean | 146 ++- .../Congruence_Exercise_ygr/Problem_7.lean | 187 ++-- .../Example/SCHAUM/Problem1.5.lean | 62 +- .../Example/SCHAUM/Problem1.7.lean | 3 +- .../Axiom/Basic/Angle/FromMathlib.lean | 3 +- .../Foundation/Axiom/Linear/Line.lean | 42 + .../Foundation/Axiom/Linear/Order.lean | 868 ++++++++++++++++++ .../Axiom/Position/Angle_ex_trash.lean | 12 +- .../Axiom/Triangle/Congruence_trash.lean | 1 + .../Triangle/IsocelesTriangle_trash.lean | 4 + .../Polygon/Parallelogram_trash.lean | 2 +- .../Triangle/Orthocenter_trash.lean | 13 + EuclideanGeometry/Foundation/Index.lean | 1 + 15 files changed, 1498 insertions(+), 139 deletions(-) create mode 100644 EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_11.lean create mode 100644 EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_5.lean create mode 100644 EuclideanGeometry/Foundation/Axiom/Linear/Order.lean create mode 100644 EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter_trash.lean diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_11.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_11.lean new file mode 100644 index 00000000..3fa3024c --- /dev/null +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_11.lean @@ -0,0 +1,103 @@ +import EuclideanGeometry.Foundation.Index +import EuclideanGeometry.Foundation.Axiom.Linear.Order + +noncomputable section + +namespace EuclidGeom + +namespace Problem_11 + +/- +Let $l$ be a directed line on the plane. +Let $B, E, C, F$ be four points on $l$ in this order. +Let $A, D$ be two points on the plane such that they lies on the same side of $l$. +If $AB = DF$, $AC = DE$ and $BE = CF$, prove that $\angle BAC = - \angle FDE$. +-/ + +structure Setting (Plane : Type _) [EuclideanPlane Plane] where +-- Let $l$ be a directed line on the plane + l : DirLine Plane +-- Let $B, E, C, F$ be four points on $l$ in this order. + B : Plane + E : Plane + C : Plane + F : Plane + B_on_l : B LiesOn l + E_on_l : E LiesOn l + C_on_l : C LiesOn l + F_on_l : F LiesOn l + B_lt_E_on_l : (⟨B, B_on_l⟩ : l.carrier.Elem) < ⟨E, E_on_l⟩ + E_lt_C_on_l : (⟨E, E_on_l⟩ : l.carrier.Elem) < ⟨C, C_on_l⟩ + C_lt_F_on_l : (⟨C, C_on_l⟩ : l.carrier.Elem) < ⟨F, F_on_l⟩ +-- Let $A, D$ be two points on the plane, + A : Plane + D : Plane +-- such that they lies on different sides of $l$, + A_D_IsOnSameSide_l : IsOnSameSide A D l +-- $AB = DF$, + AB_eq_DF : (SEG A B).length = (SEG D F).length +-- $AC = DE$, + AC_eq_DE : (SEG A C).length = (SEG D E).length +-- $BE = CF$. + BE_eq_CF : (SEG B E).length = (SEG C F).length +lemma B_ne_C' {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.B ≠ e.C := by + apply (DirLine.ne_iff_ne_as_line_elem e.B_on_l e.C_on_l).mpr; apply ne_of_lt; + calc + (⟨e.B, e.B_on_l⟩ : e.l.carrier.Elem) + _< ⟨e.E, e.E_on_l⟩ := e.B_lt_E_on_l + _< ⟨e.C, e.C_on_l⟩ := e.E_lt_C_on_l +instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : PtNe e.B e.C := ⟨B_ne_C'⟩ +lemma E_ne_F' {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.F := by + apply (DirLine.ne_iff_ne_as_line_elem e.E_on_l e.F_on_l).mpr; apply ne_of_lt; + calc + (⟨e.E, e.E_on_l⟩ : e.l.carrier.Elem) + _< ⟨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⟩ + +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 + +-- 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 + have E_int_BC : e.E LiesInt (SEG e.B e.C) := by + apply DirLine.lies_int_seg_of_lt_and_lt e.B_on_l e.E_on_l e.C_on_l + exact e.B_lt_E_on_l; exact e.E_lt_C_on_l + have C_int_EF : e.C LiesInt (SEG e.E e.F) := by + apply DirLine.lies_int_seg_of_lt_and_lt e.E_on_l e.C_on_l e.F_on_l + exact e.E_lt_C_on_l; exact e.C_lt_F_on_l + have CB_eq_EF : (SEG e.C e.B).length = (SEG e.E e.F).length := by + calc + _= (SEG e.B e.C).length := by apply length_of_rev_eq_length' + _= (SEG e.B e.E).length + (SEG e.E e.C).length := by + apply length_eq_length_add_length + apply Seg.lies_on_of_lies_int + exact E_int_BC + _= (SEG e.E e.C).length + (SEG e.C e.F).length := by simp only [e.BE_eq_CF]; ring + _= _ := by + symm; + apply length_eq_length_add_length + apply Seg.lies_on_of_lies_int + exact C_int_EF + have BA_eq_FD : (SEG e.B e.A).length = (SEG e.F e.D).length := by + calc + _= (SEG e.A e.B).length := by apply length_of_rev_eq_length' + _= (SEG e.D e.F).length := e.AB_eq_DF + _=_ := by apply length_of_rev_eq_length' + have clockwise_ACB_eq_neg_clockwise_DEF : (TRI_nd e.A e.C e.B e.not_colinear_ACB).is_cclock = ¬(TRI_nd e.D e.E e.F e.not_colinear_DEF).is_cclock := by sorry + have triangle_ACB_acongr_triangle_DEF : (TRI_nd e.A e.C e.B e.not_colinear_ACB) ≅ₐ (TRI_nd e.D e.E e.F e.not_colinear_DEF) := by + apply TriangleND.acongr_of_SSS_of_ne_orientation + · exact CB_eq_EF + · exact BA_eq_FD + · exact e.AC_eq_DE + · exact clockwise_ACB_eq_neg_clockwise_DEF +end Problem_11 + +end EuclidGeom diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_5.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_5.lean new file mode 100644 index 00000000..2486e0f2 --- /dev/null +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_5.lean @@ -0,0 +1,190 @@ +import EuclideanGeometry.Foundation.Index +import EuclideanGeometry.Foundation.Axiom.Linear.Order + +noncomputable section + +namespace EuclidGeom + +namespace Problem_5 + +/- +Let $l$ be a directed line on the plane. +Let $A, F, C, D$ be four points on $l$ in this order. +Let $B, E$ be two points on the plane such that they lies on different sides of $l$, and that $CB \parallel FE$. +If $\angle BAC = \angle EDF$ and $AF = DC$, prove that $AB = DE$. +-/ + +structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +-- Let $l$ be a directed line on the plane + l : DirLine Plane +-- Let $A, F, C, D$ be four points on $l$ in this order. + A : Plane + F : Plane + C : Plane + D : Plane + A_on_l : A LiesOn l + F_on_l : F LiesOn l + C_on_l : C LiesOn l + D_on_l : D LiesOn l + A_lt_F_on_l : (⟨A, A_on_l⟩ : l.carrier.Elem) < ⟨F, F_on_l⟩ + F_lt_C_on_l : (⟨F, F_on_l⟩ : l.carrier.Elem) < ⟨C, C_on_l⟩ + C_lt_D_on_l : (⟨C, C_on_l⟩ : l.carrier.Elem) < ⟨D, D_on_l⟩ +-- Let $B, E$ be two points on the plane, + B : Plane + E : Plane +-- such that they lies on different sides of $l$, + B_E_IsOnOppositeSide_l : IsOnOppositeSide B E l + +-- Claim : $A \ne C$. +lemma A_ne_C' {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.A ≠ e.C := by + apply (DirLine.ne_iff_ne_as_line_elem e.A_on_l e.C_on_l).mpr; apply ne_of_lt; + calc + (⟨e.A, e.A_on_l⟩ : e.l.carrier.Elem) + _< ⟨e.F, e.F_on_l⟩ := e.A_lt_F_on_l + _< ⟨e.C, e.C_on_l⟩ := e.F_lt_C_on_l +instance A_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.C := ⟨A_ne_C'⟩ +-- Claim : $D \ne F$. +lemma D_ne_F' {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.D ≠ e.F := by + symm; apply (DirLine.ne_iff_ne_as_line_elem e.F_on_l e.D_on_l).mpr; apply ne_of_lt; + calc + (⟨e.F, e.F_on_l⟩ : e.l.carrier.Elem) + _< ⟨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 + 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 + _= (LIN e.C e.A) := by + apply Line.eq_line_of_pt_pt_of_ne + apply Line.fst_pt_lies_on_mk_pt_pt + apply Line.snd_pt_lies_on_mk_pt_pt + _=_ := by + apply Line.eq_line_of_pt_pt_of_ne + apply DirLine.lies_on_iff_lies_on_toLine.mpr; exact e.C_on_l + apply DirLine.lies_on_iff_lies_on_toLine.mpr; exact e.A_on_l + have : IsOnOppositeSide e.B e.E (RAY e.C e.A) = IsOnOppositeSide e.B e.E e.l := by + calc + _= IsOnOppositeSide e.B e.E (RAY e.C e.A).toLine := by rfl + _=_ := 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 + 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 + 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 + _= (LIN e.F e.D) := by + apply Line.eq_line_of_pt_pt_of_ne + apply Line.fst_pt_lies_on_mk_pt_pt + apply Line.snd_pt_lies_on_mk_pt_pt + _=_ := by + apply Line.eq_line_of_pt_pt_of_ne + apply DirLine.lies_on_iff_lies_on_toLine.mpr; exact e.F_on_l + apply DirLine.lies_on_iff_lies_on_toLine.mpr; exact e.D_on_l + have : IsOnOppositeSide e.B e.E (RAY e.F e.D) = IsOnOppositeSide e.B e.E e.l := by + calc + _= IsOnOppositeSide e.B e.E (RAY e.F e.D).toLine := by rfl + _=_ := 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 + by_contra h2; absurd h1 + exact perm_colinear_snd_trd_fst h2 +-- 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⟩ +-- 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⟩ +-- 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⟩ +-- 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⟩ + +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 +-- and that $CB \parallel FE$, + CB_parallel_FE : (LIN C B) ∥ (LIN F E) +-- If $\angle BAC = - \angle EDF$, + angle_BAC_eq_angle_EDF : (∠ B A C) = (∠ E D F) +-- and $AF = DC$, + AF_eq_DC : (SEG A F).length = (SEG D C).length +-- Prove that $AB = DE$. + +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 + 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 + 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 + apply (DirLine.ne_iff_ne_as_line_elem e.C_on_l e.F_on_l).mpr; apply ne_of_gt + simp only [e.F_lt_C_on_l] + haveI C_ne_F : PtNe e.C e.F := ⟨C_ne_F'⟩ + have CA_eq_FD : (SEG e.C e.A).length = (SEG e.F e.D).length := by + calc + _= (SEG e.A e.C).length := by apply length_of_rev_eq_length' + _= (SEG e.A e.F).length + (SEG e.F e.C).length := by + apply length_eq_length_add_length + apply Seg.lies_on_of_lies_int + exact F_int_AC + _= (SEG e.D e.C).length + (SEG e.C e.F).length := by congr 1; exact e.AF_eq_DC; exact length_of_rev_eq_length' + _= (SEG e.D e.F).length := by + symm; apply length_eq_length_add_length + apply Seg.lies_on_of_lies_int + exact C_int_DF + _=_ := by apply length_of_rev_eq_length' + have angle_ACB_eq_angle_DFE : (∠ e.A e.C e.B) = (∠ e.D e.F e.E) := by + have dir_CA_eq_neg_dir_FD : (RAY e.C e.A).toDir = - (RAY e.F e.D).toDir := by + calc + _= - e.l.toDir := by + apply DirLine.neg_toDir_of_gt e.C_on_l e.A_on_l + calc + (⟨e.A, e.A_on_l⟩ : e.l.carrier.Elem) + _< ⟨e.F, e.F_on_l⟩ := e.A_lt_F_on_l + _< ⟨e.C, e.C_on_l⟩ := e.F_lt_C_on_l + _=_ := by + simp only [neg_inj]; symm + apply DirLine.eq_toDir_of_lt e.F_on_l e.D_on_l + calc + (⟨e.F, e.F_on_l⟩ : e.l.carrier.Elem) + _< ⟨e.C, e.C_on_l⟩ := e.F_lt_C_on_l + _< ⟨e.D, e.D_on_l⟩ := e.C_lt_D_on_l + have dir_CB_eq_neg_dir_FE : (RAY e.C e.B).toDir = - (RAY e.F e.E).toDir := by + have h : IsOnOppositeSide e.B e.E (SEG_nd e.C e.F) := by + have h1 : (SEG_nd e.C e.F).toLine = e.l := by + calc + _= (LIN e.C e.F) := by + symm; + apply Line.eq_line_of_pt_pt_of_ne + apply SegND.lies_on_toLine_of_lie_on; exact SegND.source_lies_on + apply SegND.lies_on_toLine_of_lie_on; exact SegND.target_lies_on + _=_ := by + apply Line.eq_line_of_pt_pt_of_ne + exact e.C_on_l + exact e.F_on_l + have h2 : IsOnOppositeSide e.B e.E (SEG_nd e.C e.F) = IsOnOppositeSide e.B e.E e.l := by + calc + _= IsOnOppositeSide e.B e.E (SEG_nd e.C e.F).toLine := by rfl + _=_ := by congr + simp only [h2]; exact e.B_E_IsOnOppositeSide_l + apply neg_toDir_of_parallel_and_IsOnOppositeSide + · exact e.CB_parallel_FE + · exact h + apply ang_eq_ang_of_toDir_rev_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 + apply TriangleND.congr_of_ASA + · exact angle_ACB_eq_angle_DFE + · exact CA_eq_FD + · exact e.angle_BAC_eq_angle_EDF + exact triangle_BCA_congr_triangle_EFD.edge₂ +end Problem_5 + +end EuclidGeom diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean index 65f9615c..3e2111b2 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean @@ -1,47 +1,121 @@ import EuclideanGeometry.Foundation.Index +import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex_trash noncomputable section namespace EuclidGeom -variable {P : Type*} [EuclideanPlane P] +namespace Problem_6 -namespace Wuwowuji_Problem_1_6 /- -In $▵ ABC$, $D, E$ are two different points on side $BC$, $AD = AE$, $∠ BAD = -∠ CAE$. +In $\triangle ABC$, let $D$, $E$ be different points on the segment $BC$, such that the points on segment $BC$ are arranged in the order $B, D, E, C$, $AD = AE$ and $\angle BAD = - \angle CAE$. -Prove that $AB = AC$. +Prove that $AB = AC$ -/ --- Define $▵ ABC$. -variable {A B C : P} {hnd1 : ¬ Collinear A B C} --- $D, E$ are two different points on side $BC$. -variable {D E : P} {hd : D LiesInt SEG B C} {he : E LiesInt SEG B C} --- nondegenerate -lemma hnd2 : ¬ Collinear A D E := by sorry -lemma a_ne_b : A ≠ B := by sorry -lemma a_ne_d : A ≠ D := by sorry -lemma a_ne_c : A ≠ C := by sorry -lemma a_ne_e : A ≠ E := by sorry --- $AD = AE$. -variable {hisoc : (TRI_nd A D E hnd2).1.IsIsoceles} --- $∠ BAD = -∠ CAE$. -variable {hang : ∠ B A D a_ne_b a_ne_d = -∠ C A E a_ne_c a_ne_e} --- State the main goal. -theorem Wuwowuji_Problem_1_6 : (SEG A B).length = (SEG A C).length := by - -- nondegenerate - have hnd3 : ¬ Collinear B D A := by sorry - have hnd4 : ¬ Collinear C E A := by sorry - -- Use ASA to prove $▵ BDA ≅ₐ ▵ CEA$. - have h : (TRI_nd B D A hnd3) ≅ₐ (TRI_nd C E A hnd4) := by + +structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +-- Let $\triangle ABC$ be a triangle. + A : Plane + B : Plane + C : Plane + not_colinear_ABC : ¬ colinear A B C +-- Claim : $B \ne A$. + B_ne_A : PtNe B A := ⟨(ne_of_not_colinear not_colinear_ABC).2.2⟩ +-- Claim : $C \ne A$. + C_ne_A : PtNe C A := ⟨(ne_of_not_colinear not_colinear_ABC).2.1.symm⟩ +-- Let $D$ be a point on the segment $BC$. + D : Plane + D_int_BC : D LiesInt (SEG B C) +-- Let $E$ be a point on the segment $BC$, different to $D$. + E : Plane + 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⟩ +-- 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)⟩ +-- 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 : e.D ≠ e.A := by + by_contra h + have h2 : ¬ colinear 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 ⟨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 : e.E ≠ e.A := by + by_contra h + have h2 : ¬ colinear 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 ⟨this⟩ + +structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where +-- such that $AD = AE$. + AD_eq_AE : (SEG A D).length = (SEG A E).length +-- and $\angle BAD = - \angle CAE$ + angle_BAD_eq_neg_angle_CAE : ∠ B A D = - ∠ C A E + +-- 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 + 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.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 + 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 + _= ↑ (π) + (- ∠ e.A e.D e.E) := by abel + _= ↑ (π) + (∠ e.E e.D e.A) := by + congr 1; symm; + apply 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 := (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 + _= (∠ 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 apply TriangleND.acongr_of_ASA - · sorry - · -- $DA = EA$ by condition. - calc - _ = (SEG A D).length := length_of_rev_eq_length' - _ = _ := hisoc.symm - · -- $∠ BAD = -∠ CAE$ by condition. - exact hang - -- $AB = AC$ follows from the congruence. - exact h.edge₂ - -end Wuwowuji_Problem_1_6 + · exact angle_DAB_eq_neg_angle_EAC + · exact e.AD_eq_AE + · exact angle_BDA_eq_neg_angle_CEA + calc + (SEG e.A e.B).length + _= (SEG e.B e.A).length := by apply length_of_rev_eq_length' + _= (SEG e.C e.A).length := triangle_BAD_acongr_triangle_CAE.edge₃ + _= (SEG e.A e.C).length := by apply length_of_rev_eq_length' +end Problem_6 + +end EuclidGeom diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean index 8b4496c6..12bbc886 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean @@ -1,78 +1,135 @@ import EuclideanGeometry.Foundation.Index +import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence_trash +import EuclideanGeometry.Foundation.Axiom.Position.Angle_trash noncomputable section namespace EuclidGeom -variable {P : Type*} [EuclideanPlane P] +namespace Problem_7 -namespace Wuwowuji_Problem_1_7 /- -Segment $AD$ and $BC$ intersect at $O$, $∠ ACB = ∠ ADB$, $OA = OB$. +Let $A, B, C, D$ be four points on the plane such that $A, B, C$ are not colinear, and that $A, B, D$ are not colinear.Let $O$ be the intersection of segment $AD$ and segment $BC$. +If $\angle ACO = - \angle BDO$ and $OA = OB$, Prove that $AD = BC$. +-/ + +structure Setting (Plane : Type _) [EuclideanPlane Plane] where +-- Let $A, B, C, D$ be four points on the plane, + A : Plane + B : Plane + C : Plane + D : Plane +-- such that $A, B, C$ are not colinear, + not_colinear_ABC : ¬ colinear A B C +-- and that $A, B, D$ are not colinear. + not_colinear_ABD : ¬ colinear A B D +-- Let $O$ be the intersection of segment $AD$ and segment $BC$. + O : Plane + O_int_AD : O LiesInt (SEG A D) + O_int_BC : O LiesInt (SEG B C) +-- Claim : $C \ne A$. + C_ne_A : PtNe C A := ⟨(ne_of_not_colinear not_colinear_ABC).2.1.symm⟩ +-- Claim : $D \ne B$. + B_ne_D : PtNe B D := ⟨(ne_of_not_colinear not_colinear_ABD).1.symm⟩ +-- Claim : $O \ne C$. + O_ne_C : PtNe O C := ⟨ne_source_of_lies_int_seg C B O (Seg.lies_int_rev_iff_lies_int.mpr O_int_BC)⟩ +-- Claim : $O \ne D$. + O_ne_D : PtNe O D := ⟨ne_source_of_lies_int_seg D A O (Seg.lies_int_rev_iff_lies_int.mpr O_int_AD)⟩ +-- If $\angle ACO = - \angle BDO$ + angle_OCA_eq_neg_angle_ODB : ∠ O C A = - (∠ O D B) +-- and $OA = OB$. + OA_eq_OB : (SEG O A).length = (SEG O B).length +attribute [instance] Setting.C_ne_A Setting.B_ne_D Setting.O_ne_C Setting.O_ne_D -Prove that $AD = BC$. +theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.A e.D).length = (SEG e.B e.C).length := by +/- +We have $\angle AOC = \angle DOB$ since they are opposite angles, and $\angle DOB = - \angle BOD$ by symmetry. Therefore, $\angle AOC = - \angle BOD$. +We already know that $\angle OCA = - \angle ODB$ and $OA = OB$ in the hypothesis. +In $\triangle COA$ and $\triangle DOB$, +$\cdot \angle AOC = - \angle BOD$ +$\cdot \angle OCA = - \angle ODB$ +$\cdot OA = OB$ +Thus, $\triangle COA \cong_a \triangle DOB$ (by AAS). +So, we have $AD = AO + OD = BO + OC = BC$, since $O$ lies on $AD$ and $O$ lies on $BC$. -/ --- $AD$ and $BC$ intersect at $O$. -variable {A B C D O: P} {h1 : O LiesInt (SEG A D)} {h2 : O LiesInt (SEG B C)} --- nondegenerate -variable {hnd1 : ¬ Collinear C B A} {hnd2 : ¬ Collinear D A B} -lemma a_ne_b : A ≠ B := by sorry -lemma a_ne_c : A ≠ C := by sorry -lemma a_ne_d : A ≠ D := by sorry -lemma b_ne_c : B ≠ C := by sorry -lemma b_ne_d : B ≠ D := by sorry -lemma c_ne_d : C ≠ D := by sorry --- $∠ ACB = ∠ ADB$. -variable {hang : ∠ A C B a_ne_c.symm b_ne_c.symm = ∠ A D B a_ne_d.symm b_ne_d.symm} --- $OA = OB$. -variable {hseg : (SEG O A).length = (SEG O B).length} --- State the main goal. -theorem Wuwowuji_Problem_1_7 : (SEG A D).length = (SEG B C).length := by - -- nondegenerate - have o_ne_a : O ≠ A := by sorry - have o_ne_b : O ≠ B := by sorry - have o_ne_c : O ≠ C := by sorry - have o_ne_d : O ≠ D := by sorry - have hnd3 : ¬ Collinear O A B := by sorry - -- $▵ OAB$ is isoceles because $OA = OB$. - have hisoc : (TRI_nd O A B hnd3).1.IsIsoceles := by + + -- We have that $C, O, A$ are not colinear. + have not_colinear_COA : ¬ colinear e.C e.O e.A := by sorry + -- We have that $D, O, B$ are not colinear. + have not_colinear_DOB : ¬ colinear e.D e.O e.B := by sorry + -- We have $O \ne A$. + haveI O_ne_A : PtNe e.O e.A := ⟨ne_source_of_lies_int_seg e.A e.D e.O e.O_int_AD⟩ + -- We have $O \ne B$. + haveI O_ne_B : PtNe e.O e.B := ⟨ne_source_of_lies_int_seg e.B e.C e.O e.O_int_BC⟩ + -- We have $C \ne B$. + haveI C_ne_B : PtNe e.C e.B := ⟨(ne_of_not_colinear e.not_colinear_ABC).1⟩ + -- We have $A \ne D$. + haveI A_ne_D : PtNe e.A e.D := ⟨((ne_of_not_colinear e.not_colinear_ABD).2.1)⟩ + -- We have $\angle AOC = - \angle BOD$. + have angle_AOC_eq_neg_angle_BOD : (∠ e.A e.O e.C) = - (∠ e.B e.O e.D) := by calc - _ = (SEG O B).length := length_of_rev_eq_length' - _ = _ := hseg.symm - -- Use AAS to prove $▵ CBA ≅ₐ ▵ DAB$. - have h : (TRI_nd C B A hnd1) ≅ₐ (TRI_nd D A B hnd2) := by - apply Triangle_nd.acongr_of_AAS - · -- $∠ BCA = -∠ ADB$ because $∠ ACB = ∠ ADB$. - calc - _ = -∠ A C B a_ne_c.symm b_ne_c.symm := by apply neg_value_of_rev_ang - _ = -∠ A D B a_ne_d.symm b_ne_d.symm := by rw [hang] - · -- $∠ ABC = ∠ ABO = -∠ OBA = -∠ BAO = -∠ BAD$. - calc - _ = ∠ A B O a_ne_b o_ne_b := by - unfold value_of_angle_of_three_point_nd - congr - apply eq_ang_of_liesint_liesint - · apply Seg_nd.target_lies_int_toray (seg_nd := (SEG_nd B A a_ne_b)) - · exact Seg_nd.lies_int_toray_of_lies_int (seg_nd := (SEG_nd B C b_ne_c.symm)) h2 - _ = -∠ O B A o_ne_b a_ne_b := by apply neg_value_of_rev_ang - _ = -∠ B A O a_ne_b.symm o_ne_a := by - have : ∠ O B A o_ne_b a_ne_b = ∠ B A O a_ne_b.symm o_ne_a := (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri.mp hisoc).symm - rw [this] - _ = _ := by - have : ANG B A O a_ne_b.symm o_ne_a = ANG B A D a_ne_b.symm a_ne_d.symm := by - apply eq_ang_of_liesint_liesint - · apply Seg_nd.target_lies_int_toray (seg_nd := (SEG_nd A B a_ne_b.symm)) - · apply (pt_lies_int_ray_of_pt_pt_iff_pt_lies_int_ray_of_pt_pt a_ne_d.symm o_ne_a).mpr - exact Seg_nd.lies_int_toray_of_lies_int (seg_nd := (SEG_nd A D a_ne_d.symm)) h1 - unfold value_of_angle_of_three_point_nd - rw [this] - rfl - · -- $BA = AB$ is trivial. - exact length_of_rev_eq_length' - -- $AD = BC$ follows from the congruence. + (∠ e.A e.O e.C) + -- $\angle AOC = - \angle COA$ by symmetry. + _= - (∠ e.C e.O e.A) := by + apply neg_value_of_rev_ang + -- $\angle COA = \angle BOD$ since they are opposite angles. + _= - (∠ e.B e.O e.D) := by + simp only [neg_inj] + apply ang_eq_ang_of_toDir_rev_toDir + · calc + (RAY e.O e.C).toDir + _= - (RAY e.C e.O).toDir := by apply Ray.toDir_eq_neg_toDir_of_mk_pt_pt + _= - (RAY e.C e.B).toDir := by + congr 1; + apply Ray.pt_pt_toDir_eq_ray_toDir (ray := (RAY e.C e.B)) (A := e.O) + apply SegND.lies_int_toRay_of_lies_int (X := e.O) (seg_nd := (SEG_nd e.C e.B)) + exact lies_int_seg_nd_of_lies_int_seg e.C e.B e.O (Seg.lies_int_rev_iff_lies_int.mpr e.O_int_BC) + _= (RAY e.B e.C).toDir := by symm; apply Ray.toDir_eq_neg_toDir_of_mk_pt_pt + _= (RAY e.B e.O).toDir := by + symm; + apply Ray.pt_pt_toDir_eq_ray_toDir (ray := (RAY e.B e.C)) (A := e.O) + apply SegND.lies_int_toRay_of_lies_int (X := e.O) (seg_nd := (SEG_nd e.B e.C)) + exact lies_int_seg_nd_of_lies_int_seg e.B e.C e.O e.O_int_BC + _= - (RAY e.O e.B).toDir := by apply Ray.toDir_eq_neg_toDir_of_mk_pt_pt + · calc + (RAY e.O e.A).toDir + _= - (RAY e.A e.O).toDir := by apply Ray.toDir_eq_neg_toDir_of_mk_pt_pt + _= - (RAY e.A e.D).toDir := by + congr 1; + apply Ray.pt_pt_toDir_eq_ray_toDir (ray := (RAY e.A e.D)) (A := e.O) + apply SegND.lies_int_toRay_of_lies_int (X := e.O) (seg_nd := (SEG_nd e.A e.D)) + exact lies_int_seg_nd_of_lies_int_seg e.A e.D e.O e.O_int_AD + _= (RAY e.D e.A).toDir := by symm; apply Ray.toDir_eq_neg_toDir_of_mk_pt_pt + _= (RAY e.D e.O).toDir := by + symm; + apply Ray.pt_pt_toDir_eq_ray_toDir (ray := (RAY e.D e.A)) (A := e.O) + apply SegND.lies_int_toRay_of_lies_int (X := e.O) (seg_nd := (SEG_nd e.D e.A)) + exact lies_int_seg_nd_of_lies_int_seg e.D e.A e.O (Seg.lies_int_rev_iff_lies_int.mpr e.O_int_AD) + _= - (RAY e.O e.D).toDir := by apply Ray.toDir_eq_neg_toDir_of_mk_pt_pt + have triangle_COA_acongr_triangle_DOB : (TRI_nd e.C e.O e.A not_colinear_COA) ≅ₐ (TRI_nd e.D e.O e.B not_colinear_DOB) := by + apply acongr_of_AAS' + · exact e.angle_OCA_eq_neg_angle_ODB + · exact angle_AOC_eq_neg_angle_BOD + · exact e.OA_eq_OB calc - _ = (SEG D A).length := length_of_rev_eq_length' - _ = (SEG C B).length := h.edge₃.symm - _ = _ := length_of_rev_eq_length' + (SEG e.A e.D).length + _= (SEG e.D e.A).length := by apply length_of_rev_eq_length' + _= (SEG e.D e.O).length + (SEG e.O e.A).length := by + apply length_eq_length_add_length + apply Seg.lies_on_rev_iff_lies_on.mp + apply Seg.lies_on_of_lies_int + exact e.O_int_AD + _= (SEG e.C e.O).length + (SEG e.O e.B).length := by + congr 1 + symm; exact triangle_COA_acongr_triangle_DOB.edge₃ + exact triangle_COA_acongr_triangle_DOB.edge₁ + _= (SEG e.C e.B).length := by + symm; + apply length_eq_length_add_length + apply Seg.lies_on_rev_iff_lies_on.mp + apply Seg.lies_on_of_lies_int + exact e.O_int_BC + _= (SEG e.B e.C).length := by apply length_of_rev_eq_length' +end Problem_7 -end Wuwowuji_Problem_1_7 +end EuclidGeom diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean index a06987c5..36cb2422 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean @@ -63,25 +63,25 @@ As a consequence, we know that $PQRS$ is a parallelogram. -/ -- We have $P \ne A$. - have P_ne_A : e.P ≠ e.A := by sorry + haveI P_ne_A : PtNe e.P e.A := by sorry -- We have $R \ne C$. - have R_ne_C : e.R ≠ e.C := by sorry + haveI R_ne_C : PtNe e.R e.C := by sorry -- We have $S \ne A$. - have S_ne_A : e.S ≠ e.A := by sorry + haveI S_ne_A : PtNe e.S e.A := by sorry -- We have $Q \ne C$. - have Q_ne_C : e.Q ≠ e.C := by sorry + haveI Q_ne_C : PtNe e.Q e.C := by sorry -- We have $B \ne A$. - have B_ne_A : e.B ≠ e.A := by sorry + haveI B_ne_A : PtNe e.B e.A := by sorry -- We have $C \ne D$. - have C_ne_D : e.C ≠ e.D := by sorry + haveI C_ne_D : PtNe e.C e.D := by sorry -- We have $D \ne A$. - have D_ne_A : e.D ≠ e.A := by sorry + haveI D_ne_A : PtNe e.D e.A := by sorry -- We have $C \ne B$. - have C_ne_B : e.C ≠ e.B := by sorry - -- We have that $A, P, C$ is not collinear. - have not_collinear_APC : ¬ Collinear e.A e.P e.C := by sorry - -- We have that $A, S, C$ is not collinear. - have not_collinear_ASC : ¬ Collinear e.A e.S e.C := by sorry + haveI C_ne_B : PtNe e.C e.B := by sorry + -- We have that $A, P, C$ is not colinear. + have not_colinear_APC : ¬ colinear e.A e.P e.C := by sorry + -- We have that $A, S, C$ is not colinear. + have not_colinear_ASC : ¬ colinear e.A e.S e.C := by sorry -- We have that $S$ lies on $AD$ by applying symmetry to the fact that $S$ lies on $DA$. have S_int_AD : e.S LiesInt (SEG e.A e.D) := Seg.lies_int_rev_iff_lies_int.mp e.S_int_DA -- We have that $Q$ lies on $CB$ by applying symmetry to the fact that $Q$ lies on $BC$. @@ -89,21 +89,21 @@ As a consequence, we know that $PQRS$ is a parallelogram. -- We have that $APCR$ is a parallelogram. have isprgnd_APCR : (QDR e.A e.P e.C e.R).IsParallelogram_nd := by -- We have that $AP, RC$ are of the same direction. - have dir_ap_eq_dir_rc_rev : (SEG_nd e.A e.P P_ne_A).toDir = (SEG_nd e.R e.C R_ne_C.symm).toDir := by + have dir_ap_eq_dir_rc_rev : (SEG_nd e.A e.P).toDir = (SEG_nd e.R e.C ).toDir := by calc - (SEG_nd e.A e.P P_ne_A).toDir + (SEG_nd e.A e.P).toDir -- Since $P$ lies on $AB$, we have $AP, AB$ are of the same direction, - _= (SEG_nd e.A e.B B_ne_A).toDir := by + _= (SEG_nd e.A e.B).toDir := by symm; - exact SegND.source_pt_toDir_eq_toDir_of_lies_int e.A e.B e.P B_ne_A e.P_int_AB + exact eq_todir_of_lies_int_seg_nd e.A e.B e.P e.P_int_AB -- in parallelogram $ABCD$, we have $AB, DC$ are of the same direction, - _= (SEG_nd e.D e.C C_ne_D).toDir := todir_eq_of_is_prg_nd e.A e.B e.C e.D e.hprgnd B_ne_A C_ne_D + _= (SEG_nd e.D e.C).toDir := todir_eq_of_is_prg_nd e.A e.B e.C e.D e.hprgnd -- $CD, DC$ are of the opposite direction because of symmetry, - _= - (SEG_nd e.C e.D C_ne_D.symm).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.D C_ne_D.symm)) + _= - (SEG_nd e.C e.D).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.D)) -- since $R$ lies on $CD$, we have $CR, CD$ are of the same direction, - _= - (SEG_nd e.C e.R R_ne_C).toDir := by simp only [SegND.source_pt_toDir_eq_toDir_of_lies_int e.C e.D e.R C_ne_D.symm e.R_int_CD] + _= - (SEG_nd e.C e.R).toDir := by simp only [eq_toDir_of_lies_int_seg_nd e.C e.D e.R e.R_int_CD] -- $CR, RC$ are of the opposite direction because of symmetry. - _= (SEG_nd e.R e.C R_ne_C.symm).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.R R_ne_C)) + _= (SEG_nd e.R e.C).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.R)) -- We have $AP = RC$. have AP_eq_RC : (SEG e.A e.P).length = (SEG e.R e.C).length := by calc @@ -113,27 +113,27 @@ As a consequence, we know that $PQRS$ is a parallelogram. -- $CR = RC$ by symmetry. _= (SEG e.R e.C).length := by exact length_of_rev_eq_length' (A := e.R) (B := e.C) -- We have that $APCR$ is a parallelogram, because $AP, RC$ are of the same direction and $AP = RC$. - have isprg_APCR : (QDR e.A e.P e.C e.R).IsParallelogram := by exact vec_eq_of_eq_dir_and_eq_length P_ne_A R_ne_C.symm dir_ap_eq_dir_rc_rev AP_eq_RC - -- Since $A, P, C$ is not collinear, we know that the parallelogram $APCR$ is non-degenerate. - exact is_prg_nd_of_is_prg_not_collinear₁₂₃ (QDR e.A e.P e.C e.R) isprg_APCR not_collinear_APC + have isprg_APCR : (QDR e.A e.P e.C e.R).IsParallelogram := by exact vec_eq_of_eq_dir_and_eq_length dir_ap_eq_dir_rc_rev AP_eq_RC + -- Since $A, P, C$ is not colinear, we know that the parallelogram $APCR$ is non-degenerate. + exact is_prg_nd_of_is_prg_not_colinear₁₂₃ (QDR e.A e.P e.C e.R) isprg_APCR not_colinear_APC -- We have that $ASCQ$ is a parallelogram. have isprgnd_ASCQ : (QDR e.A e.S e.C e.Q) IsPRG_nd := by -- We have that $AS, QC$ are of the same direction. - have dir_as_eq_dir_qc_rev : (SEG_nd e.A e.S S_ne_A).toDir = (SEG_nd e.Q e.C Q_ne_C.symm).toDir := by + have dir_as_eq_dir_qc_rev : (SEG_nd e.A e.S).toDir = (SEG_nd e.Q e.C).toDir := by calc - (SEG_nd e.A e.S S_ne_A).toDir + (SEG_nd e.A e.S).toDir -- Since $S$ lies on $AD$, we have $AS, AD$ are of the same direction, - _= (SEG_nd e.A e.D D_ne_A).toDir := by + _= (SEG_nd e.A e.D).toDir := by symm; - exact SegND.source_pt_toDir_eq_toDir_of_lies_int e.A e.D e.S D_ne_A S_int_AD + exact eq_todir_of_lies_int_seg_nd e.A e.D e.S S_int_AD -- in parallelogram $ABCD$, we have $AD, BC$ are of the same direction, - _= (SEG_nd e.B e.C C_ne_B).toDir := todir_eq_of_is_prg_nd_variant e.A e.B e.C e.D e.hprgnd D_ne_A C_ne_B + _= (SEG_nd e.B e.C).toDir := todir_eq_of_is_prg_nd_variant e.A e.B e.C e.D e.hprgnd -- $BC, CB$ are of the opposite direction because of symmetry, - _= - (SEG_nd e.C e.B C_ne_B.symm).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.B C_ne_B.symm)) + _= - (SEG_nd e.C e.B).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.B)) -- since $Q$ lies on $CB$, we have $CQ, CB$ are of the same direction, - _= - (SEG_nd e.C e.Q Q_ne_C).toDir := by simp only [SegND.source_pt_toDir_eq_toDir_of_lies_int e.C e.B e.Q C_ne_B.symm Q_int_CB] + _= - (SEG_nd e.C e.Q).toDir := by simp only [eq_todir_of_lies_int_seg_nd e.C e.B e.Q Q_int_CB] -- $CQ, QC$ are of the opposite direction because of symmetry. - _= (SEG_nd e.Q e.C Q_ne_C.symm).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.Q Q_ne_C)) + _= (SEG_nd e.Q e.C).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.Q)) -- We have $AS = QC$. have AS_eq_QC : (SEG e.A e.S).length = (SEG e.Q e.C).length := by calc diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean index 22402e40..1617d404 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean @@ -4,6 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Position.Angle_trash import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence_trash import EuclideanGeometry.Foundation.Axiom.Linear.Line_trash import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex_trash +import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle_trash noncomputable section @@ -60,7 +61,7 @@ Since $DX$ is perpendicular to $AB$ at $X$, we have $\angle BXD = \pi/2 (\mod \p Since $EY$ is perpendicular to $AC$ at $Y$, we have $\angle CYE = \pi/2 (\mod \pi)$. Thus, $\angle BXD = \angle CYE (\mod \pi)$. In $\triangle XBD$ and $\triangle YCE$, -$\cdot $\angle BXD = \angle CYE (\mod \pi)$ +$\cdot \angle BXD = \angle CYE (\mod \pi)$ $\cdot \angle DBX = - \angle ECY$ $\cdot BD = CE$ Thus, $\triangle XBD \cong_a \triangle YEC$ (by AAS) diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean index f26c6fdd..e187994b 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean @@ -1,6 +1,5 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Circle import Mathlib.Data.Int.Parity - /-! # APIs about Angle from Mathlib @@ -11,10 +10,10 @@ noncomputable section attribute [ext] Complex.ext + open Real section Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle - namespace EuclidGeom def AngValue : Type := Angle diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean index 2fdd9a73..e3320732 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean @@ -1308,4 +1308,46 @@ end DirLine end addtorsor +section Collinear + +lemma snd_pt_lies_on_mk_pt_proj_of_vec (A B : P) [hh : PtNe A B] : B LiesOn (Line.mk_pt_proj A ((VEC_nd A B).toProj)) := by + have : (Line.mk_pt_proj A ((VEC_nd A B).toProj)) = (SEG_nd A B).toLine := by + have : (Line.mk_pt_proj A ((VEC_nd A B).toProj)).toProj = (SEG_nd A B).toLine.toProj := by + calc + _= ((VEC_nd A B).toProj) := by apply Line.proj_eq_of_mk_pt_proj + _= _ := by rfl + apply Line.eq_of_same_toProj_and_pt_lies_on (A := A) _ _ this + apply Line.pt_lies_on_of_mk_pt_proj + apply SegND.source_lies_on_toLine + simp only [this] + apply SegND.target_lies_on_toLine + +theorem exist_line_of_collinear {A B C : P} (h : Collinear A B C) : ∃ (l : Line P), A LiesOn l ∧ B LiesOn l ∧ C LiesOn l := by + unfold Collinear at h + rcases eq_or_ne C B with (c_eq_b | c_ne_b) + · simp only [c_eq_b]; simp only [and_self] + rcases eq_or_ne B A with (b_eq_a | b_ne_a) + · simp only [b_eq_a, and_self]; apply Line.exist_line_pt_lies_on + · haveI : PtNe B A := ⟨b_ne_a⟩ + refine' ⟨(Line.mk_pt_proj A ((VEC_nd A B).toProj)), Line.pt_lies_on_of_mk_pt_proj A ((VEC_nd A B).toProj), snd_pt_lies_on_mk_pt_proj_of_vec A B⟩ + · rcases eq_or_ne A C with (a_eq_c | a_ne_c) + · simp only [a_eq_c.symm] + rcases eq_or_ne B A with (b_eq_a | b_ne_a) + · simp only [b_eq_a, and_self]; apply Line.exist_line_pt_lies_on + · haveI : PtNe B A := ⟨b_ne_a⟩ + refine' ⟨(Line.mk_pt_proj A ((VEC_nd A B).toProj)), Line.pt_lies_on_of_mk_pt_proj A ((VEC_nd A B).toProj), snd_pt_lies_on_mk_pt_proj_of_vec A B, Line.pt_lies_on_of_mk_pt_proj A ((VEC_nd A B).toProj)⟩ + · rcases eq_or_ne B A with (b_eq_a | b_ne_a) + · simp only [b_eq_a, and_self_left] + haveI : PtNe A C := ⟨a_ne_c⟩ + refine' ⟨(Line.mk_pt_proj A ((VEC_nd A C).toProj)), Line.pt_lies_on_of_mk_pt_proj A ((VEC_nd A C).toProj), snd_pt_lies_on_mk_pt_proj_of_vec A C⟩ + · simp only [c_ne_b, a_ne_c, b_ne_a, or_self, dite_false] at h + unfold collinear_of_nd at h + haveI : PtNe B A := ⟨b_ne_a⟩ + haveI : PtNe A C := ⟨a_ne_c⟩ + haveI : PtNe C B := ⟨c_ne_b⟩ + have h3 : C LiesOn (Line.mk_pt_proj A ((VEC_nd A B).toProj)) := by + simp only [h]; exact snd_pt_lies_on_mk_pt_proj_of_vec A C + refine' ⟨(Line.mk_pt_proj A ((VEC_nd A B).toProj)), (Line.pt_lies_on_of_mk_pt_proj A ((VEC_nd A B).toProj)), snd_pt_lies_on_mk_pt_proj_of_vec A B, h3⟩ + +end Collinear end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Order.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Order.lean new file mode 100644 index 00000000..471d31b3 --- /dev/null +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Order.lean @@ -0,0 +1,868 @@ +import EuclideanGeometry.Foundation.Axiom.Linear.Class +import EuclideanGeometry.Foundation.Axiom.Linear.Collinear + +noncomputable section + +namespace EuclidGeom + +variable {P : Type _} [EuclideanPlane P] +-- `unused section` +/- +-- Definition +def DirObj.le {α : Type*} [DirObj α] (l : α) (A B : P) : Prop := (0 : ℝ) ≤ inner (VEC A B) (toDir l).unitVecND + +def DirObj.lt {α : Type*} [DirObj α] (l : α) (A B : P) : Prop := (0 : ℝ) < inner (VEC A B) (toDir l).unitVecND + +notation A : max "≤[" l : max "]" B : max => DirObj.le l A B +notation A : max "<[" l : max "]" B : max => DirObj.lt l A B +-- Proof of Preorder +def DirObj.instPreorder {α : Type*} [DirObj α] (l : α) : Preorder P where + le := DirObj.le l + lt := DirObj.lt l + le_refl := by + rintro a; simp only; unfold le + simp only [vec_same_eq_zero, ne_eq, Dir.coe_unitVecND, inner_zero_left, le_refl] + le_trans := by + rintro a b c; simp only; unfold le; rintro h1 h2 + calc + _≤ inner (VEC a b) ↑(toDir l).unitVecND + inner (VEC b c) ↑(toDir l).unitVecND := by positivity + _= inner (VEC a c) ↑(toDir l).unitVecND := by + symm; + have : (VEC a c) = (VEC a b) + (VEC b c) := by simp only [vec_add_vec] + simp only [this] + apply InnerProductSpace.add_left + lt_iff_le_not_le := by + rintro a b; simp only; unfold le; unfold lt + constructor + · rintro h1 + constructor + · positivity + · simp only [ne_eq, Dir.coe_unitVecND, not_le] + have : (VEC b a) = (-1 : ℝ) • (VEC a b) := by simp only [neg_smul, one_smul, neg_vec] + simp only [this] + have : inner ((-1 : ℝ) • VEC a b) (toDir l).unitVec = (-1 : ℝ) * (inner (VEC a b) (toDir l).unitVec) := by + exact InnerProductSpace.smul_left (VEC a b) ((toDir l).unitVec) (-1 : ℝ) + simp only [this] + simp only [neg_mul, one_mul, Left.neg_neg_iff, gt_iff_lt] + positivity + · rintro ⟨_, h2⟩ + simp only [ne_eq, Dir.coe_unitVecND, not_le] at h2 + have : (VEC b a) = (-1 : ℝ) • (VEC a b) := by simp only [neg_smul, one_smul, neg_vec] + simp only [this] at h2 + have : inner ((-1 : ℝ) • VEC a b) (toDir l).unitVec = (-1 : ℝ) * (inner (VEC a b) (toDir l).unitVec) := by + exact InnerProductSpace.smul_left (VEC a b) ((toDir l).unitVec) (-1 : ℝ) + simp only [this] at h2 + simp only [neg_mul, one_mul, Left.neg_neg_iff, gt_iff_lt] at h2 + exact h2 + +@[aesop unsafe] +theorem lt_of_le_not_le {α : Type*} [DirObj α] (l : α) {a : P} {b : P} : +a ≤[l] b → ¬b ≤[l] a → a <[l] b := + @_root_.lt_of_le_not_le P (DirObj.instPreorder l) a b +-/ + +namespace DirLine +section linear_order + +-- # preparatory theorems +abbrev lelem (A : P) {l : DirLine P} (ha : A LiesOn l) : l.carrier.Elem := ⟨A, ha⟩ +-- Collinearity -- `moved to Linear.Line` + +-- linear order and ne +theorem ne_iff_ne_as_line_elem {Dl : DirLine P} {A B : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) : (A ≠ B) ↔ (lelem A ha ≠ lelem B hb) := by + simp only [ne_eq, Subtype.mk.injEq] + +-- linear order and vector +theorem exist_pos_smul_of_lt {Dl : DirLine P} {A B : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl)(a_lt_b : (lelem A ha) < (lelem B hb)) : (∃ t : ℝ, 0 < t ∧ (VEC A B) = t • (Dl.toDir).unitVec) := by + have h1 : (0 : ℝ) < ddist ha hb := (DirLine.lt_iff_zero_lt_ddist ha hb).mp a_lt_b + have h3 : ∃ t : ℝ, VEC A B = t • (Dl.toDir).unitVec := by + apply Line.exist_real_vec_eq_smul_of_lies_on + have : Line.mk_pt_dir A Dl.toDir = Dl.toLine := by + calc + _= (DirLine.mk_pt_dir A Dl.toDir).toLine := by rfl + _=_ := by + congr 1 + apply DirLine.mk_pt_dir_eq_of_eq_toDir + exact ha; rfl + simp only [this] + apply DirLine.lies_on_iff_lies_on_toLine.mpr + exact hb + rcases h3 with ⟨x1, hx1⟩ + have h1 : (0 : ℝ) < inner (VEC A B) (Dl.toDir).unitVec := by exact h1 + have h1 : (0 : ℝ) < x1 := by + calc + (0 : ℝ) + _< inner (x1 • Dl.toDir.unitVec) Dl.toDir.unitVec := by simp only [hx1.symm]; exact h1 + _= x1 * inner Dl.toDir.unitVec Dl.toDir.unitVec := by + apply InnerProductSpace.smul_left + _= x1 := by simp only [Dir.inner_unitVec, vsub_self, AngValue.cos_zero, mul_one] + use x1 + +theorem exist_nonneg_smul_of_le {Dl : DirLine P} {A B : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl)(a_le_b : (lelem A ha) ≤ (lelem B hb)) : (∃ t : ℝ, 0 ≤ t ∧ (VEC A B) = t • (Dl.toDir).unitVec) := by + have h1 : (0 : ℝ) ≤ ddist ha hb := (DirLine.le_iff_zero_le_ddist ha hb).mp a_le_b + have h3 : ∃ t : ℝ, VEC A B = t • (Dl.toDir).unitVec := by + apply Line.exist_real_vec_eq_smul_of_lies_on + have : Line.mk_pt_dir A Dl.toDir = Dl.toLine := by + calc + _= (DirLine.mk_pt_dir A Dl.toDir).toLine := by rfl + _=_ := by + congr 1 + apply DirLine.mk_pt_dir_eq_of_eq_toDir + exact ha; rfl + simp only [this] + apply DirLine.lies_on_iff_lies_on_toLine.mpr + exact hb + rcases h3 with ⟨x1, hx1⟩ + have h1 : (0 : ℝ) ≤ inner (VEC A B) (Dl.toDir).unitVec := by exact h1 + have h1 : (0 : ℝ) ≤ x1 := by + calc + (0 : ℝ) + _≤ inner (x1 • Dl.toDir.unitVec) Dl.toDir.unitVec := by simp only [hx1.symm]; exact h1 + _= x1 * inner Dl.toDir.unitVec Dl.toDir.unitVec := by + apply InnerProductSpace.smul_left + _= x1 := by simp only [Dir.inner_unitVec, vsub_self, AngValue.cos_zero, mul_one] + use x1 + +theorem lt_of_exist_pos_smul {Dl : DirLine P} {A B : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (h : ∃ (x : ℝ), ((0 : ℝ) < x) ∧ (VEC A B) = x • (Dl.toDir).unitVec): lelem A ha < lelem B hb := by + rcases h with ⟨x, ⟨xpos, h⟩⟩ + by_contra h1 + have : ¬ 0 < ddist ha hb := by + by_contra h3; absurd h1 + apply (DirLine.lt_iff_zero_lt_ddist ha hb).mpr h3 + simp only [not_lt] at this + have : lelem B hb ≤ lelem A ha := by + apply (DirLine.le_iff_zero_le_ddist hb ha).mpr + calc + _≤ - ddist ha hb := by linarith + _= ddist hb ha := by + unfold ddist; simp only [neg_vsub_eq_vsub_rev] + rcases exist_nonneg_smul_of_le hb ha this with ⟨t, ⟨tnneg, ht⟩⟩ + have : (VEC A B) = - (VEC B A) := by simp only [neg_vec] + simp only [this, ht] at h + have : -(t • Dl.toDir.unitVec) = (-t) • Dl.toDir.unitVec := by simp only [neg_smul] + simp only [this] at h + have h2 : (x + t) • Dl.toDir.unitVec = (0 : Vec) := by + calc + _= x • Dl.toDir.unitVec + t • Dl.toDir.unitVec := by apply add_smul + _= (-t) • Dl.toDir.unitVec + t • Dl.toDir.unitVec := by simp only [h.symm] + _= (-t + t) • Dl.toDir.unitVec := by simp only [neg_smul, add_left_neg, zero_smul] + _= 0 • Dl.toDir.unitVec := by simp only [add_left_neg, zero_smul] + _= (0 : Vec) := by simp only [zero_smul] + have : Dl.toDir.unitVec ≠ (0 : Vec) := by + simp only [ne_eq, VecND.ne_zero, not_false_eq_true] + have h1 : x + t = 0 := by + by_contra h1; push_neg at h1 + absurd this + calc + _= ((x + t)⁻¹ * (x + t)) • Dl.toDir.unitVec := by + field_simp + _= (x + t)⁻¹ • ((x + t) • Dl.toDir.unitVec) := by apply mul_smul + _= (x + t)⁻¹ • (0 : Vec) := by simp only [h2] + _= (0 : Vec) := by simp only [smul_zero] + linarith + +theorem le_of_exist_nonneg_smul {Dl : DirLine P} {A B : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (h : ∃ (x : ℝ), ((0 : ℝ) ≤ x) ∧ (VEC A B) = x • (Dl.toDir).unitVec): lelem A ha ≤ lelem B hb := by + rcases h with ⟨x, ⟨xnneg, h⟩⟩ + rcases lt_or_eq_of_le xnneg with (xpos | h0) + apply le_of_lt + apply lt_of_exist_pos_smul ha hb + use x + simp only [h0.symm, zero_smul] at h + have : A = B := by + apply (eq_iff_vec_eq_zero B A).mpr + have : (VEC B A) = - (VEC A B) := by simp only [neg_vec] + simp only [this, h, neg_zero] + simp only [this, le_refl] + +-- LiesInt SegND.extension and LiesOn Seg +theorem lies_int_seg_nd_ext_iff_lies_int (A B C : P) [a_ne_c : PtNe A C] : B LiesInt (SEG_nd A C).extension ↔ C LiesInt (SEG A B) := by + constructor + · rintro h1 + rcases Ray.lies_int_iff.mp h1 with ⟨x1, ⟨x1pos, hx1⟩⟩ + rcases Ray.lies_int_iff.mp (Ray.snd_pt_lies_int_mk_pt_pt A C) with ⟨x2, ⟨x2pos, hx2⟩⟩ + apply Seg.lies_int_iff.mpr + constructor + · show B ≠ A + by_contra h3; simp only [h3] at h1; absurd h1; + apply SegND.not_lies_int_extn_of_lies_on + show A LiesOn (SEG A C) + apply Seg.source_lies_on + · use x2 / (x1 + x2) + · constructor + · positivity + · constructor + · have : 0 < 1 - (x2 / (x1 + x2)) := by + calc + _< x1 / (x1 + x2) := by positivity + _= 1 - (x2 / (x1 + x2)) := by field_simp + linarith + · symm; + calc + _= (x2 / (x1 + x2)) • (VEC A B) := by rfl + _= (x2 / (x1 + x2)) • (VEC A C + VEC C B) := by congr 1; simp only [vec_add_vec] + _= (x2 / (x1 + x2)) • (VEC A C) + (x2 / (x1 + x2)) • (VEC C B) := by apply smul_add + _= (x2 / (x1 + x2)) • (VEC A C) + (x2 / (x1 + x2)) • x1 • (SegND.extension (SEG_nd A C)).toDir.unitVec := by congr 2; + _= (x2 / (x1 + x2)) • (VEC A C) + (x2 / (x1 + x2)) • x1 • (RAY A C).toDir.unitVec := by rfl + _= (x2 / (x1 + x2)) • (VEC A C) + ((x2 / (x1 + x2)) * x1) • (RAY A C).toDir.unitVec := by congr 1; symm; apply mul_smul + _= (x2 / (x1 + x2)) • (VEC A C) + ((x1 / (x1 + x2)) * x2) • (RAY A C).toDir.unitVec := by congr 2; field_simp; ring + _= (x2 / (x1 + x2)) • (VEC A C) + (x1 / (x1 + x2)) • x2 • (RAY A C).toDir.unitVec := by congr 1; apply mul_smul + _= (x2 / (x1 + x2)) • (VEC A C) + (x1 / (x1 + x2)) • (VEC A C) := by + congr 2; symm; + show VEC (RAY A C).source C = x2 • (RAY A C).toDir.unitVec + exact hx2 + _= (x2 / (x1 + x2) + x1 / (x1 + x2)) • (VEC A C) := by symm; apply add_smul + _= (1 : ℝ) • (VEC A C) := by congr 1; field_simp; ring; + _= _ := by simp only [one_smul] + · rintro h1 + rcases Seg.lies_int_iff.mp h1 with ⟨_, ⟨x1, ⟨x1pos, ⟨x1lt1, hx1⟩⟩⟩⟩ + rcases Ray.lies_int_iff.mp (Ray.snd_pt_lies_int_mk_pt_pt A C) with ⟨x2, ⟨x2pos, hx2⟩⟩ + apply Ray.lies_int_iff.mpr + have : 0 < 1 - x1 := by simp only [sub_pos, x1lt1] + use ((1 - x1) / x1) * x2 + constructor + · positivity + · show (VEC C B) = (((1 - x1) / x1) * x2) • (RAY A C).toDir.unitVec + symm; + calc + _= ((1 - x1) / x1) • x2 • (RAY A C).toDir.unitVec := by apply mul_smul + _= ((1 - x1) / x1) • (VEC A C) := by simp only [hx2.symm]; congr 1; + _= ((1 - x1) / x1) • x1 • (VEC A B) := by congr 1; + _= (((1 - x1) / x1) * x1) • (VEC A B) := by symm; apply mul_smul + _= (1 - x1) • (VEC A B) := by congr 1; field_simp + _= (1 + (-x1)) • (VEC A B) := by congr 1; + _= (1 : ℝ) • (VEC A B) + (-x1) • (VEC A B) := by apply add_smul + _= (VEC A B) + (- x1 • VEC A B) := by congr 1; apply one_smul; + _= (VEC A B) + (- (x1 • (VEC A B))) := by + congr 1; apply neg_smul + _= (VEC A B) - (x1 • (VEC A B)) := by symm; apply sub_eq_add_neg + _= (VEC A B) - (VEC A C) := by + congr 1; symm; + show VEC (SEG A B).source C = x1 • (SEG A B).toVec + exact hx1 + _= (VEC C B) := by simp only [vec_sub_vec] + +-- LiesOn SegND.extension and LiesInt Seg +theorem lies_on_seg_nd_ext_iff_lies_on (A B C : P) [a_ne_c : PtNe A C] : B LiesOn (SEG_nd A C).extension ↔ C LiesOn (SEG A B) := by + rcases eq_or_ne B C with (b_eq_c | b_ne_c) + · simp only [b_eq_c] + have h : C LiesOn (SEG_nd A C) ∧ C LiesOn SegND.extension (SEG_nd A C) := by + apply (SegND.eq_target_iff_lies_on_lies_on_extn (A := C) (seg_nd := (SEG_nd A C))).mpr + rfl + simp only [h, true_iff] + show C LiesOn (SEG_nd A C) + exact h.1 + · constructor + · rintro h1 + have : B LiesInt SegND.extension (SEG_nd A C) := by refine' ⟨h1, b_ne_c⟩ + apply Seg.lies_on_of_lies_int + exact (lies_int_seg_nd_ext_iff_lies_int A B C).mp this + · rintro h1 + have : C LiesInt (SEG A B) := by refine' ⟨h1, a_ne_c.out.symm, b_ne_c.symm⟩ + apply Ray.lies_on_of_lies_int + exact (lies_int_seg_nd_ext_iff_lies_int A B C).mpr this + +-- # Order Relations to Position Relations +-- linear order and LiesInt Seg +theorem lies_int_seg_of_lt_and_lt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_lt_b : lelem A ha < lelem B hb) (b_lt_c : lelem B hb < lelem C hc) : B LiesInt (SEG A C) := by + rcases exist_pos_smul_of_lt ha hb a_lt_b with ⟨x1, ⟨x1pos, hx1⟩⟩ + rcases exist_pos_smul_of_lt hb hc b_lt_c with ⟨x2, ⟨x2pos, hx2⟩⟩ + apply Seg.lies_int_iff.mpr + constructor + · have : lelem A ha ≠ lelem C hc := by + apply ne_of_lt; exact lt_trans a_lt_b b_lt_c + apply (ne_iff_ne_as_line_elem hc ha).mpr + exact this.symm + · use (x1 / (x1 + x2)) + constructor + · positivity + · constructor + · have : 0 < 1 - x1 / (x1 + x2) := by + calc + _< x2 / (x1 + x2) := by positivity + _= _ := by field_simp + linarith [this] + · simp only [hx1] + have : (SEG A C).toVec = (VEC A B) + (VEC B C) := by simp only [seg_toVec_eq_vec, + vec_add_vec] + simp only [this, hx1, hx2, smul_add] + calc + _= ((x1 / (x1 + x2)) * x1 + (x1 / (x1 + x2)) * x2) • Dl.toDir.unitVec := by + congr 1; field_simp; ring + _= ((x1 / (x1 + x2)) * x1) • Dl.toDir.unitVec + ((x1 / (x1 + x2)) * x2) • Dl.toDir.unitVec := by apply add_smul + _=_ := by congr 1; apply mul_smul; apply mul_smul + +theorem lies_int_seg_of_gt_and_gt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_gt_b : (lelem A ha) > (lelem B hb)) (b_gt_c : (lelem B hb) > (lelem C hc)) : B LiesInt (SEG A C) := by + apply Seg.lies_int_rev_iff_lies_int.mp + apply lies_int_seg_of_lt_and_lt hc hb ha + exact b_gt_c + exact a_gt_b + +-- linear order and LiesOn Seg +theorem lies_on_seg_of_le_and_le {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_le_b : lelem A ha ≤ lelem B hb) (b_le_c : lelem B hb ≤ lelem C hc) : B LiesOn (SEG A C) := by + have h1 : (lelem A ha = lelem B hb) ∨ (lelem A ha < lelem B hb) := le_iff_eq_or_lt.mp a_le_b + have h2 : (lelem B hb = lelem C hc) ∨ (lelem B hb < lelem C hc) := le_iff_eq_or_lt.mp b_le_c + rcases h1 with (a_eq_b | a_lt_b) + · have : A = B := Subtype.val_inj.mpr a_eq_b + simp only [this.symm] + apply Seg.source_lies_on + · rcases h2 with (b_eq_c | b_lt_c) + have : B = C := Subtype.val_inj.mpr b_eq_c + simp only [this] + apply Seg.target_lies_on + · have : B LiesInt (SEG A C) := lies_int_seg_of_lt_and_lt ha hb hc a_lt_b b_lt_c + exact Seg.lies_on_of_lies_int this + +theorem lies_on_seg_of_ge_and_ge {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_ge_b : (lelem A ha) ≥ (lelem B hb)) (b_ge_c : (lelem B hb) ≥ (lelem C hc)) : B LiesOn (SEG A C) := by + apply Seg.lies_on_rev_iff_lies_on.mp + apply lies_on_seg_of_le_and_le hc hb ha + exact b_ge_c + exact a_ge_b + +-- linear order and toDir +theorem eq_toDir_of_lt {Dl : DirLine P} {A B : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (a_lt_b : lelem A ha < lelem B hb) : (RAY A B ((ne_iff_ne_as_line_elem ha hb).mpr (ne_of_lt a_lt_b)).symm).toDir = Dl.toDir := by + haveI B_ne_A : PtNe B A := ⟨((ne_iff_ne_as_line_elem ha hb).mpr (ne_of_lt a_lt_b)).symm⟩ + rcases exist_pos_smul_of_lt ha hb a_lt_b with ⟨x1, ⟨x1pos, hx1⟩⟩ + calc + _= (VEC_nd A B).toDir := by rfl + _= (Dl.toDir.unitVecND).toDir := by + apply VecND.toDir_eq_toDir_iff.mpr + unfold VecND.SameDir + use x1; simp only [ne_eq, VecND.coe_mkPtPt, Dir.coe_unitVecND, hx1, and_true, x1pos] + _=_ := by simp only [Dir.unitVecND_toDir] + +theorem neg_toDir_of_gt {Dl : DirLine P} {A B : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (a_gt_b : lelem A ha > lelem B hb) : (RAY A B ((ne_iff_ne_as_line_elem ha hb).mpr (ne_of_gt a_gt_b)).symm).toDir = - Dl.toDir := by + haveI B_ne_A : PtNe B A := ⟨((ne_iff_ne_as_line_elem ha hb).mpr (ne_of_gt a_gt_b)).symm⟩ + rcases exist_pos_smul_of_lt hb ha a_gt_b with ⟨x1, ⟨x1pos, hx1⟩⟩ + calc + _= (VEC_nd A B).toDir := by rfl + _= - (VEC_nd B A).toDir := by + have : (VEC_nd A B) = - (VEC_nd B A) := by ext; simp only [ne_eq, VecND.coe_mkPtPt, RayVector.coe_neg, neg_vec] + simp only [this] + apply VecND.neg_toDir (VEC_nd B A) + _= - (Dl.toDir.unitVecND).toDir := by + simp only [neg_inj] + apply VecND.toDir_eq_toDir_iff.mpr + unfold VecND.SameDir + use x1; simp only [ne_eq, VecND.coe_mkPtPt, Dir.coe_unitVecND, hx1, and_true, x1pos] + _=_ := by simp only [Dir.unitVecND_toDir] + +-- linear order and LiesInt ray +theorem lies_int_ray_of_lt_and_lt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_lt_b : lelem A ha < lelem B hb) (a_lt_c : lelem A ha < lelem C hc) : B LiesInt (RAY A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm):= by + haveI : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm⟩ + rcases exist_pos_smul_of_lt ha hb a_lt_b with ⟨x1, ⟨x1pos, hx1⟩⟩ + apply Ray.lies_int_iff.mpr + use x1 + constructor + · exact x1pos + · have : (RAY A C).toDir = Dl.toDir := eq_toDir_of_lt ha hc a_lt_c + simp only [this] + exact hx1 + +theorem lies_int_ray_of_gt_and_gt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_gt_b : lelem A ha > lelem B hb) (a_gt_c : lelem A ha > lelem C hc) : B LiesInt (RAY A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm):= by + haveI : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm⟩ + rcases exist_pos_smul_of_lt hb ha a_gt_b with ⟨x1, ⟨x1pos, hx1⟩⟩ + apply Ray.lies_int_iff.mpr + use x1 + constructor + · exact x1pos + · have : (RAY A C).toDir = - Dl.toDir := neg_toDir_of_gt ha hc a_gt_c + simp only [this] + have : (VEC A B) = - (VEC B A) := by simp only [ne_eq, VecND.coe_mkPtPt, RayVector.coe_neg, neg_vec] + simp only [Dir.neg_unitVec, smul_neg] + show (VEC A B) = - (x1 • Dl.toDir.unitVec) + simp only [this, hx1] + +-- linear order and LiesOn ray +theorem lies_on_ray_of_le_and_lt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_le_b : lelem A ha ≤ lelem B hb) (a_lt_c : lelem A ha < lelem C hc) : B LiesOn (RAY A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm):= by + haveI : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm⟩ + rcases exist_nonneg_smul_of_le ha hb a_le_b with ⟨x1, ⟨x1nneg, hx1⟩⟩ + apply Ray.lies_on_iff.mpr + use x1 + constructor + · exact x1nneg + · have : (RAY A C).toDir = Dl.toDir := eq_toDir_of_lt ha hc a_lt_c + simp only [this] + exact hx1 + +theorem lies_on_ray_of_ge_and_gt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_ge_b : lelem A ha ≥ lelem B hb) (a_gt_c : lelem A ha > lelem C hc) : B LiesOn (RAY A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm):= by + haveI : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm⟩ + rcases exist_nonneg_smul_of_le hb ha a_ge_b with ⟨x1, ⟨x1nneg, hx1⟩⟩ + apply Ray.lies_on_iff.mpr + use x1 + constructor + · exact x1nneg + · have : (RAY A C).toDir = - Dl.toDir := neg_toDir_of_gt ha hc a_gt_c + simp only [this] + have : (VEC A B) = - (VEC B A) := by simp only [ne_eq, VecND.coe_mkPtPt, RayVector.coe_neg, neg_vec] + simp only [Dir.neg_unitVec, smul_neg] + show (VEC A B) = - (x1 • Dl.toDir.unitVec) + simp only [this, hx1] + +-- linear order and LiesInt SegND.extension +theorem lies_int_seg_nd_ext_of_lt_and_lt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_lt_c : lelem A ha < lelem C hc) (c_lt_b : lelem C hc < lelem B hb) : B LiesInt (SEG_nd A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm).extension := by + haveI C_ne_A : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm⟩ + rcases exist_pos_smul_of_lt hc hb c_lt_b with ⟨x2, ⟨x2pos, hx2⟩⟩ + apply Ray.lies_int_iff.mpr + use x2 + constructor + · exact x2pos + · simp only [SegND.extn_toDir, Dir.quotient_mk_eq, SegND.mkPtPt_toDir] + have : (VEC_nd A C).toDir = Dl.toDir := + calc + _= (RAY A C).toDir := by rfl + _= _ := eq_toDir_of_lt ha hc a_lt_c + simp only [this] + exact hx2 + +theorem lies_int_seg_nd_ext_of_gt_and_gt {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_gt_c : lelem A ha > lelem C hc) (c_gt_b : lelem C hc > lelem B hb) : B LiesInt (SEG_nd A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm).extension := by + haveI C_ne_A : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm⟩ + rcases exist_pos_smul_of_lt hb hc c_gt_b with ⟨x2, ⟨x2pos, hx2⟩⟩ + apply Ray.lies_int_iff.mpr + use x2 + constructor + · exact x2pos + · simp only [SegND.extn_toDir, Dir.quotient_mk_eq, SegND.mkPtPt_toDir] + have : (VEC_nd A C).toDir = - Dl.toDir := + calc + _= (RAY A C).toDir := by rfl + _= _ := neg_toDir_of_gt ha hc a_gt_c + simp only [this, Dir.neg_unitVec, smul_neg] + show (VEC C B) = - (x2 • Dl.toDir.unitVec) + have : (VEC C B) = - (VEC B C) := by simp only [neg_vec] + simp only [this, neg_inj, hx2] + +-- linear order and LiesOn SegND.extension +theorem lies_on_seg_nd_ext_of_lt_and_le {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_lt_c : lelem A ha < lelem C hc) (c_le_b : lelem C hc ≤ lelem B hb) : B LiesOn (SEG_nd A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm).extension := by + haveI C_ne_A : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_lt a_lt_c)).symm⟩ + rcases exist_nonneg_smul_of_le hc hb c_le_b with ⟨x2, ⟨x2nneg, hx2⟩⟩ + apply Ray.lies_on_iff.mpr + use x2 + constructor + · exact x2nneg + · simp only [SegND.extn_toDir, Dir.quotient_mk_eq, SegND.mkPtPt_toDir] + have : (VEC_nd A C).toDir = Dl.toDir := + calc + _= (RAY A C).toDir := by rfl + _= _ := eq_toDir_of_lt ha hc a_lt_c + simp only [this] + exact hx2 + +theorem lies_on_seg_nd_ext_of_gt_and_ge {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (a_gt_c : lelem A ha > lelem C hc) (c_ge_b : lelem C hc ≥ lelem B hb) : B LiesOn (SEG_nd A C ((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm).extension := by + haveI C_ne_A : PtNe C A := ⟨((ne_iff_ne_as_line_elem ha hc).mpr (ne_of_gt a_gt_c)).symm⟩ + rcases exist_nonneg_smul_of_le hb hc c_ge_b with ⟨x2, ⟨x2nneg, hx2⟩⟩ + apply Ray.lies_on_iff.mpr + use x2 + constructor + · exact x2nneg + · simp only [SegND.extn_toDir, Dir.quotient_mk_eq, SegND.mkPtPt_toDir] + have : (VEC_nd A C).toDir = - Dl.toDir := + calc + _= (RAY A C).toDir := by rfl + _= _ := neg_toDir_of_gt ha hc a_gt_c + simp only [this, Dir.neg_unitVec, smul_neg] + show (VEC C B) = - (x2 • Dl.toDir.unitVec) + have : (VEC C B) = - (VEC B C) := by simp only [neg_vec] + simp only [this, neg_inj, hx2] + +-- # Position Relations to Order Relations +-- linear order and LiesInt Seg +theorem lt_and_lt_of_lies_int_seg_and_le {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (hac : B LiesInt (SEG A C)) (a_le_c : lelem A ha ≤ lelem C hc) : ((lelem A ha) < (lelem B hb)) ∧ ((lelem B hb) < (lelem C hc)) := by + have a_ne_c : A ≠ C := by + by_contra h' + simp only [h'] at hac + have : C ≠ C := by exact (Seg.lies_int_iff.mp hac).1 + contradiction + have : lelem A ha ≠ lelem C hc := by + simp only [ne_eq, Subtype.mk.injEq, a_ne_c, not_false_eq_true] + have : lelem A ha < lelem C hc := by + apply lt_of_le_of_ne a_le_c this + rcases (exist_pos_smul_of_lt ha hc this) with ⟨x1, ⟨x1pos, hx1⟩⟩ + rcases (Seg.lies_int_iff.mp hac) with ⟨_, ⟨x2, ⟨x2pos, ⟨x2lt1, hx2⟩⟩⟩⟩ + have : (SEG A C).toVec = (VEC A C) := by simp only [seg_toVec_eq_vec] + simp only [this] at hx2 + constructor + · apply lt_of_exist_pos_smul ha hb + use x2 * x1 + constructor + · positivity + · simp only [mul_smul, hx1.symm] + exact hx2 + · apply lt_of_exist_pos_smul hb hc + use (1 - x2) * x1 + constructor + · simp only [gt_iff_lt, x1pos, mul_pos_iff_of_pos_right, sub_pos, x2lt1] + · simp only [mul_smul, hx1.symm] + calc + _= (VEC A C) - (VEC A B) := by simp only [vec_sub_vec] + _= 1 • (VEC A C) - x2 • (VEC A C) := by congr 1; simp only [one_smul] + _= 1 • (VEC A C) + (- x2) • (VEC A C) := by simp only [one_smul, neg_smul]; exact rfl + _= (1 + (-x2)) • (VEC A C) := by symm; simp only [add_smul 1 (-x2) (VEC A C), one_smul, neg_smul] + _= _ := by congr 1; + +theorem ord_of_lies_int_seg {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (hac : B LiesInt (SEG A C)) : (((lelem A ha) < (lelem B hb)) ∧ ((lelem B hb) < (lelem C hc))) ∨ (((lelem A ha) > (lelem B hb)) ∧ ((lelem B hb) > (lelem C hc))) := by + have : lelem A ha ≠ lelem C hc := by + have a_ne_c : A ≠ C := by + by_contra h' + simp only [h'] at hac + have : C ≠ C := by exact (Seg.lies_int_iff.mp hac).1 + contradiction + simp only [ne_eq, Subtype.mk.injEq, a_ne_c, not_false_eq_true] + have : (lelem A ha ≤ lelem C hc) ∨ (lelem C hc ≤ lelem A ha) := le_total (lelem A ha) (lelem C hc) + rcases this with (a_le_c | c_le_a) + · left + apply lt_and_lt_of_lies_int_seg_and_le ha hb hc hac a_le_c + · right + have : lelem C hc < lelem B hb ∧ lelem B hb < lelem A ha := by + apply lt_and_lt_of_lies_int_seg_and_le hc hb ha _ c_le_a + exact Seg.lies_int_rev_iff_lies_int.mp hac + simp only [gt_iff_lt, this, and_self] + +theorem lt_iff_lt_of_lies_int_seg₁₃ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (hac : B LiesInt (SEG A C)) : (lelem A ha) < (lelem B hb) ↔ (lelem B hb) < (lelem C hc) := by + have : (((lelem A ha) < (lelem B hb)) ∧ ((lelem B hb) < (lelem C hc))) ∨ (((lelem A ha) > (lelem B hb)) ∧ ((lelem B hb) > (lelem C hc))) := ord_of_lies_int_seg ha hb hc hac + constructor + · rintro h1; by_contra h2; absurd this; push_neg + constructor + · simp only [h1, h2, not_false_eq_true, forall_true_left]; exact le_of_not_lt h2 + · simp only [gt_iff_lt, (not_lt_of_le (le_of_lt h1)), IsEmpty.forall_iff] + · rintro h1; by_contra h2; absurd this; push_neg + constructor + · rintro h3; contradiction + · rintro _; exact le_of_lt h1 + +theorem lt_iff_lt_of_lies_int_seg₁₂ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (hac : B LiesInt (SEG A C)) : (lelem A ha) < (lelem B hb) ↔ (lelem A ha) < (lelem C hc) := by + have : (((lelem A ha) < (lelem B hb)) ∧ ((lelem B hb) < (lelem C hc))) ∨ (((lelem A ha) > (lelem B hb)) ∧ ((lelem B hb) > (lelem C hc))) := ord_of_lies_int_seg ha hb hc hac + constructor + · rintro h1; by_contra h2; absurd this; push_neg + constructor + · rintro _; by_contra h3; absurd h2; exact lt_trans h1 (lt_of_not_le h3) + · simp only [gt_iff_lt, not_lt_of_le (le_of_lt h1), IsEmpty.forall_iff] + · by_contra h3; push_neg at h3 + rcases this with (hl | hr) + · absurd hl; push_neg at hl; simp only [not_and]; rintro h4; exfalso; absurd h4; exact not_lt_of_le h3.2 + · have : lelem A ha > lelem C hc := gt_trans hr.1 hr.2 + have : ¬ lelem A ha < lelem C hc := not_lt_of_le (le_of_lt (lt_trans hr.2 hr.1)) + absurd this; exact h3.1 + +theorem lt_iff_lt_of_lies_int_seg₂₃ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (hac : B LiesInt (SEG A C)) : (lelem A ha) < (lelem C hc) ↔ (lelem B hb) < (lelem C hc) := by + simp only [(lt_iff_lt_of_lies_int_seg₁₂ ha hb hc hac).symm, + (lt_iff_lt_of_lies_int_seg₁₃ ha hb hc hac)] + +-- linear order and LiesOn seg +theorem le_and_le_of_lies_on_seg_and_le {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (hac : B LiesOn (SEG A C)) (a_le_c : lelem A ha ≤ lelem C hc) : ((lelem A ha) ≤ (lelem B hb)) ∧ ((lelem B hb) ≤ (lelem C hc)) := by + rcases eq_or_ne B A with (heq | h1) + simp only [heq, le_refl, a_le_c, and_self] + rcases eq_or_ne B C with (heq | h2) + simp only [heq, a_le_c, le_refl, and_self] + have : B LiesInt (SEG A C) := by + refine' ⟨hac, h1, h2⟩ + exact ⟨le_of_lt (lt_and_lt_of_lies_int_seg_and_le ha hb hc this a_le_c).1, le_of_lt (lt_and_lt_of_lies_int_seg_and_le ha hb hc this a_le_c).2⟩ + +theorem ord_of_lies_on_seg {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (SEG A C)) : (lelem A ha ≤ lelem B hb ∧ lelem B hb ≤ lelem C hc) ∨ (lelem A ha ≥ lelem B hb ∧ lelem B hb ≥ lelem C hc) := by + have : (lelem A ha ≤ lelem C hc) ∨ (lelem C hc ≤ lelem A ha) := le_total (lelem A ha) (lelem C hc) + rcases this with (a_le_c | c_le_a) + · left + exact le_and_le_of_lies_on_seg_and_le ha hb hc h a_le_c + · right + have : lelem C hc ≤ lelem B hb ∧ lelem B hb ≤ lelem A ha := by + apply le_and_le_of_lies_on_seg_and_le hc hb ha _ c_le_a + exact Seg.lies_on_rev_iff_lies_on.mp h + simp only [ge_iff_le, this, and_self] + +theorem le_of_lies_on_seg_and_lt₃₁ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (SEG A C)) (h1 : lelem A ha < lelem B hb) : lelem B hb ≤ lelem C hc := by + have : (lelem A ha ≤ lelem B hb ∧ lelem B hb ≤ lelem C hc) ∨ (lelem A ha ≥ lelem B hb ∧ lelem B hb ≥ lelem C hc) := ord_of_lies_on_seg ha hb hc h + rcases this with (hl | hr) + · exact hl.2 + · exfalso; absurd hr.1; exact not_le_of_lt h1 + +theorem lt_of_lies_on_seg_and_lt₂₁ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (SEG A C)) (h1 : lelem A ha < lelem B hb) : lelem A ha < lelem C hc := lt_of_lt_of_le h1 (le_of_lies_on_seg_and_lt₃₁ ha hb hc h h1) + +theorem le_of_lies_on_seg_and_lt₁₃ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (SEG A C)) (h3 : lelem B hb < lelem C hc) : lelem A ha ≤ lelem B hb := by + have : (lelem A ha ≤ lelem B hb ∧ lelem B hb ≤ lelem C hc) ∨ (lelem A ha ≥ lelem B hb ∧ lelem B hb ≥ lelem C hc) := ord_of_lies_on_seg ha hb hc h + rcases this with (hl | hr) + · exact hl.1 + · exfalso; absurd hr.2; exact not_le_of_lt h3 + +theorem lt_of_lies_on_seg_and_lt₂₃ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (SEG A C)) (h3 : lelem B hb < lelem C hc) : lelem A ha < lelem C hc := lt_of_le_of_lt (le_of_lies_on_seg_and_lt₁₃ ha hb hc h h3) h3 + +theorem le_of_lies_on_seg_and_le₁₂ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (SEG A C)) (h2 : lelem A ha ≤ lelem C hc) : lelem A ha ≤ lelem B hb := by + have : (lelem A ha ≤ lelem B hb ∧ lelem B hb ≤ lelem C hc) ∨ (lelem A ha ≥ lelem B hb ∧ lelem B hb ≥ lelem C hc) := ord_of_lies_on_seg ha hb hc h + rcases this with (hl | hr) + · exact hl.1 + · exact le_trans h2 hr.2 + +theorem le_of_lies_on_seg_and_le₃₂ {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (SEG A C)) (h2 : lelem A ha ≤ lelem C hc) : lelem B hb ≤ lelem C hc := by + have : (lelem A ha ≤ lelem B hb ∧ lelem B hb ≤ lelem C hc) ∨ (lelem A ha ≥ lelem B hb ∧ lelem B hb ≥ lelem C hc) := ord_of_lies_on_seg ha hb hc h + rcases this with (hl | hr) + · exact hl.2 + · exact le_trans hr.1 h2 + +-- linear order and LiesInt ray +theorem lt_iff_lt_of_lies_int_ray {Dl : DirLine P} {A B C : P} [hh : PtNe A C] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesInt (RAY A C)) : lelem A ha < lelem C hc ↔ lelem A ha < lelem B hb := by + rcases Ray.lies_int_iff.mp h with ⟨x2, ⟨x2pos, hx2⟩⟩ + rcases Ray.lies_int_iff.mp (Ray.snd_pt_lies_int_mk_pt_pt A C) with ⟨x1, ⟨x1pos, hx1⟩⟩ + have h1 : (VEC A C) = (x1 / x2) • (VEC A B) := by + calc + _= x1 • (RAY A C).toDir.unitVec := hx1 + _= ((x1 / x2) * x2) • (RAY A C).toDir.unitVec := by + congr 1; symm; apply div_mul_cancel_of_imp + by_contra h'; push_neg at h'; linarith + _= (x1 / x2) • (x2 • (RAY A C).toDir.unitVec) := by apply mul_smul + _= _ := by congr 1; symm; exact hx2 + have h2 : (VEC A B) = (x2 / x1) • (VEC A C) := by + calc + _= x2 • (RAY A C).toDir.unitVec := hx2 + _= ((x2 / x1) * x1) • (RAY A C).toDir.unitVec := by + congr 1; symm; apply div_mul_cancel_of_imp + by_contra h'; push_neg at h'; linarith + _= (x2 / x1) • (x1 • (RAY A C).toDir.unitVec) := by apply mul_smul + _= _ := by congr 1; symm; exact hx1 + constructor + · rintro h1; rcases exist_pos_smul_of_lt ha hc h1 with ⟨x3, ⟨x3pos, hx3⟩⟩ + apply lt_of_exist_pos_smul; use (x2 / x1) * x3 + constructor + · positivity + · symm; + calc + _= (x2 / x1) • (x3 • Dl.toDir.unitVec) := by apply mul_smul + _= (x2 / x1) • (VEC A C) := by simp only [hx3] + _= _ := by symm; exact h2 + · rintro h2; rcases exist_pos_smul_of_lt ha hb h2 with ⟨x3, ⟨x3pos, hx3⟩⟩ + apply lt_of_exist_pos_smul; use (x1 / x2) * x3 + constructor + · positivity + · symm; + calc + _= (x1 / x2) • (x3 • Dl.toDir.unitVec) := by apply mul_smul + _= (x1 / x2) • (VEC A B) := by simp only [hx3] + _= _ := by symm; exact h1 + +-- linear order and LiesOn ray +theorem lt_of_lies_on_ray_and_lt {Dl : DirLine P} {A B C : P} [hh : PtNe A C] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (RAY A C)) (h1 : lelem A ha < lelem B hb) : lelem A ha < lelem C hc := by + have : lelem A ha ≠ lelem B hb := ne_of_lt h1 + have : B ≠ A := by symm; exact (ne_iff_ne_as_line_elem ha hb).mpr this + have : B LiesInt (RAY A C) := by refine' ⟨h, this⟩ + exact (lt_iff_lt_of_lies_int_ray ha hb hc this).mpr h1 + +theorem le_of_lies_on_ray_and_lt {Dl : DirLine P} {A B C : P} [hh : PtNe A C] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : B LiesOn (RAY A C)) (h1 : lelem A ha < lelem C hc) : lelem A ha ≤ lelem B hb := by + rcases eq_or_ne A B with (heq | hne) + · simp only [heq, le_refl] + · have : B LiesInt (RAY A C) := by refine' ⟨h, hne.symm⟩ + exact le_of_lt ((lt_iff_lt_of_lies_int_ray ha hb hc this).mp h1) + +-- linear order and toDir +theorem lt_of_eq_toDir {Dl : DirLine P} {A B : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (h : (RAY A B).toDir = Dl.toDir) : lelem A ha < lelem B hb := by + rcases Ray.lies_int_iff.mp (Ray.snd_pt_lies_int_mk_pt_pt A B) with ⟨x1, ⟨x1pos, hx1⟩⟩ + simp only [h] at hx1 + apply lt_of_exist_pos_smul; use x1; + constructor + · exact x1pos + · show VEC (RAY A B).source B = x1 • Dl.toDir.unitVec + exact hx1 + +theorem gt_of_neg_toDir {Dl : DirLine P} {A B : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (h : (RAY A B).toDir = - Dl.toDir) : lelem A ha > lelem B hb := by + have : (RAY B A).toDir = Dl.toDir := by + calc + _= (SEG_nd B A).toDir := by rfl + _= - (SEG_nd A B).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd A B)) + _= - (RAY A B).toDir := by congr 1; + _= - - Dl.toDir := by simp only [h] + _= _ := by simp only [neg_neg] + exact lt_of_eq_toDir hb ha this + +-- linear order and LiesInt SegND.extension +/- +-- `to be used for tactic testing` +theorem ord_of_lies_int_seg_nd_ext {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesInt (SEG_nd A B).extension) : ((lelem A ha < lelem B hb) ∧ (lelem B hb < lelem C hc)) ∨ ((lelem A ha > lelem B hb) ∧ (lelem B hb > lelem C hc)) := by sorry + +theorem lt_iff_lt_of_lies_int_seg_ne_ext₁₂ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesInt (SEG_nd A B).extension) : lelem A ha < lelem B hb ↔ lelem A ha < lelem C hc := by sorry + +theorem lt_iff_lt_of_lies_int_seg_ne_ext₁₃ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesInt (SEG_nd A B).extension) : lelem A ha < lelem B hb ↔ lelem B hb < lelem C hc := by sorry + +theorem lt_iff_lt_of_lies_int_seg_ne_ext₂₃ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesInt (SEG_nd A B).extension) : lelem A ha < lelem C hc ↔ lelem B hb < lelem C hc := by sorry +-/ + +-- linear order and LiesOn SegND.extension +/- +-- `to be used for tactic testing` +theorem ord_of_lies_on_seg_nd_ext {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesOn (SEG_nd A B).extension) : ((lelem A ha < lelem B hb) ∧ (lelem B hb ≤ lelem C hc)) ∨ ((lelem A ha > lelem B hb) ∧ (lelem B hb ≥ lelem C hc)) := by sorry + +theorem le_of_lies_on_seg_nd_ext_and_le₃₁ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesOn (SEG_nd A B).extension) (h1 : lelem A ha ≤ lelem B hb) : lelem B hb ≤ lelem C hc := by sorry + +theorem lt_of_lies_on_seg_nd_ext_and_le₂₁ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesOn (SEG_nd A B).extension) (h1 : lelem A ha ≤ lelem B hb) : lelem A ha < lelem C hc := by sorry + +theorem le_of_lies_on_seg_nd_ext_and_le₃₂ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesOn (SEG_nd A B).extension) (h2 : lelem A ha ≤ lelem C hc) : lelem B hb ≤ lelem C hc := by sorry + +theorem lt_of_lies_on_seg_nd_ext_and_le₁₂ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesOn (SEG_nd A B).extension) (h2 : lelem A ha ≤ lelem C hc) : lelem A ha < lelem B hb := by sorry + +theorem lt_of_lies_on_seg_nd_ext_and_lt₁₃ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesOn (SEG_nd A B).extension) (h3 : lelem B hb < lelem C hc) : lelem A ha < lelem B hb := by sorry + +theorem lt_of_lies_on_seg_nd_ext_and_lt₂₃ {Dl : DirLine P} {A B C : P} [a_ne_b : PtNe A B] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) (h : C LiesOn (SEG_nd A B).extension) (h3 : lelem B hb < lelem C hc) : lelem A ha < lelem C hc := by sorry +-/ + +-- # Corollary +-- `Hilbert Axioms II.3` +theorem lies_on_or_lies_on_or_lies_on_of_lies_on_DirLine {Dl : DirLine P} {A B C : P} (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) : (A LiesOn (SEG B C)) ∨ (B LiesOn (SEG A C)) ∨ (C LiesOn (SEG A B)) := by + rcases le_total (lelem A ha) (lelem B hb) with (a_le_b | b_le_a) + · rcases le_total (lelem B hb) (lelem C hc) with (b_le_c | c_le_b) + · right; left; exact lies_on_seg_of_le_and_le ha hb hc a_le_b b_le_c + · rcases le_total (lelem A ha) (lelem C hc) with (a_le_c | c_le_a) + · right; right; exact lies_on_seg_of_le_and_le ha hc hb a_le_c c_le_b + · left; exact lies_on_seg_of_ge_and_ge hb ha hc a_le_b c_le_a + · rcases le_total (lelem B hb) (lelem C hc) with (b_le_c | c_le_b) + · rcases le_total (lelem A ha) (lelem C hc) with (a_le_c | c_le_a) + · left; exact lies_on_seg_of_le_and_le hb ha hc b_le_a a_le_c + · right; right; exact lies_on_seg_of_ge_and_ge ha hc hb c_le_a b_le_c + · right; left; exact lies_on_seg_of_ge_and_ge ha hb hc b_le_a c_le_b + +theorem lies_on_or_lies_on_or_lies_on_of_lies_on_Line {l : Line P} {A B C : P} (ha : A LiesOn l) (hb : B LiesOn l) (hc : C LiesOn l) : (A LiesOn (SEG B C)) ∨ (B LiesOn (SEG A C)) ∨ (C LiesOn (SEG A B)) := by + rcases eq_or_ne A B with (a_eq_b | a_ne_b) + · left; simp only [a_eq_b]; apply Seg.source_lies_on + · haveI : PtNe A B := ⟨a_ne_b⟩ + have : (RAY A B).toDirLine.toLine = l := by + calc + _= (LIN A B) := by rfl + _= _ := by + apply Line.eq_of_pt_pt_lies_on_of_ne _ _ ha hb + apply Line.fst_pt_lies_on_mk_pt_pt + apply Line.snd_pt_lies_on_mk_pt_pt + have h1 : A LiesOn (RAY A B).toDirLine := by + apply DirLine.lies_on_iff_lies_on_toLine.mp + simp only [this]; exact ha + have h2 : B LiesOn (RAY A B).toDirLine := by + apply DirLine.lies_on_iff_lies_on_toLine.mp + simp only [this]; exact hb + have h3 : C LiesOn (RAY A B).toDirLine := by + apply DirLine.lies_on_iff_lies_on_toLine.mp + simp only [this]; exact hc + exact lies_on_or_lies_on_or_lies_on_of_lies_on_DirLine h1 h2 h3 + +theorem lies_on_or_lies_on_or_lies_on_of_collinear {A B C : P} (h : Collinear A B C) : (A LiesOn (SEG B C)) ∨ (B LiesOn (SEG A C)) ∨ (C LiesOn (SEG A B)) := by + rcases exist_line_of_collinear h with ⟨l, ⟨ha, ⟨hb, hc⟩⟩⟩ + exact lies_on_or_lies_on_or_lies_on_of_lies_on_Line ha hb hc + +theorem lies_int_or_lies_int_or_lies_int_of_lies_on_DirLine {Dl : DirLine P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) : (A LiesInt (SEG B C)) ∨ (B LiesInt (SEG A C)) ∨ (C LiesInt (SEG A B)) := by + rcases lies_on_or_lies_on_or_lies_on_of_lies_on_DirLine ha hb hc with (h1 | (h2 | h3)) + · left; refine' ⟨h1, hh1.out, hh2.out⟩ + · right; left; refine' ⟨h2, hh1.out.symm, hh3.out⟩ + · right; right; refine' ⟨h3, hh2.out.symm, hh3.out.symm⟩ + +theorem lies_int_or_lies_int_or_lies_int_of_lies_on_Line {l : Line P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn l) (hb : B LiesOn l) (hc : C LiesOn l) : (A LiesInt (SEG B C)) ∨ (B LiesInt (SEG A C)) ∨ (C LiesInt (SEG A B)) := by + rcases lies_on_or_lies_on_or_lies_on_of_lies_on_Line ha hb hc with (h1 | (h2 | h3)) + · left; refine' ⟨h1, hh1.out, hh2.out⟩ + · right; left; refine' ⟨h2, hh1.out.symm, hh3.out⟩ + · right; right; refine' ⟨h3, hh2.out.symm, hh3.out.symm⟩ + +theorem lies_int_or_lies_int_or_lies_int_of_collinear {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (h : Collinear A B C) : (A LiesInt (SEG B C)) ∨ (B LiesInt (SEG A C)) ∨ (C LiesInt (SEG A B)) := by + rcases lies_on_or_lies_on_or_lies_on_of_collinear h with (h1 | (h2 | h3)) + · left; refine' ⟨h1, hh1.out, hh2.out⟩ + · right; left; refine' ⟨h2, hh1.out.symm, hh3.out⟩ + · right; right; refine' ⟨h3, hh2.out.symm, hh3.out.symm⟩ + +theorem not_lies_int_and_lies_int₁ (A B C : P) : ¬ (B LiesInt (SEG A C) ∧ C LiesInt (SEG A B)) := by + by_contra h + rcases Seg.lies_int_iff.mp h.1 with ⟨h1, ⟨x1, ⟨x1pos, ⟨x1lt1, hx1⟩⟩⟩⟩ + rcases Seg.lies_int_iff.mp h.2 with ⟨_, ⟨x2, ⟨_, ⟨x2lt1, hx2⟩⟩⟩⟩ + haveI : PtNe C A := ⟨h1⟩ + have : (VEC A C) = (x2 * x1) • (VEC A C) := by + calc + _= x2 • (VEC A B) := by + show VEC (SEG A B).source C = x2 • (SEG A B).toVec + exact hx2 + _= x2 • x1 • (VEC A C) := by congr 1; + _= (x2 * x1) • (VEC A C) := by symm; apply mul_smul + have : (x2 * x1 - 1) • (VEC A C) = 0 := by + calc + _= (x2 * x1) • (VEC A C) - (1 : ℝ) • (VEC A C) := by apply sub_smul + _= (VEC A C) - (VEC A C) := by simp only [this.symm, one_smul] + _= 0 := by simp only [sub_self] + simp at this + have h2 : x2 * x1 < (1 : ℝ) := by + calc + _< (1 : ℝ) * 1 := by + apply mul_lt_mul x2lt1 (le_of_lt x1lt1) x1pos _ + norm_num + _= (1 : ℝ) := by norm_num + have h2 : x2 * x1 - 1 ≠ 0 := by linarith + simp only [h2, false_or] at this + have : C = A := (eq_iff_vec_eq_zero A C).mpr this + absurd h1; exact this + +theorem not_lies_int_and_lies_int₂ (A B C : P) : ¬ (A LiesInt (SEG B C) ∧ C LiesInt (SEG A B)) := by + by_contra h + have : ¬ (A LiesInt (SEG B C) ∧ C LiesInt (SEG B A)) := not_lies_int_and_lies_int₁ B A C + absurd this + exact ⟨h.1, Seg.lies_int_rev_iff_lies_int.mpr h.2⟩ + +theorem not_lies_int_and_lies_int₃ (A B C : P) : ¬ (A LiesInt (SEG B C) ∧ B LiesInt (SEG A C)) := by + by_contra h + have : _ := not_lies_int_and_lies_int₁ C A B + absurd this + exact ⟨Seg.lies_int_rev_iff_lies_int.mpr h.1, Seg.lies_int_rev_iff_lies_int.mpr h.2⟩ + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_DirLine₁ {Dl : DirLine P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) : (A LiesInt (SEG B C)) ↔ ((¬ B LiesInt (SEG A C)) ∧ (¬ C LiesInt (SEG A B))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_lies_on_DirLine ha hb hc + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_DirLine₂ {Dl : DirLine P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) : (B LiesInt (SEG A C)) ↔ ((¬ A LiesInt (SEG B C)) ∧ (¬ C LiesInt (SEG A B))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_lies_on_DirLine ha hb hc + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_DirLine₃ {Dl : DirLine P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn Dl) (hb : B LiesOn Dl) (hc : C LiesOn Dl) : (C LiesInt (SEG A B)) ↔ ((¬ A LiesInt (SEG B C)) ∧ (¬ B LiesInt (SEG A C))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_lies_on_DirLine ha hb hc + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_Line₁ {l : Line P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn l) (hb : B LiesOn l) (hc : C LiesOn l) : (A LiesInt (SEG B C)) ↔ ((¬ B LiesInt (SEG A C)) ∧ (¬ C LiesInt (SEG A B))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_lies_on_Line ha hb hc + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_Line₂ {l : Line P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn l) (hb : B LiesOn l) (hc : C LiesOn l) : (B LiesInt (SEG A C)) ↔ ((¬ A LiesInt (SEG B C)) ∧ (¬ C LiesInt (SEG A B))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_lies_on_Line ha hb hc + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_Line₃ {l : Line P} {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (ha : A LiesOn l) (hb : B LiesOn l) (hc : C LiesOn l) : (C LiesInt (SEG A B)) ↔ ((¬ A LiesInt (SEG B C)) ∧ (¬ B LiesInt (SEG A C))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_lies_on_Line ha hb hc + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_collinear₁ {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (h : Collinear A B C) : (A LiesInt (SEG B C)) ↔ ((¬ B LiesInt (SEG A C)) ∧ (¬ C LiesInt (SEG A B))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_collinear h + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_collinear₂ {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (h : Collinear A B C) : (B LiesInt (SEG A C)) ↔ ((¬ A LiesInt (SEG B C)) ∧ (¬ C LiesInt (SEG A B))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_collinear h + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +theorem lies_int_iff_not_lies_int_and_not_lies_int_of_collinear₃ {A B C : P} [hh1 : PtNe A B] [hh2 : PtNe A C] [hh3 : PtNe B C] (h : Collinear A B C) : (C LiesInt (SEG A B)) ↔ ((¬ A LiesInt (SEG B C)) ∧ (¬ B LiesInt (SEG A C))) := by + have hh0 : _ := lies_int_or_lies_int_or_lies_int_of_collinear h + have hh1 : _ := not_lies_int_and_lies_int₁ A B C + have hh2 : _ := not_lies_int_and_lies_int₂ A B C + have hh3 : _ := not_lies_int_and_lies_int₃ A B C + tauto + +end linear_order +end DirLine + +end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean index b7b9b708..f1c02171 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean @@ -1,6 +1,6 @@ -import EuclideanGeometry.Foundation.Index import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular +import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex2 namespace EuclidGeom @@ -8,12 +8,18 @@ variable {P : Type*} [EuclideanPlane P] theorem perp_foot_lies_int_ray_of_acute_ang {A B C : P} (b_ne_a : B ≠ A) (c_ne_a : C ≠ A) (acu : Angle.IsAcu (ANG B A C b_ne_a c_ne_a)) : (perp_foot C (LIN A B b_ne_a)) LiesInt (RAY A B b_ne_a) := by sorry -theorem ang_acute_of_is_isoceles {A B C : P} (not_collinear_ABC : ¬ Collinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcu (ANG C B A (ne_of_not_collinear not_collinear_ABC).1 (ne_of_not_collinear not_collinear_ABC).2.2.symm) := by sorry +theorem perp_foot_lies_int_ray_rev_of_acute_ang {A B C : P} [b_ne_a : PtNe B A] [c_ne_a : PtNe C A] (obt : Angle.IsObt (ANG B A C)) : (perp_foot C (LIN A B)) LiesInt (RAY A B).reverse := by sorry -theorem ang_acute_of_is_isoceles_variant {A B C : P} (not_collinear_ABC : ¬ Collinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcu (ANG A C B (ne_of_not_collinear not_collinear_ABC).2.1 (ne_of_not_collinear not_collinear_ABC).1.symm) := by sorry +theorem perp_foot_eq_source_of_right_ang {A B C : P} [b_ne_a : PtNe B A] [c_ne_a : PtNe C A] (rgt : Angle.IsRight (ANG B A C)) : (perp_foot C (LIN A B)) = A := by sorry theorem is_acute_of_is_acute_rev {O A B : P} (h1 : A ≠ O) (h2 : B ≠ O) (h3 : Angle.IsAcu (ANG A O B h1 h2)) : Angle.IsAcu (ANG B O A h2 h1) := by sorry theorem ang_eq_ang_of_toDir_eq_neg_toDir {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = - ang₂.start_ray.toDir) (he : ang₁.end_ray.toDir = - ang₂.end_ray.toDir) : Angle.value ang₁ = Angle.value ang₂ := by sorry +theorem ang_value_eq_ang_value_add_ang_value (A B C O : P) [hne1 : PtNe A O] [hne2 : PtNe B O] [hne3 : PtNe C O]: (∠ A O B) + (∠ B O C) = (∠ A O C) := by + symm; + apply Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang (ANG A O B) (ANG B O C) _ + unfold Angle.mk_pt_pt_pt + rfl + end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean index 86a556fa..fe409ebe 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean @@ -9,5 +9,6 @@ theorem Triangle.IsCongr.unique_of_eq_eq {tr₁ tr₂ : Triangle P} (h : tr₁.I theorem acongr_of_AAS_variant (tr_nd₁ tr_nd₂ : TriangleND P) (a₁ : tr_nd₁.angle₁.dvalue = - tr_nd₂.angle₁.dvalue) (a₂ : tr_nd₁.angle₂.value = - tr_nd₂.angle₂.value) (e₃ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) : tr_nd₁ ≅ₐ tr_nd₂ := by sorry +theorem acongr_of_AAS' (tr_nd₁ tr_nd₂ : TriangleND P) (a₁ : tr_nd₁.angle₁.value = - tr_nd₂.angle₁.value) (a₂ : tr_nd₁.angle₂.value = - tr_nd₂.angle₂.value) (e₃ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) : tr_nd₁ ≅ₐ tr_nd₂ := by sorry end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean index 442e5127..ec5c1392 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean @@ -9,4 +9,8 @@ lemma isoceles_tri_pts_ne {tri : Triangle P} (h : tri.IsIsoceles) (hne : tri.poi theorem is_isoceles_tri_ang_eq_ang_of_tri {tri : Triangle P} (h : tri.IsIsoceles) (hne : tri.point₂ ≠ tri.point₃) : ∠ tri.point₃ tri.point₂ tri.point₁ hne.symm (isoceles_tri_pts_ne h hne).1 = ∠ tri.point₁ tri.point₃ tri.point₂ (isoceles_tri_pts_ne h hne).2 hne := by sorry +theorem ang_acute_of_is_isoceles {A B C : P} (not_colinear_ABC : ¬ Collinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcu (ANG C B A (ne_of_not_collinear not_colinear_ABC).1 (ne_of_not_collinear not_colinear_ABC).2.2.symm) := by sorry + +theorem ang_acute_of_is_isoceles_variant {A B C : P} (not_collinear_ABC : ¬ Collinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcu (ANG A C B (ne_of_not_collinear not_collinear_ABC).2.1 (ne_of_not_collinear not_collinear_ABC).1.symm) := by sorry + end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean index eb4a71de..d1e46bc9 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean @@ -4,7 +4,7 @@ namespace EuclidGeom variable {P : Type*} [EuclideanPlane P] -theorem vec_eq_of_eq_dir_and_eq_length {A B C D : P} (h1 : B ≠ A) (h2 : D ≠ C) (h3 : (SEG_nd A B h1).toDir = (SEG_nd C D h2).toDir) (h4 : (SEG A B).length = (SEG C D).length) : VEC A B = VEC C D := by sorry +theorem vec_eq_of_eq_dir_and_eq_length {A B C D : P} [h1 : PtNe B A] [h2 : PtNe D C] (h3 : (SEG_nd A B).toDir = (SEG_nd C D).toDir) (h4 : (SEG A B).length = (SEG C D).length) : VEC A B = VEC C D := by sorry /-- In the main file already. -/ theorem is_prg_nd_of_diag_inx_eq_mid_eq_mid_variant_1 {A B C D : P} (h : (QDR A B C D).IsConvex) (h' : (SEG A C).midpoint = (SEG B D).midpoint) : ((QDR_cvx A B C D h).toQuadrilateral).IsParallelogramND := by sorry diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter_trash.lean b/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter_trash.lean new file mode 100644 index 00000000..1e9552d6 --- /dev/null +++ b/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter_trash.lean @@ -0,0 +1,13 @@ +import EuclideanGeometry.Foundation.Axiom.Triangle.Basic +import EuclideanGeometry.Foundation.Construction.Triangle.Orthocenter +import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex + +noncomputable section +namespace EuclidGeom + +variable {P : Type _} [EuclideanPlane P] + +namespace TriangleND +theorem perp_foot_lies_int_edge_of_acute_acute₁ (tr_nd : TriangleND P) (acu₂ : Angle.IsAcuteAngle tr_nd.angle₂) (acu₃ : Angle.IsAcuteAngle tr_nd.angle₂) : (perp_foot tr_nd.point₁ tr_nd.edge_nd₁.toLine) LiesInt tr_nd.edge_nd₁ := sorry +end TriangleND +end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Index.lean b/EuclideanGeometry/Foundation/Index.lean index f0965524..ae8a8815 100644 --- a/EuclideanGeometry/Foundation/Index.lean +++ b/EuclideanGeometry/Foundation/Index.lean @@ -9,6 +9,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash import EuclideanGeometry.Foundation.Axiom.Linear.Collinear import EuclideanGeometry.Foundation.Axiom.Linear.Line import EuclideanGeometry.Foundation.Axiom.Linear.Class +import EuclideanGeometry.Foundation.Axiom.Linear.Order import EuclideanGeometry.Foundation.Axiom.Linear.Parallel import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular /- Axiom.Position -/