From 9ad02a612f4d6d2dd4e92737e318e11bd9142d1b Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Thu, 11 Jan 2024 23:10:43 +0800 Subject: [PATCH] 1.11 change names in LCPosition --- .../Foundation/Axiom/Circle/CirclePower.lean | 190 +++++++++--------- .../Foundation/Axiom/Circle/LCPosition.lean | 150 +++++++------- 2 files changed, 174 insertions(+), 166 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean index c951d545..ff61fcf4 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean @@ -8,6 +8,8 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] +open DirLC + namespace Circle -- Define the power of a point P relative to a circle ω with center O and radius r to be OP ^ 2 - r ^ 2 @@ -146,23 +148,23 @@ theorem line_tangent_circle {ω : Circle P} {p : P} (h : p LiesOut ω) : ((DLIN · apply pt_pt_perp_tangent h (tangents_lieson_circle h).1 (tangents_perp₁ h) apply pt_pt_perp_tangent h (tangents_lieson_circle h).2 (tangents_perp₂ h) -theorem tangent_pts_eq_tangents {ω : Circle P} {p : P} (h : p LiesOut ω) : (DirLC_Tangent_pt (line_tangent_circle h).1 = (pt_tangent_circle_pts h).left) ∧ (DirLC_Tangent_pt (line_tangent_circle h).2 = (pt_tangent_circle_pts h).right) := by +theorem tangent_pts_eq_tangents {ω : Circle P} {p : P} (h : p LiesOut ω) : (Tangentpt (line_tangent_circle h).1 = (pt_tangent_circle_pts h).left) ∧ (Tangentpt (line_tangent_circle h).2 = (pt_tangent_circle_pts h).right) := by constructor · symm apply pt_pt_perp_eq_tangent_pt h (tangents_lieson_circle h).1 (tangents_perp₁ h) symm apply pt_pt_perp_eq_tangent_pt h (tangents_lieson_circle h).2 (tangents_perp₂ h) -lemma tangent_length_sq_eq_power {p : P} {l : DirLine P} {ω : Circle P} (h₁ : l Tangent ω) (h₂ : p LiesOn l) : (dist p (DirLC_Tangent_pt h₁)) ^ 2 = power ω p := by +lemma tangent_length_sq_eq_power {p : P} {l : DirLine P} {ω : Circle P} (h₁ : l Tangent ω) (h₂ : p LiesOn l) : (dist p (Tangentpt h₁)) ^ 2 = power ω p := by calc - _ = (dist p (perp_foot ω.center l)) ^ 2 := by rw [DirLC_tangent_pt_eq_perp_foot] + _ = (dist p (perp_foot ω.center l)) ^ 2 := by rw [tangent_pt_eq_perp_foot] _ = (dist ω.center p) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2 := by rw [eq_sub_iff_add_eq, add_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] apply Pythagoras_of_perp_foot _ _ h₂ - _ = (dist ω.center p) ^ 2 - (dist ω.center (DirLC_Tangent_pt h₁)) ^ 2 := by rw [DirLC_tangent_pt_eq_perp_foot] + _ = (dist ω.center p) ^ 2 - (dist ω.center (Tangentpt h₁)) ^ 2 := by rw [tangent_pt_eq_perp_foot] _ = (dist ω.center p) ^ 2 - ω.radius ^ 2 := by congr - exact (DirLC_inx_pts_lieson_circle (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h₁))).1 + exact (inx_pts_lieson_circle (intersect_iff_tangent_or_secant.mpr (Or.inl h₁))).1 _ = power ω p := rfl theorem length_of_tangent {ω : Circle P} {p : P} (h : p LiesOut ω) : dist p (pt_tangent_circle_pts h).left = dist p (pt_tangent_circle_pts h).right := by @@ -181,80 +183,80 @@ section position namespace Circle -lemma liesout_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (p ≠ (DirLC_inx_pts h₁).front) ∧ (p ≠ (DirLC_inx_pts h₁).back) := by +lemma liesout_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (p ≠ (Inxpts h₁).front) ∧ (p ≠ (Inxpts h₁).back) := by constructor - · apply (pt_liesout_ne_pt_lieson h₃ (DirLC_inx_pts_lieson_circle h₁).1).out - apply (pt_liesout_ne_pt_lieson h₃ (DirLC_inx_pts_lieson_circle h₁).2).out + · apply (pt_liesout_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).1).out + apply (pt_liesout_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).2).out -lemma liesint_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (p ≠ (DirLC_inx_pts h₁).front) ∧ (p ≠ (DirLC_inx_pts h₁).back) := by +lemma liesint_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (p ≠ (Inxpts h₁).front) ∧ (p ≠ (Inxpts h₁).back) := by constructor - · apply (pt_liesint_ne_pt_lieson h₃ (DirLC_inx_pts_lieson_circle h₁).1).out - apply (pt_liesint_ne_pt_lieson h₃ (DirLC_inx_pts_lieson_circle h₁).2).out + · apply (pt_liesint_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).1).out + apply (pt_liesint_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).2).out -theorem liesout_back_lieson_ray_front {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (DirLC_inx_pts h₁).back LiesOn (RAY p (DirLC_inx_pts h₁).front (liesout_ne_inxpts h₁ h₂ h₃).1.symm) := by - haveI : PtNe p (DirLC_inx_pts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ - by_cases heq : (DirLC_inx_pts h₁).front = (DirLC_inx_pts h₁).back +theorem liesout_back_lieson_ray_front {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front (liesout_ne_inxpts h₁ h₂ h₃).1.symm) := by + haveI : PtNe p (Inxpts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ + by_cases heq : (Inxpts h₁).front = (Inxpts h₁).back · simp_rw [← heq] apply Ray.snd_pt_lies_on_mk_pt_pt - haveI : PtNe (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back := ⟨heq⟩ - have eq₁ : LIN (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (DirLC_inx_pts_lieson_dlin h₁).1 (DirLC_inx_pts_lieson_dlin h₁).2 - have h₂' : p LiesOn (LIN (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back) := by + haveI : PtNe (Inxpts h₁).front (Inxpts h₁).back := ⟨heq⟩ + have eq₁ : LIN (Inxpts h₁).front (Inxpts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (inx_pts_lieson_dlin h₁).1 (inx_pts_lieson_dlin h₁).2 + have h₂' : p LiesOn (LIN (Inxpts h₁).front (Inxpts h₁).back) := by rw [eq₁] exact h₂ - have eq₂ : perp_foot ω.center l = (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint := by - rw [← pts_lieson_circle_perpfoot_eq_midpoint (DirLC_inx_pts_lieson_circle h₁).1 (DirLC_inx_pts_lieson_circle h₁).2, eq₁] - have trieq₁ : (dist p (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 := by + have eq₂ : perp_foot ω.center l = (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint := by + rw [← pts_lieson_circle_perpfoot_eq_midpoint (inx_pts_lieson_circle h₁).1 (inx_pts_lieson_circle h₁).2, eq₁] + have trieq₁ : (dist p (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 := by rw [← eq₂, eq_sub_iff_add_eq, add_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] apply Pythagoras_of_perp_foot _ _ h₂ - have trieq₂ : (dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 = (dist ω.center (DirLC_inx_pts h₁).front) ^ 2 - (dist ω.center (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 := by + have trieq₂ : (dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 = (dist ω.center (Inxpts h₁).front) ^ 2 - (dist ω.center (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 := by rw [← eq₂, eq_sub_iff_add_eq, add_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] - apply Pythagoras_of_perp_foot _ _ (DirLC_inx_pts_lieson_dlin h₁).1 - have hgt : dist p (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint > dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint := by + apply Pythagoras_of_perp_foot _ _ (inx_pts_lieson_dlin h₁).1 + have hgt : dist p (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint > dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint := by calc - _ = |dist p (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] - _ > |dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint| := by + _ = |dist p (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] + _ > |dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint| := by apply sq_lt_sq.mp rw [trieq₁, trieq₂] simp apply sq_lt_sq.mpr - rw [abs_of_nonneg dist_nonneg, abs_of_nonneg dist_nonneg, (DirLC_inx_pts_lieson_circle h₁).1] + rw [abs_of_nonneg dist_nonneg, abs_of_nonneg dist_nonneg, (inx_pts_lieson_circle h₁).1] exact h₃ - _ = dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint := by rw [abs_of_nonneg dist_nonneg] + _ = dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint := by rw [abs_of_nonneg dist_nonneg] apply (not_lies_on_segnd_iff_lieson_ray h₂').mp apply (midpoint_dist_gt_iff_liesout h₂').mp hgt -theorem liesint_back_lieson_ray_front_reverse {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (DirLC_inx_pts h₁).back LiesOn (RAY p (DirLC_inx_pts h₁).front (liesint_ne_inxpts h₁ h₂ h₃).1.symm).reverse := by - haveI : PtNe p (DirLC_inx_pts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ +theorem liesint_back_lieson_ray_front_reverse {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front (liesint_ne_inxpts h₁ h₂ h₃).1.symm).reverse := by + haveI : PtNe p (Inxpts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ have hs : dist_pt_line ω.center l.toLine < ω.radius := by calc _ ≤ dist ω.center p := dist_pt_line_shortest _ _ h₂ _ < ω.radius := h₃ - haveI : PtNe (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back := ⟨by + haveI : PtNe (Inxpts h₁).front (Inxpts h₁).back := ⟨by contrapose! hs - rw [(DirLC_inx_pts_same_iff_tangent h₁).mp hs.symm]⟩ - have eq₁ : LIN (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (DirLC_inx_pts_lieson_dlin h₁).1 (DirLC_inx_pts_lieson_dlin h₁).2 - have h₂' : p LiesOn (LIN (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back) := by + rw [(inx_pts_same_iff_tangent h₁).mp hs.symm]⟩ + have eq₁ : LIN (Inxpts h₁).front (Inxpts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (inx_pts_lieson_dlin h₁).1 (inx_pts_lieson_dlin h₁).2 + have h₂' : p LiesOn (LIN (Inxpts h₁).front (Inxpts h₁).back) := by rw [eq₁] exact h₂ - have eq₂ : perp_foot ω.center l = (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint := by - rw [← pts_lieson_circle_perpfoot_eq_midpoint (DirLC_inx_pts_lieson_circle h₁).1 (DirLC_inx_pts_lieson_circle h₁).2, eq₁] - have trieq₁ : (dist p (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 := by + have eq₂ : perp_foot ω.center l = (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint := by + rw [← pts_lieson_circle_perpfoot_eq_midpoint (inx_pts_lieson_circle h₁).1 (inx_pts_lieson_circle h₁).2, eq₁] + have trieq₁ : (dist p (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 := by rw [← eq₂, eq_sub_iff_add_eq, add_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] apply Pythagoras_of_perp_foot _ _ h₂ - have trieq₂ : (dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 = (dist ω.center (DirLC_inx_pts h₁).front) ^ 2 - (dist ω.center (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint) ^ 2 := by + have trieq₂ : (dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 = (dist ω.center (Inxpts h₁).front) ^ 2 - (dist ω.center (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint) ^ 2 := by rw [← eq₂, eq_sub_iff_add_eq, add_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] - apply Pythagoras_of_perp_foot _ _ (DirLC_inx_pts_lieson_dlin h₁).1 - have hgt : dist p (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint < dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint := by + apply Pythagoras_of_perp_foot _ _ (inx_pts_lieson_dlin h₁).1 + have hgt : dist p (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint < dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint := by calc - _ = |dist p (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] - _ < |dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint| := by + _ = |dist p (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] + _ < |dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint| := by apply sq_lt_sq.mp rw [trieq₁, trieq₂] simp apply sq_lt_sq.mpr - rw [abs_of_nonneg dist_nonneg, abs_of_nonneg dist_nonneg, (DirLC_inx_pts_lieson_circle h₁).1] + rw [abs_of_nonneg dist_nonneg, abs_of_nonneg dist_nonneg, (inx_pts_lieson_circle h₁).1] exact h₃ - _ = dist (DirLC_inx_pts h₁).front (SEG (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back).midpoint := by rw [abs_of_nonneg dist_nonneg] + _ = dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint := by rw [abs_of_nonneg dist_nonneg] apply (liesint_segnd_iff_lieson_ray_reverse h₂').mp apply (midpoint_dist_lt_iff_liesint h₂').mp hgt @@ -266,99 +268,99 @@ section power namespace Circle -theorem circle_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) : ⟪VEC p (DirLC_inx_pts h₁).front, VEC p (DirLC_inx_pts h₁).back⟫_ℝ = power ω p := by - rcases DirLC_intersect_iff_tangent_or_secant.mp h₁ with h | h - · have heq : (DirLC_inx_pts h₁).back = (DirLC_inx_pts h₁).front := (DirLC_inx_pts_same_iff_tangent h₁).mpr h +theorem circle_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) : ⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ = power ω p := by + rcases intersect_iff_tangent_or_secant.mp h₁ with h | h + · have heq : (Inxpts h₁).back = (Inxpts h₁).front := (inx_pts_same_iff_tangent h₁).mpr h rw [heq, Vec.real_inner_apply _ _, ← Vec.norm_sq] calc - _ = (dist p (DirLC_Tangent_pt h)) ^ 2 := by + _ = (dist p (Tangentpt h)) ^ 2 := by rw [dist_comm, NormedAddTorsor.dist_eq_norm'] rfl _ = power ω p := tangent_length_sq_eq_power _ h₂ - haveI : PtNe (DirLC_inx_pts h₁).back (DirLC_inx_pts h₁).front := ⟨by + haveI : PtNe (Inxpts h₁).back (Inxpts h₁).front := ⟨by have h : dist_pt_line ω.center l.toLine < ω.radius := h contrapose! h - have : dist_pt_line ω.center l.toLine = ω.radius := (DirLC_inx_pts_same_iff_tangent h₁).mp h + have : dist_pt_line ω.center l.toLine = ω.radius := (inx_pts_same_iff_tangent h₁).mp h rw [this] ⟩ - have heq : - VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).front = VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).back := by + have heq : - VEC (perp_foot ω.center l) (Inxpts h₁).front = VEC (perp_foot ω.center l) (Inxpts h₁).back := by calc - _ = VEC (DirLC_inx_pts h₁).front (perp_foot ω.center l) := by rw [neg_vec] - _ = VEC (DirLC_inx_pts h₁).front (perp_foot ω.center (LIN (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back)) := by + _ = VEC (Inxpts h₁).front (perp_foot ω.center l) := by rw [neg_vec] + _ = VEC (Inxpts h₁).front (perp_foot ω.center (LIN (Inxpts h₁).front (Inxpts h₁).back)) := by congr; symm - apply Line.eq_line_of_pt_pt_of_ne (DirLC_inx_pts_lieson_dlin h₁).1 (DirLC_inx_pts_lieson_dlin h₁).2 - _ = VEC (perp_foot ω.center (LIN (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back)) (DirLC_inx_pts h₁).back := by - apply pts_lieson_circle_vec_eq (DirLC_inx_pts_lieson_circle h₁).1 (DirLC_inx_pts_lieson_circle h₁).2 - _ = VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).back := by + apply Line.eq_line_of_pt_pt_of_ne (inx_pts_lieson_dlin h₁).1 (inx_pts_lieson_dlin h₁).2 + _ = VEC (perp_foot ω.center (LIN (Inxpts h₁).front (Inxpts h₁).back)) (Inxpts h₁).back := by + apply pts_lieson_circle_vec_eq (inx_pts_lieson_circle h₁).1 (inx_pts_lieson_circle h₁).2 + _ = VEC (perp_foot ω.center l) (Inxpts h₁).back := by congr - apply Line.eq_line_of_pt_pt_of_ne (DirLC_inx_pts_lieson_dlin h₁).1 (DirLC_inx_pts_lieson_dlin h₁).2 + apply Line.eq_line_of_pt_pt_of_ne (inx_pts_lieson_dlin h₁).1 (inx_pts_lieson_dlin h₁).2 have eq₁ : (dist p (perp_foot ω.center l)) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2 := by rw [eq_sub_iff_add_eq, add_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] apply Pythagoras_of_perp_foot _ _ h₂ - have eq₂ : (dist (DirLC_inx_pts h₁).front (perp_foot ω.center l)) ^ 2 = (dist ω.center (DirLC_inx_pts h₁).front) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2 := by + have eq₂ : (dist (Inxpts h₁).front (perp_foot ω.center l)) ^ 2 = (dist ω.center (Inxpts h₁).front) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2 := by rw [eq_sub_iff_add_eq, add_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] - apply Pythagoras_of_perp_foot _ _ (DirLC_inx_pts_lieson_dlin h₁).1 + apply Pythagoras_of_perp_foot _ _ (inx_pts_lieson_dlin h₁).1 calc - _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).front, VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).back⟫_ℝ := by rw [vec_add_vec, vec_add_vec] - _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).front, VEC p (perp_foot ω.center l) - VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).front⟫_ℝ := by rw [← heq, sub_eq_add_neg] - _ = ‖VEC p (perp_foot ω.center l)‖ ^ 2 - ‖VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).front‖ ^ 2 := by + _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (Inxpts h₁).front, VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (Inxpts h₁).back⟫_ℝ := by rw [vec_add_vec, vec_add_vec] + _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (Inxpts h₁).front, VEC p (perp_foot ω.center l) - VEC (perp_foot ω.center l) (Inxpts h₁).front⟫_ℝ := by rw [← heq, sub_eq_add_neg] + _ = ‖VEC p (perp_foot ω.center l)‖ ^ 2 - ‖VEC (perp_foot ω.center l) (Inxpts h₁).front‖ ^ 2 := by rw [inner_add_left, inner_sub_right, inner_sub_right, Vec.norm_sq, Vec.norm_sq, ← Vec.real_inner_apply _ _, ← Vec.real_inner_apply _ _, add_comm, real_inner_comm] ring - _ = (dist p (perp_foot ω.center l)) ^ 2 - (dist (DirLC_inx_pts h₁).front (perp_foot ω.center l)) ^ 2 := by + _ = (dist p (perp_foot ω.center l)) ^ 2 - (dist (Inxpts h₁).front (perp_foot ω.center l)) ^ 2 := by rw [dist_comm, NormedAddTorsor.dist_eq_norm', NormedAddTorsor.dist_eq_norm'] rfl - _ = ((dist ω.center p) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2) - ((dist ω.center (DirLC_inx_pts h₁).front) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2) := by rw [eq₁, eq₂] - _ = (dist ω.center p) ^ 2 - (dist ω.center (DirLC_inx_pts h₁).front) ^ 2 := by ring - _ = (dist ω.center p) ^ 2 - ω.radius ^ 2 := by rw [(DirLC_inx_pts_lieson_circle h₁).1] + _ = ((dist ω.center p) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2) - ((dist ω.center (Inxpts h₁).front) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2) := by rw [eq₁, eq₂] + _ = (dist ω.center p) ^ 2 - (dist ω.center (Inxpts h₁).front) ^ 2 := by ring + _ = (dist ω.center p) ^ 2 - ω.radius ^ 2 := by rw [(inx_pts_lieson_circle h₁).1] _ = power ω p := rfl -theorem chord_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (dist p (DirLC_inx_pts h₁).front) * (dist p (DirLC_inx_pts h₁).back) = - power ω p := by - haveI hne : PtNe p (DirLC_inx_pts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ - have hl : (DirLC_inx_pts h₁).back LiesOn (RAY p (DirLC_inx_pts h₁).front).reverse := liesint_back_lieson_ray_front_reverse h₁ h₂ h₃ +theorem chord_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (dist p (Inxpts h₁).front) * (dist p (Inxpts h₁).back) = - power ω p := by + haveI hne : PtNe p (Inxpts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ + have hl : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front).reverse := liesint_back_lieson_ray_front_reverse h₁ h₂ h₃ rcases pt_lies_on_ray_rev_iff_vec_opposite_dir.mp hl with ⟨t, tnonpos, ht⟩ - have heq : dist p (DirLC_inx_pts h₁).back = -t := by + have heq : dist p (Inxpts h₁).back = -t := by calc - _ = ‖VEC p (DirLC_inx_pts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = ‖t • (RAY p (DirLC_inx_pts h₁).front).toDir.unitVec‖ := by rw [← ht]; rfl + _ = ‖VEC p (Inxpts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = ‖t • (RAY p (Inxpts h₁).front).toDir.unitVec‖ := by rw [← ht]; rfl _ = -t := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonpos tnonpos] - have ht' : VEC p (DirLC_inx_pts h₁).back = (t * (dist p (DirLC_inx_pts h₁).front)⁻¹) • (VEC p (DirLC_inx_pts h₁).front) := by + have ht' : VEC p (Inxpts h₁).back = (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front) := by calc - _ = t • (RAY p (DirLC_inx_pts h₁).front).toDir.unitVec := by rw [← ht]; rfl - _ = t • ((dist p (DirLC_inx_pts h₁).front)⁻¹ • (VEC p (DirLC_inx_pts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = (t * (dist p (DirLC_inx_pts h₁).front)⁻¹) • (VEC p (DirLC_inx_pts h₁).front) := by rw [smul_smul] + _ = t • (RAY p (Inxpts h₁).front).toDir.unitVec := by rw [← ht]; rfl + _ = t • ((dist p (Inxpts h₁).front)⁻¹ • (VEC p (Inxpts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front) := by rw [smul_smul] symm calc - _ = -⟪VEC p (DirLC_inx_pts h₁).front, VEC p (DirLC_inx_pts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] - _ = -⟪VEC p (DirLC_inx_pts h₁).front, (t * (dist p (DirLC_inx_pts h₁).front)⁻¹) • (VEC p (DirLC_inx_pts h₁).front)⟫_ℝ := by rw [ht'] - _ = -(t * (dist p (DirLC_inx_pts h₁).front)⁻¹) * ‖VEC p (DirLC_inx_pts h₁).front‖ ^ 2 := by + _ = -⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] + _ = -⟪VEC p (Inxpts h₁).front, (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front)⟫_ℝ := by rw [ht'] + _ = -(t * (dist p (Inxpts h₁).front)⁻¹) * ‖VEC p (Inxpts h₁).front‖ ^ 2 := by rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] simp - _ = (dist p (DirLC_inx_pts h₁).front) * (dist p (DirLC_inx_pts h₁).back) := by + _ = (dist p (Inxpts h₁).front) * (dist p (Inxpts h₁).back) := by unfold Vec.mkPtPt rw [← NormedAddTorsor.dist_eq_norm', dist_comm, heq, neg_mul, mul_assoc, mul_comm, pow_two, inv_mul_cancel_left₀] simp apply dist_ne_zero.mpr hne.out.symm -theorem secant_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (dist p (DirLC_inx_pts h₁).front) * (dist p (DirLC_inx_pts h₁).back) = power ω p := by - haveI hne : PtNe p (DirLC_inx_pts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ - have hl : (DirLC_inx_pts h₁).back LiesOn (RAY p (DirLC_inx_pts h₁).front) := liesout_back_lieson_ray_front h₁ h₂ h₃ +theorem secant_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (dist p (Inxpts h₁).front) * (dist p (Inxpts h₁).back) = power ω p := by + haveI hne : PtNe p (Inxpts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ + have hl : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front) := liesout_back_lieson_ray_front h₁ h₂ h₃ rcases Ray.lies_on_iff.mp hl with ⟨t, tnonneg, ht⟩ - have heq : dist p (DirLC_inx_pts h₁).back = t := by + have heq : dist p (Inxpts h₁).back = t := by calc - _ = ‖VEC p (DirLC_inx_pts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = ‖t • (RAY p (DirLC_inx_pts h₁).front).toDir.unitVec‖ := by rw [← ht]; rfl + _ = ‖VEC p (Inxpts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = ‖t • (RAY p (Inxpts h₁).front).toDir.unitVec‖ := by rw [← ht]; rfl _ = t := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonneg tnonneg] - have ht' : VEC p (DirLC_inx_pts h₁).back = (t * (dist p (DirLC_inx_pts h₁).front)⁻¹) • (VEC p (DirLC_inx_pts h₁).front) := by + have ht' : VEC p (Inxpts h₁).back = (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front) := by calc - _ = t • (RAY p (DirLC_inx_pts h₁).front).toDir.unitVec := by rw [← ht]; rfl - _ = t • ((dist p (DirLC_inx_pts h₁).front)⁻¹ • (VEC p (DirLC_inx_pts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = (t * (dist p (DirLC_inx_pts h₁).front)⁻¹) • (VEC p (DirLC_inx_pts h₁).front) := by rw [smul_smul] + _ = t • (RAY p (Inxpts h₁).front).toDir.unitVec := by rw [← ht]; rfl + _ = t • ((dist p (Inxpts h₁).front)⁻¹ • (VEC p (Inxpts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front) := by rw [smul_smul] symm calc - _ = ⟪VEC p (DirLC_inx_pts h₁).front, VEC p (DirLC_inx_pts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] - _ = ⟪VEC p (DirLC_inx_pts h₁).front, (t * (dist p (DirLC_inx_pts h₁).front)⁻¹) • (VEC p (DirLC_inx_pts h₁).front)⟫_ℝ := by rw [ht'] - _ = (t * (dist p (DirLC_inx_pts h₁).front)⁻¹) * ‖VEC p (DirLC_inx_pts h₁).front‖ ^ 2 := by rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] - _ = (dist p (DirLC_inx_pts h₁).front) * (dist p (DirLC_inx_pts h₁).back) := by + _ = ⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] + _ = ⟪VEC p (Inxpts h₁).front, (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front)⟫_ℝ := by rw [ht'] + _ = (t * (dist p (Inxpts h₁).front)⁻¹) * ‖VEC p (Inxpts h₁).front‖ ^ 2 := by rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] + _ = (dist p (Inxpts h₁).front) * (dist p (Inxpts h₁).back) := by unfold Vec.mkPtPt rw [← NormedAddTorsor.dist_eq_norm', dist_comm, heq, mul_assoc, mul_comm, pow_two, inv_mul_cancel_left₀] apply dist_ne_zero.mpr hne.out.symm diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index 9393c526..8b8a7ec8 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -24,16 +24,18 @@ scoped infix : 50 " Secant " => Circle.DirLine.IsSecant scoped infix : 50 " Tangent " => Circle.DirLine.IsTangent scoped infix : 50 " Disjoint " => Circle.DirLine.IsDisjoint -namespace Circle +open Circle + +namespace DirLC -theorem DirLC_disjoint_pt_liesout_circle {l : DirLine P} {ω : Circle P} {A : P} (h : l Disjoint ω) (hh : A LiesOn l.toLine) : A LiesOut ω := by +theorem disjoint_pt_liesout_circle {l : DirLine P} {ω : Circle P} {A : P} (h : l Disjoint ω) (hh : A LiesOn l.toLine) : A LiesOut ω := by show dist ω.center A > ω.radius calc _ ≥ dist_pt_line ω.center l.toLine := by apply dist_pt_line_shortest _ _ hh _ > ω.radius := h -theorem DirLC_intersect_iff_tangent_or_secant {l : DirLine P} {ω : Circle P} : (DirLine.IsIntersected l ω) ↔ (l Tangent ω) ∨ (l Secant ω) := by +theorem intersect_iff_tangent_or_secant {l : DirLine P} {ω : Circle P} : (DirLine.IsIntersected l ω) ↔ (l Tangent ω) ∨ (l Secant ω) := by constructor · intro h have : dist_pt_line ω.center l.toLine ≤ ω.radius := h @@ -51,14 +53,14 @@ theorem DirLC_intersect_iff_tangent_or_secant {l : DirLine P} {ω : Circle P} : have : dist_pt_line ω.center l.toLine < ω.radius := h linarith -end Circle +end DirLC @[ext] structure DirLCInxpts (P : Type _) [EuclideanPlane P] where front : P back : P -namespace Circle +namespace DirLC lemma dist_pt_line_ineq {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2 ≥ 0 := by have : dist_pt_line ω.center l.toLine ≤ ω.radius := h @@ -70,57 +72,57 @@ lemma dist_pt_line_ineq {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersect exact length_nonneg linarith -def DirLC_inx_pts {l : DirLine P} {ω : Circle P} (_h : DirLine.IsIntersected l ω) : DirLCInxpts P where +def Inxpts {l : DirLine P} {ω : Circle P} (_h : DirLine.IsIntersected l ω) : DirLCInxpts P where front := ((Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec) +ᵥ (perp_foot ω.center l.toLine) back := (- (Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec) +ᵥ (perp_foot ω.center l.toLine) -lemma DirLC_inx_pts_lieson_dlin {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((DirLC_inx_pts h).front LiesOn l) ∧ ((DirLC_inx_pts h).back LiesOn l) := by +lemma inx_pts_lieson_dlin {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((Inxpts h).front LiesOn l) ∧ ((Inxpts h).back LiesOn l) := by have hl : perp_foot ω.center l.toLine LiesOn l := by apply perp_foot_lies_on_line constructor - · have : (DirLC_inx_pts h).front LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl) := by + · have : (Inxpts h).front LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl) := by apply Ray.lies_on_iff.mpr use (Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) constructor apply Real.sqrt_nonneg - unfold DirLC_inx_pts Vec.mkPtPt + unfold Inxpts Vec.mkPtPt simp calc _ = ((Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec) +ᵥ (perp_foot ω.center l.toLine) -ᵥ (perp_foot ω.center l.toLine) := rfl _ = (Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec := by rw [vadd_vsub] - have : (DirLC_inx_pts h).front LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).toDirLine := by + have : (Inxpts h).front LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).toDirLine := by apply Ray.lies_on_toDirLine_iff_lies_on_or_lies_on_rev.mpr left; exact this rw [ray_of_pt_dirline_toDirLine_eq_dirline] at this exact this - have : (DirLC_inx_pts h).back LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).reverse := by + have : (Inxpts h).back LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).reverse := by apply Ray.lies_on_iff.mpr use (Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) constructor apply Real.sqrt_nonneg - unfold DirLC_inx_pts Vec.mkPtPt + unfold Inxpts Vec.mkPtPt simp calc _ = -((Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec) +ᵥ (perp_foot ω.center l.toLine) -ᵥ (perp_foot ω.center l.toLine) := rfl _ = -((Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec) := by rw [vadd_vsub] - have : (DirLC_inx_pts h).back LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).toDirLine := by + have : (Inxpts h).back LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).toDirLine := by apply Ray.lies_on_toDirLine_iff_lies_on_or_lies_on_rev.mpr right; exact this rw [ray_of_pt_dirline_toDirLine_eq_dirline] at this exact this -theorem DirLC_inx_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((DirLC_inx_pts h).front LiesOn ω) ∧ ((DirLC_inx_pts h).back LiesOn ω) := by +theorem inx_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((Inxpts h).front LiesOn ω) ∧ ((Inxpts h).back LiesOn ω) := by constructor - · have : (SEG ω.center (perp_foot ω.center l.toLine)).length ^ 2 + (SEG (DirLC_inx_pts h).front (perp_foot ω.center l.toLine)).length ^ 2 = (SEG ω.center (DirLC_inx_pts h).front).length ^ 2 := by apply Pythagoras_of_perp_foot _ _ (DirLC_inx_pts_lieson_dlin h).1 + · have : (SEG ω.center (perp_foot ω.center l.toLine)).length ^ 2 + (SEG (Inxpts h).front (perp_foot ω.center l.toLine)).length ^ 2 = (SEG ω.center (Inxpts h).front).length ^ 2 := by apply Pythagoras_of_perp_foot _ _ (inx_pts_lieson_dlin h).1 rw [← dist_pt_line] at this - show dist ω.center (DirLC_inx_pts h).front = ω.radius + show dist ω.center (Inxpts h).front = ω.radius apply (sq_eq_sq _ _).mp calc - _ = (dist_pt_line ω.center l.toLine) ^ 2 + (SEG (DirLC_inx_pts h).front (perp_foot ω.center l.toLine)).length ^ 2 := by rw [← Seg.length_eq_dist, ← this] - _ = (dist_pt_line ω.center l.toLine) ^ 2 + ‖VEC (DirLC_inx_pts h).front (perp_foot ω.center l.toLine)‖ ^ 2 := by + _ = (dist_pt_line ω.center l.toLine) ^ 2 + (SEG (Inxpts h).front (perp_foot ω.center l.toLine)).length ^ 2 := by rw [← Seg.length_eq_dist, ← this] + _ = (dist_pt_line ω.center l.toLine) ^ 2 + ‖VEC (Inxpts h).front (perp_foot ω.center l.toLine)‖ ^ 2 := by rw [Seg.length_eq_norm_toVec] simp only [seg_toVec_eq_vec] _ = (dist_pt_line ω.center l.toLine) ^ 2 + ‖(Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec‖ ^ 2 := by - unfold DirLC_inx_pts + unfold Inxpts simp only [vec_of_vadd_pt_pt_eq_neg_vec, norm_neg] _ = ω.radius ^ 2 := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonneg (Real.sqrt_nonneg _), Real.sq_sqrt] @@ -129,17 +131,17 @@ theorem DirLC_inx_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : DirLine apply dist_nonneg apply le_iff_lt_or_eq.mpr left; exact ω.rad_pos - have : (SEG ω.center (perp_foot ω.center l.toLine)).length ^ 2 + (SEG (DirLC_inx_pts h).back (perp_foot ω.center l.toLine)).length ^ 2 = (SEG ω.center (DirLC_inx_pts h).back).length ^ 2 := by apply Pythagoras_of_perp_foot _ _ (DirLC_inx_pts_lieson_dlin h).2 + have : (SEG ω.center (perp_foot ω.center l.toLine)).length ^ 2 + (SEG (Inxpts h).back (perp_foot ω.center l.toLine)).length ^ 2 = (SEG ω.center (Inxpts h).back).length ^ 2 := by apply Pythagoras_of_perp_foot _ _ (inx_pts_lieson_dlin h).2 rw [← dist_pt_line] at this - show dist ω.center (DirLC_inx_pts h).back = ω.radius + show dist ω.center (Inxpts h).back = ω.radius apply (sq_eq_sq _ _).mp calc - _ = (dist_pt_line ω.center l.toLine) ^ 2 + (SEG (DirLC_inx_pts h).back (perp_foot ω.center l.toLine)).length ^ 2 := by rw [← Seg.length_eq_dist, ← this] - _ = (dist_pt_line ω.center l.toLine) ^ 2 + ‖VEC (DirLC_inx_pts h).back (perp_foot ω.center l.toLine)‖ ^ 2 := by + _ = (dist_pt_line ω.center l.toLine) ^ 2 + (SEG (Inxpts h).back (perp_foot ω.center l.toLine)).length ^ 2 := by rw [← Seg.length_eq_dist, ← this] + _ = (dist_pt_line ω.center l.toLine) ^ 2 + ‖VEC (Inxpts h).back (perp_foot ω.center l.toLine)‖ ^ 2 := by rw [Seg.length_eq_norm_toVec] simp only [seg_toVec_eq_vec] _ = (dist_pt_line ω.center l.toLine) ^ 2 + ‖(Real.sqrt (ω.radius ^ 2 - (dist_pt_line ω.center l.toLine) ^ 2)) • l.toDir.unitVec‖ ^ 2 := by - unfold DirLC_inx_pts + unfold Inxpts simp only [neg_smul, vec_of_vadd_pt_pt_eq_neg_vec, neg_neg] _ = ω.radius ^ 2 := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonneg (Real.sqrt_nonneg _), Real.sq_sqrt] @@ -149,8 +151,8 @@ theorem DirLC_inx_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : DirLine apply le_iff_lt_or_eq.mpr left; exact ω.rad_pos -theorem DirLC_inx_pts_same_iff_tangent {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : (DirLC_inx_pts h).back = (DirLC_inx_pts h).front ↔ (l Tangent ω) := by - unfold DirLC_inx_pts +theorem inx_pts_same_iff_tangent {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : (Inxpts h).back = (Inxpts h).front ↔ (l Tangent ω) := by + unfold Inxpts simp apply Iff.trans (neg_eq_self ℝ _) apply Iff.trans smul_eq_zero @@ -175,12 +177,12 @@ theorem DirLC_inx_pts_same_iff_tangent {l : DirLine P} {ω : Circle P} (h : DirL left; rw [this, sub_self] simp -lemma DirLC_inx_pts_ne_center {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((DirLC_inx_pts h).front ≠ ω.center) ∧ ((DirLC_inx_pts h).back ≠ ω.center) := by +lemma inx_pts_ne_center {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((Inxpts h).front ≠ ω.center) ∧ ((Inxpts h).back ≠ ω.center) := by constructor - · apply (pt_lieson_ne_center (DirLC_inx_pts_lieson_circle h).1).out - apply (pt_lieson_ne_center (DirLC_inx_pts_lieson_circle h).2).out + · apply (pt_lieson_ne_center (inx_pts_lieson_circle h).1).out + apply (pt_lieson_ne_center (inx_pts_lieson_circle h).2).out -theorem DirLC_inxwith_iff_intersect {l : DirLine P} {ω : Circle P} : l InxWith ω ↔ DirLine.IsIntersected l ω := by +theorem inxwith_iff_intersect {l : DirLine P} {ω : Circle P} : l InxWith ω ↔ DirLine.IsIntersected l ω := by unfold intersect constructor · rintro ⟨A, ⟨h₁, h₂⟩⟩ @@ -189,26 +191,26 @@ theorem DirLC_inxwith_iff_intersect {l : DirLine P} {ω : Circle P} : l InxWith _ ≤ dist ω.center A := by apply dist_pt_line_shortest _ _ h₁ _ = ω.radius := h₂ intro h - use (DirLC_inx_pts h).front - exact ⟨(DirLC_inx_pts_lieson_dlin h).1, (DirLC_inx_pts_lieson_circle h).1⟩ + use (Inxpts h).front + exact ⟨(inx_pts_lieson_dlin h).1, (inx_pts_lieson_circle h).1⟩ -theorem DirLC_inxwith_iff_tangent_or_secant {l : DirLine P} {ω : Circle P} : l InxWith ω ↔ (l Tangent ω) ∨ (l Secant ω) := Iff.trans DirLC_inxwith_iff_intersect DirLC_intersect_iff_tangent_or_secant +theorem inxwith_iff_tangent_or_secant {l : DirLine P} {ω : Circle P} : l InxWith ω ↔ (l Tangent ω) ∨ (l Secant ω) := Iff.trans inxwith_iff_intersect intersect_iff_tangent_or_secant /- Tangent point -/ -def DirLC_Tangent_pt {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : P := (DirLC_inx_pts (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h))).front +def Tangentpt {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : P := (Inxpts (intersect_iff_tangent_or_secant.mpr (Or.inl h))).front -lemma DirLC_tangent_pt_ne_center {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : DirLC_Tangent_pt h ≠ ω.center := (DirLC_inx_pts_ne_center (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h))).1 +lemma tangent_pt_ne_center {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : Tangentpt h ≠ ω.center := (inx_pts_ne_center (intersect_iff_tangent_or_secant.mpr (Or.inl h))).1 -theorem DirLC_tangent_pt_center_perp_line {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : (LIN ω.center (DirLC_Tangent_pt h) (DirLC_tangent_pt_ne_center h)) ⟂ l.toLine := by +theorem tangent_pt_center_perp_line {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : (LIN ω.center (Tangentpt h) (tangent_pt_ne_center h)) ⟂ l.toLine := by have h : dist_pt_line ω.center l.toLine = ω.radius := h - have : DirLC_Tangent_pt h = perp_foot ω.center l.toLine := by - unfold DirLC_Tangent_pt DirLC_inx_pts + have : Tangentpt h = perp_foot ω.center l.toLine := by + unfold Tangentpt Inxpts simp apply (Real.sqrt_eq_zero _).mpr rw [h]; ring rw [h]; linarith - have : LIN ω.center (DirLC_Tangent_pt h) (DirLC_tangent_pt_ne_center h) = perp_line ω.center l.toLine := by + have : LIN ω.center (Tangentpt h) (tangent_pt_ne_center h) = perp_line ω.center l.toLine := by simp_rw [this] apply line_of_self_perp_foot_eq_perp_line_of_not_lies_on intro hn @@ -222,64 +224,68 @@ theorem DirLC_tangent_pt_center_perp_line {l : DirLine P} {ω : Circle P} (h : l unfold perp_line apply Line.proj_eq_of_mk_pt_proj -theorem DirLC_tangent_pt_eq_perp_foot {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : DirLC_Tangent_pt h = perp_foot ω.center l := by - haveI : PtNe (DirLC_Tangent_pt h) ω.center := ⟨DirLC_tangent_pt_ne_center h⟩ - have hp : (DLIN ω.center (DirLC_Tangent_pt h)) ⟂ l := by - show (DLIN ω.center (DirLC_Tangent_pt h)).toProj = l.toProj.perp +theorem tangent_pt_eq_perp_foot {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : Tangentpt h = perp_foot ω.center l := by + haveI : PtNe (Tangentpt h) ω.center := ⟨tangent_pt_ne_center h⟩ + have hp : (DLIN ω.center (Tangentpt h)) ⟂ l := by + show (DLIN ω.center (Tangentpt h)).toProj = l.toProj.perp calc - _ = (LIN ω.center (DirLC_Tangent_pt h)).toProj := rfl - _ = l.toLine.toProj.perp := DirLC_tangent_pt_center_perp_line h + _ = (LIN ω.center (Tangentpt h)).toProj := rfl + _ = l.toLine.toProj.perp := tangent_pt_center_perp_line h _ = l.toProj.perp := by rw [DirLine.toLine_toProj_eq_toProj] symm - exact perp_foot_unique (DirLC_inx_pts_lieson_dlin _).1 hp - + exact perp_foot_unique (inx_pts_lieson_dlin _).1 hp +end DirLC /- If we need, we can add some coercion to state that inx_pts with respect to "InxWith". -/ --- def DirLC_Inx_pts {l : DirLine P} {ω : Circle P} (h : l InxWith ω) : DirLCInxpts P where --- front := (DirLC_inx_pts (DirLC_inxwith_iff_intersect.mp h)).front --- back := (DirLC_inx_pts (DirLC_inxwith_iff_intersect.mp h)).back +-- def Inxpts {l : DirLine P} {ω : Circle P} (h : l InxWith ω) : DirLCInxpts P where +-- front := (Inxpts (DirLC_inxwith_iff_intersect.mp h)).front +-- back := (Inxpts (DirLC_inxwith_iff_intersect.mp h)).back --- theorem DirLC_inx_pts_lieson_dlin {l : DirLine P} {ω : Circle P} (h : l InxWith ω) : ((DirLC_Inx_pts h).front LiesOn l) ∧ ((DirLC_Inx_pts h).back LiesOn l) := by sorry +-- theorem Inxpts_lieson_dlin {l : DirLine P} {ω : Circle P} (h : l InxWith ω) : ((Inxpts h).front LiesOn l) ∧ ((Inxpts h).back LiesOn l) := by sorry --- theorem DirLC_inx_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : l InxWith ω) : ((DirLC_Inx_pts h).front LiesOn ω) ∧ ((DirLC_Inx_pts h).back LiesOn ω) := by sorry +-- theorem Inxpts_lieson_circle {l : DirLine P} {ω : Circle P} (h : l InxWith ω) : ((Inxpts h).front LiesOn ω) ∧ ((Inxpts h).back LiesOn ω) := by sorry /- DirLine and circle have at most two intersections. -/ /- inx pts' uniqueness -/ -theorem DirLC_intersection_eq_inxpts {l : DirLine P} {ω : Circle P} {A : P} (h : DirLine.IsIntersected l ω) (h₁ : A LiesOn l.toLine) (h₂ : A LiesOn ω) : (A = (DirLC_inx_pts h).front) ∨ (A = (DirLC_inx_pts h).back) := by - rcases (DirLC_intersect_iff_tangent_or_secant.mp h) with h' | h' +namespace Circle + +open DirLC + +theorem DirLC_intersection_eq_inxpts {l : DirLine P} {ω : Circle P} {A : P} (h : DirLine.IsIntersected l ω) (h₁ : A LiesOn l.toLine) (h₂ : A LiesOn ω) : (A = (Inxpts h).front) ∨ (A = (Inxpts h).back) := by + rcases (intersect_iff_tangent_or_secant.mp h) with h' | h' · left - show A = DirLC_Tangent_pt h' + show A = Tangentpt h' calc _ = perp_foot ω.center l := by apply eq_dist_eq_perp_foot h₁ rw [h₂, h'] - _ = DirLC_Tangent_pt h' := by rw [DirLC_tangent_pt_eq_perp_foot _] + _ = Tangentpt h' := by rw [tangent_pt_eq_perp_foot _] contrapose! h₂ intro h₃ - haveI hne₁ : PtNe A (DirLC_inx_pts h).front := ⟨h₂.1⟩ - haveI hne₂ : PtNe A (DirLC_inx_pts h).back := ⟨h₂.2⟩ - haveI hne₃ : PtNe (DirLC_inx_pts h).back (DirLC_inx_pts h).front := ⟨ by + haveI hne₁ : PtNe A (Inxpts h).front := ⟨h₂.1⟩ + haveI hne₂ : PtNe A (Inxpts h).back := ⟨h₂.2⟩ + haveI hne₃ : PtNe (Inxpts h).back (Inxpts h).front := ⟨ by intro eq - have h'' : l Tangent ω := (DirLC_inx_pts_same_iff_tangent h).mp eq + have h'' : l Tangent ω := (inx_pts_same_iff_tangent h).mp eq have : dist_pt_line ω.center l = ω.radius := h'' have : dist_pt_line ω.center l < ω.radius := h' linarith⟩ - have hc : colinear A (DirLC_inx_pts h).front (DirLC_inx_pts h).back := Line.linear h₁ (DirLC_inx_pts_lieson_dlin h).1 (DirLC_inx_pts_lieson_dlin h).2 - have hnc : ¬ (colinear A (DirLC_inx_pts h).front (DirLC_inx_pts h).back) := three_pts_lieson_circle_not_colinear h₃ (DirLC_inx_pts_lieson_circle h).1 (DirLC_inx_pts_lieson_circle h).2 + have hc : colinear A (Inxpts h).front (Inxpts h).back := Line.linear h₁ (inx_pts_lieson_dlin h).1 (inx_pts_lieson_dlin h).2 + have hnc : ¬ (colinear A (Inxpts h).front (Inxpts h).back) := three_pts_lieson_circle_not_colinear h₃ (inx_pts_lieson_circle h).1 (inx_pts_lieson_circle h).2 tauto -theorem pt_pt_tangent_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesOn ω) (ht : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) Tangent ω) : B = DirLC_Tangent_pt ht := by +theorem pt_pt_tangent_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesOn ω) (ht : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) Tangent ω) : B = Tangentpt ht := by haveI : PtNe A B := pt_liesout_ne_pt_lieson h₁ h₂ - rcases (DirLC_intersection_eq_inxpts (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl ht)) DirLine.snd_pt_lies_on_mk_pt_pt h₂) with heq | heq + rcases (DirLC_intersection_eq_inxpts (intersect_iff_tangent_or_secant.mpr (Or.inl ht)) DirLine.snd_pt_lies_on_mk_pt_pt h₂) with heq | heq exact heq - rw [(DirLC_inx_pts_same_iff_tangent _).mpr ht] at heq + rw [(inx_pts_same_iff_tangent _).mpr ht] at heq exact heq @@ -287,13 +293,13 @@ theorem pt_pt_tangent_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut theorem pt_pt_tangent_perp {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesOn ω) (ht : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) Tangent ω) : (DLIN ω.center B (pt_lieson_ne_center h₂).out) ⟂ (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) := by haveI : PtNe A B := pt_liesout_ne_pt_lieson h₁ h₂ haveI : PtNe B ω.center := pt_lieson_ne_center h₂ - haveI : PtNe (DirLC_Tangent_pt ht) ω.center := ⟨DirLC_tangent_pt_ne_center ht⟩ - have heq : B = DirLC_Tangent_pt ht := pt_pt_tangent_eq_tangent_pt h₁ h₂ ht + haveI : PtNe (Tangentpt ht) ω.center := ⟨tangent_pt_ne_center ht⟩ + have heq : B = Tangentpt ht := pt_pt_tangent_eq_tangent_pt h₁ h₂ ht show (DLIN ω.center B).toProj = (DLIN A B).toProj.perp calc - _ = (DLIN ω.center (DirLC_Tangent_pt ht)).toProj := by congr - _ = (LIN ω.center (DirLC_Tangent_pt ht)).toProj := rfl - _ = (DLIN A B).toLine.toProj.perp := DirLC_tangent_pt_center_perp_line _ + _ = (DLIN ω.center (Tangentpt ht)).toProj := by congr + _ = (LIN ω.center (Tangentpt ht)).toProj := rfl + _ = (DLIN A B).toLine.toProj.perp := tangent_pt_center_perp_line _ theorem pt_pt_perp_tangent {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesOn ω) (hp : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) ⟂ (DLIN ω.center B (pt_lieson_ne_center h₂).out)) : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) Tangent ω := by haveI : PtNe A B := pt_liesout_ne_pt_lieson h₁ h₂ @@ -306,12 +312,12 @@ theorem pt_pt_perp_tangent {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ _ = dist ω.center B := Seg.length_eq_dist _ = ω.radius := h₂ -theorem pt_pt_perp_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesOn ω) (hp : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) ⟂ (DLIN ω.center B (pt_lieson_ne_center h₂).out)) : B = DirLC_Tangent_pt (pt_pt_perp_tangent h₁ h₂ hp) := by +theorem pt_pt_perp_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesOn ω) (hp : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) ⟂ (DLIN ω.center B (pt_lieson_ne_center h₂).out)) : B = Tangentpt (pt_pt_perp_tangent h₁ h₂ hp) := by haveI : PtNe A B := pt_liesout_ne_pt_lieson h₁ h₂ haveI : PtNe B ω.center := pt_lieson_ne_center h₂ calc _ = perp_foot ω.center (DLIN A B) := by rw [perp_foot_unique DirLine.snd_pt_lies_on_mk_pt_pt hp.symm] - _ = DirLC_Tangent_pt (pt_pt_perp_tangent h₁ h₂ hp) := by rw [DirLC_tangent_pt_eq_perp_foot _] + _ = Tangentpt (pt_pt_perp_tangent h₁ h₂ hp) := by rw [tangent_pt_eq_perp_foot _] end Circle