From d0ffe3483a6174c1a34a19c52fb319bf3ed4be18 Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Sat, 23 Dec 2023 23:46:25 +0800 Subject: [PATCH 1/8] 12.23 fix [PtNe] CirclePower: finish the statement and proof of the general circle power thm --- .../Foundation/Axiom/Circle/Basic.lean | 15 +-- .../Foundation/Axiom/Circle/CCPosition.lean | 56 +++++---- .../Foundation/Axiom/Circle/CirclePower.lean | 112 ++++++++++++++---- .../Axiom/Circle/IncribedAngle.lean | 38 +++--- .../Foundation/Axiom/Circle/LCPosition.lean | 42 ++++--- .../Axiom/Linear/Perpendicular_trash.lean | 2 +- 6 files changed, 168 insertions(+), 97 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean index 5dd20fac..cd4b55e1 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean @@ -64,7 +64,7 @@ protected def IsOn (p : P) (ω : Circle P) : Prop := dist ω.center p = ω.radiu protected def IsInt (p : P) (ω : Circle P) : Prop := dist ω.center p < ω.radius -def IsOutside (p : P) (ω : Circle P) : Prop := ω.radius < dist ω.center p +protected def IsOutside (p : P) (ω : Circle P) : Prop := ω.radius < dist ω.center p protected def carrier (ω : Circle P) : Set P := { p : P | Circle.IsOn p ω } @@ -96,10 +96,8 @@ instance pt_liesout_ne_center {p : P} {ω : Circle P} (h : p LiesOut ω) : PtNe instance pt_lieson_ne_center {p : P} {ω : Circle P} (h : p LiesOn ω) : PtNe p ω.center := ⟨by apply dist_pos.mp - rw [dist_comm] - have : dist ω.center p = ω.radius := h - have : ω.radius > 0 := ω.rad_pos - linarith + rw [dist_comm, h] + exact ω.rad_pos ⟩ -- this instance does not work due to ω cannot be infered from A B, this should made in tactic ptne in the future @@ -159,8 +157,7 @@ lemma pts_lieson_circle_vec_eq {A B : P} {ω : Circle P} [hne : PtNe B A] (hl₁ rw [← Seg.length_eq_dist, ← Seg.length_eq_dist, ← Seg.length_eq_dist] apply Pythagoras_of_perp_foot apply Line.snd_pt_lies_on_mk_pt_pt - have : PtNe A (perp_foot ω.center (LIN A B)) - · apply Fact.mk + haveI : PtNe A (perp_foot ω.center (LIN A B)) := ⟨by intro heq have : (dist ω.center B) ^ 2 = ω.radius ^ 2 := by rw [hl₂] have : (dist ω.center B) ^ 2 > ω.radius ^ 2 := by @@ -170,7 +167,7 @@ lemma pts_lieson_circle_vec_eq {A B : P} {ω : Circle P} [hne : PtNe B A] (hl₁ _ = ω.radius ^ 2 + (dist B A) ^ 2 := by rw [hl₁] _ > ω.radius ^ 2 := by simp - linarith + linarith⟩ apply distinct_pts_same_dist_vec_eq · have : (perp_foot ω.center (LIN A B)) LiesOn (LIN A B) := perp_foot_lies_on_line _ _ have : colinear A B (perp_foot ω.center (LIN A B)) := Line.pt_pt_linear this @@ -204,6 +201,4 @@ end Circle end colinear --- ray with circle --- line with circle end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean index ee3696bb..176ee8f9 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean @@ -57,10 +57,11 @@ lemma CC_Circumscribe_centers_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h def CC_Circumscribe_Point {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Circumscribe ω₂) : P := (ω₁.radius • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec) +ᵥ ω₁.center theorem CC_circumscribe_point_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Circumscribe ω₂) : ((CC_Circumscribe_Point h) LiesOn ω₁) ∧ ((CC_Circumscribe_Point h) LiesOn ω₂) := by + haveI : PtNe ω₁.center ω₂.center := ⟨CC_Circumscribe_centers_distinct h⟩ constructor · have : dist ω₁.center (CC_Circumscribe_Point h) = ω₁.radius := by calc - _ = ‖ω₁.radius • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖ω₁.radius • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by unfold CC_Circumscribe_Point simp _ = ω₁.radius := by @@ -70,25 +71,26 @@ theorem CC_circumscribe_point_lieson_circles {ω₁ : Circle P} {ω₂ : Circle calc _ = ‖VEC (CC_Circumscribe_Point h) ω₂.center‖ := by rw [NormedAddTorsor.dist_eq_norm']; rfl _ = ‖VEC ω₁.center ω₂.center - VEC ω₁.center (CC_Circumscribe_Point h)‖ := by rw [vec_sub_vec] - _ = ‖VEC ω₁.center ω₂.center - ω₁.radius • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖VEC ω₁.center ω₂.center - ω₁.radius • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by unfold CC_Circumscribe_Point Vec.mkPtPt rw [vadd_vsub] - _ = ‖(VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).1 - ω₁.radius • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec‖ := rfl - _ = ‖(‖VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm‖ - ω₁.radius) • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖(VEC_nd ω₁.center ω₂.center).1 - ω₁.radius • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := rfl + _ = ‖(‖VEC_nd ω₁.center ω₂.center‖ - ω₁.radius) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by rw [sub_smul, VecND.norm_smul_toDir_unitVec] - _ = ‖(dist ω₁.center ω₂.center - ω₁.radius) • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖(dist ω₁.center ω₂.center - ω₁.radius) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm'] rfl - _ = ‖ω₂.radius • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖ω₂.radius • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by rw [h, add_comm, add_sub_cancel] _ = ω₂.radius := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonneg ω₂.rad_pos.le] exact this theorem CC_circumscribe_point_centers_colinear {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Circumscribe ω₂) : colinear ω₁.center (CC_Circumscribe_Point h) ω₂.center := by + haveI : PtNe ω₁.center ω₂.center := ⟨CC_Circumscribe_centers_distinct h⟩ have : VEC ω₁.center (CC_Circumscribe_Point h) = (ω₁.radius * ‖VEC ω₁.center ω₂.center‖⁻¹) • (VEC ω₁.center ω₂.center) := by calc - _ = ω₁.radius • (VEC_nd ω₁.center ω₂.center (CC_Circumscribe_centers_distinct h).symm).toDir.unitVec := by + _ = ω₁.radius • (VEC_nd ω₁.center ω₂.center).toDir.unitVec := by unfold CC_Circumscribe_Point simp _ = ω₁.radius • (‖VEC ω₁.center ω₂.center‖⁻¹ • (VEC ω₁.center ω₂.center)) := rfl @@ -107,16 +109,16 @@ theorem CC_inscribed_pt_inside_second_circle {ω₁ : Circle P} {ω₂ : Circle def CC_Inscribe_Point {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ InscribeIn ω₂) : P := (ω₁.radius • (VEC_nd ω₂.center ω₁.center h.2).toDir.unitVec) +ᵥ ω₁.center theorem CC_inscribe_point_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ InscribeIn ω₂) : ((CC_Inscribe_Point h) LiesOn ω₁) ∧ ((CC_Inscribe_Point h) LiesOn ω₂) := by + haveI : PtNe ω₁.center ω₂.center := ⟨h.2⟩ constructor · have : dist ω₁.center (CC_Inscribe_Point h) = ω₁.radius := by calc - _ = ‖ω₁.radius • (VEC_nd ω₂.center ω₁.center h.2).toDir.unitVec‖ := by + _ = ‖ω₁.radius • (VEC_nd ω₂.center ω₁.center).toDir.unitVec‖ := by unfold CC_Inscribe_Point simp _ = ω₁.radius := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonneg ω₁.rad_pos.le] exact this - haveI : PtNe ω₂.center ω₁.center := ⟨h.2.symm⟩ have : dist ω₂.center (CC_Inscribe_Point h) = ω₂.radius := by calc _ = ‖VEC (CC_Inscribe_Point h) ω₂.center‖ := by @@ -137,10 +139,9 @@ theorem CC_inscribe_point_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} ( _ = ‖(dist ω₁.center ω₂.center + ω₁.radius) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by congr rw [dist_comm] - -- apply Eq.trans _ (dist_comm _ _) -- note: why cannot rw? `fixed` apply Eq.trans _ (NormedAddTorsor.dist_eq_norm' _ _).symm -- `This should be a lemma in simp` rfl - _ = ‖ω₂.radius • (VEC_nd ω₁.center ω₂.center h.2.symm).toDir.unitVec‖ := by + _ = ‖ω₂.radius • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by congr; rw [h.1]; linarith _ = ω₂.radius := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonneg ω₂.rad_pos.le] -- note: 我不知道这行出现多少次了，不要复制粘贴，写点lemma @@ -148,19 +149,20 @@ theorem CC_inscribe_point_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} ( exact this theorem CC_inscribe_point_centers_colinear {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ InscribeIn ω₂) : colinear ω₁.center ω₂.center (CC_Inscribe_Point h) := by + haveI : PtNe ω₁.center ω₂.center := ⟨h.2⟩ have : VEC ω₁.center (CC_Inscribe_Point h) = (- ω₁.radius * ‖(VEC ω₁.center ω₂.center)‖⁻¹) • VEC ω₁.center ω₂.center := by calc - _ = ω₁.radius • (VEC_nd ω₂.center ω₁.center h.2).toDir.unitVec := by + _ = ω₁.radius • (VEC_nd ω₂.center ω₁.center).toDir.unitVec := by unfold CC_Inscribe_Point simp - _ = ω₁.radius • (- (VEC_nd ω₁.center ω₂.center h.2.symm).toDir.unitVec) := by + _ = ω₁.radius • (- (VEC_nd ω₁.center ω₂.center).toDir.unitVec) := by -- note: 为什么没有 neg_vecND - trans ω₁.radius • (-VEC_nd ω₁.center ω₂.center h.2.symm).toDir.unitVec + trans ω₁.radius • (-VEC_nd ω₁.center ω₂.center).toDir.unitVec · unfold VecND.mkPtPt Vec.mkPtPt congr rw [← neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev] · simp - _ = - ω₁.radius • (VEC_nd ω₁.center ω₂.center h.2.symm).toDir.unitVec := by + _ = - ω₁.radius • (VEC_nd ω₁.center ω₂.center).toDir.unitVec := by rw [smul_neg, neg_smul] _ = (- ω₁.radius) • ‖VEC ω₁.center ω₂.center‖⁻¹ • VEC ω₁.center ω₂.center := rfl _ = (- ω₁.radius * ‖VEC ω₁.center ω₂.center‖⁻¹) • VEC ω₁.center ω₂.center := by apply smul_smul @@ -260,23 +262,23 @@ theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Int exact Complex.I_ne_zero theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : ((CC_Intersected_pts h).left LiesOn ω₁) ∧ ((CC_Intersected_pts h).left LiesOn ω₂) ∧ ((CC_Intersected_pts h).right LiesOn ω₁) ∧ ((CC_Intersected_pts h).right LiesOn ω₂) := by - haveI : PtNe ω₁.center ω₂.center := ⟨ (CC_intersected_centers_distinct h) ⟩ + haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩ have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by apply sq_lt_sq.mpr rw [abs_of_pos ω₁.rad_pos] exact radical_axis_dist_lt_radius h - have heq : ω₂.center -ᵥ ω₁.center = (dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec := by + have heq : ω₂.center -ᵥ ω₁.center = (dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec := by calc _ = VEC ω₁.center ω₂.center := rfl - _ = ‖VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm‖ • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec := by simp only [VecND.norm_smul_toDir_unitVec, + _ = ‖VEC_nd ω₁.center ω₂.center‖ • (VEC_nd ω₁.center ω₂.center).toDir.unitVec := by simp only [VecND.norm_smul_toDir_unitVec, ne_eq, VecND.coe_mkPtPt] - _ = (dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec := by + _ = (dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec := by rw [dist_comm, NormedAddTorsor.dist_eq_norm'] rfl constructor · show dist ω₁.center (CC_Intersected_pts h).left = ω₁.radius calc - _ = ‖(Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖(Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by unfold CC_Intersected_pts simp _ = ‖Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)‖ := by @@ -289,11 +291,11 @@ theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω constructor · show dist ω₂.center (CC_Intersected_pts h).left = ω₂.radius calc - _ = ‖(dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec - (Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖(dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec - (Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by unfold CC_Intersected_pts simp rw [NormedAddTorsor.dist_eq_norm', vsub_vadd_eq_vsub_sub, heq] - _ = ‖(dist ω₁.center ω₂.center - (Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂))) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec‖ := by rw [sub_smul]; simp + _ = ‖(dist ω₁.center ω₂.center - (Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂))) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by rw [sub_smul]; simp _ = ‖dist ω₁.center ω₂.center - radical_axis_dist_to_the_first ω₁ ω₂ + (- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2)) * Complex.I‖ := by rw [norm_smul, Dir.norm_unitVec, mul_one] ring_nf @@ -309,7 +311,7 @@ theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω constructor · show dist ω₁.center (CC_Intersected_pts h).right = ω₁.radius calc - _ = ‖(- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖(- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by unfold CC_Intersected_pts simp _ = ‖- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)‖ := by @@ -321,11 +323,11 @@ theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω _ = ω₁.radius := Real.sqrt_sq (by linarith [ω₁.rad_pos]) show dist ω₂.center (CC_Intersected_pts h).right = ω₂.radius calc - _ = ‖(dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec - (- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec‖ := by + _ = ‖(dist ω₁.center ω₂.center) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec - (- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂)) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by unfold CC_Intersected_pts simp rw [NormedAddTorsor.dist_eq_norm', vsub_vadd_eq_vsub_sub, heq] - _ = ‖(dist ω₁.center ω₂.center - (- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂))) • (VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.unitVec‖ := by rw [sub_smul]; simp + _ = ‖(dist ω₁.center ω₂.center - (- Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2) * Complex.I + (radical_axis_dist_to_the_first ω₁ ω₂))) • (VEC_nd ω₁.center ω₂.center).toDir.unitVec‖ := by rw [sub_smul]; simp _ = ‖dist ω₁.center ω₂.center - radical_axis_dist_to_the_first ω₁ ω₂ + (Real.sqrt (ω₁.radius ^ 2 - (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2)) * Complex.I‖ := by rw [norm_smul, Dir.norm_unitVec, mul_one] ring_nf @@ -340,7 +342,9 @@ theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω apply mul_ne_zero (by norm_num) (dist_ne_zero.mpr (CC_intersected_centers_distinct h)) theorem CC_inx_pts_line_perp_center_line {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (LIN (CC_Intersected_pts h).left (CC_Intersected_pts h).right (CC_inx_pts_distinct h).symm) ⟂ (LIN ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm) := by - show (LIN (CC_Intersected_pts h).left (CC_Intersected_pts h).right (CC_inx_pts_distinct h).symm).toProj = (LIN ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toProj.perp + haveI : PtNe (CC_Intersected_pts h).left (CC_Intersected_pts h).right := ⟨CC_inx_pts_distinct h⟩ + haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩ + show (LIN (CC_Intersected_pts h).left (CC_Intersected_pts h).right).toProj = (LIN ω₁.center ω₂.center).toProj.perp sorry /- have hd : Complex.abs ((VEC_nd ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm).toDir.toVec) = 1 := by apply Dir.norm_of_dir_toVec_eq_one diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean index 08baf1a0..5ec9a1e3 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean @@ -112,34 +112,34 @@ lemma tangents_ne_center {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_tange lemma tangents_perp₁ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_tangent_circle_pts h).left (tangents_ne_pt h).1) ⟂ (DLIN ω.center (pt_tangent_circle_pts h).left (tangents_ne_center h).1) := by haveI : PtNe ω.center p := (Circle.pt_liesout_ne_center h).symm haveI : PtNe (pt_tangent_circle_pts h).left ω.center := ⟨(tangents_ne_center h).1⟩ - haveI : PtNe (pt_tangent_circle_pts h).left p:= ⟨ (tangents_ne_pt h).1 ⟩ - have heq₁ : ∠ p (pt_tangent_circle_pts h).left ω.center (tangents_ne_pt h).1.symm (tangents_ne_center h).1.symm = ∡[π / 2] := by sorry - -- apply inscribed_angle_of_diameter_eq_mod_pi_pt_pt_pt (mk_pt_pt_diam_fst_lieson (_h := (pt_liesout_ne_center h).symm)) - -- · exact (mk_pt_pt_diam_fst_lieson (_h := (pt_liesout_ne_center h).symm)) - -- · exact (CC_inx_pts_lieson_circles (tangent_circle_intersected h)).1 - -- · exact Arc.mk_pt_pt_diam_isantipode - show (DLIN p (pt_tangent_circle_pts h).left (tangents_ne_pt h).1).toProj = (DLIN ω.center (pt_tangent_circle_pts h).left (tangents_ne_center h).1).toProj.perp + haveI : PtNe (pt_tangent_circle_pts h).left p := ⟨(tangents_ne_pt h).1⟩ + have heq₁ : ∠ p (pt_tangent_circle_pts h).left ω.center = ∡[π / 2] := by + apply inscribed_angle_of_diameter_eq_mod_pi_pt_pt_pt + · exact (CC_inx_pts_lieson_circles (tangent_circle_intersected h)).1 + exact Arc.mk_pt_pt_diam_isantipode + show (DLIN p (pt_tangent_circle_pts h).left).toProj = (DLIN ω.center (pt_tangent_circle_pts h).left).toProj.perp calc - _ = (RAY p (pt_tangent_circle_pts h).left (tangents_ne_pt h).1).toProj := rfl - _ = (RAY (pt_tangent_circle_pts h).left p (tangents_ne_pt h).1.symm).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt - _ = (RAY (pt_tangent_circle_pts h).left ω.center (tangents_ne_center h).1.symm).toProj.perp := dvalue_eq_ang_rays_perp heq₁ - _ = (RAY ω.center (pt_tangent_circle_pts h).left (tangents_ne_center h).1).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] - _ = (DLIN ω.center (pt_tangent_circle_pts h).left (tangents_ne_center h).1).toProj.perp := rfl + _ = (RAY p (pt_tangent_circle_pts h).left).toProj := rfl + _ = (RAY (pt_tangent_circle_pts h).left p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt + _ = (RAY (pt_tangent_circle_pts h).left ω.center).toProj.perp := dvalue_eq_ang_rays_perp heq₁ + _ = (RAY ω.center (pt_tangent_circle_pts h).left).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] + _ = (DLIN ω.center (pt_tangent_circle_pts h).left).toProj.perp := rfl lemma tangents_perp₂ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_tangent_circle_pts h).right (tangents_ne_pt h).2) ⟂ (DLIN ω.center (pt_tangent_circle_pts h).right (tangents_ne_center h).2) := by - haveI : PtNe (pt_tangent_circle_pts h).right p :=⟨ (tangents_ne_pt h).2⟩ + haveI : PtNe ω.center p := (Circle.pt_liesout_ne_center h).symm + haveI : PtNe (pt_tangent_circle_pts h).right p := ⟨(tangents_ne_pt h).2⟩ haveI : PtNe ω.center (pt_tangent_circle_pts h).right := ⟨(tangents_ne_center h).2.symm⟩ - have heq₂ : ∠ p (pt_tangent_circle_pts h).right ω.center (tangents_ne_pt h).2.symm (tangents_ne_center h).2.symm = ∡[π / 2] := by sorry - -- apply inscribed_angle_of_diameter_eq_mod_pi_pt_pt_pt (Circle.pt_liesout_ne_center h) (tangents_ne_center h).2.symm (tangents_ne_pt h).2 (mk_pt_pt_diam_fst_lieson (pt_liesout_ne_center h).symm) - -- · exact (CC_inx_pts_lieson_circles (tangent_circle_intersected h)).2.2.1 - -- apply Arc.mk_pt_pt_diam_isantipode - show (DLIN p (pt_tangent_circle_pts h).right (tangents_ne_pt h).2).toProj = (DLIN ω.center (pt_tangent_circle_pts h).right (tangents_ne_center h).2).toProj.perp + have heq₂ : ∠ p (pt_tangent_circle_pts h).right ω.center = ∡[π / 2] := by + apply inscribed_angle_of_diameter_eq_mod_pi_pt_pt_pt + · exact (CC_inx_pts_lieson_circles (tangent_circle_intersected h)).2.2.1 + apply Arc.mk_pt_pt_diam_isantipode + show (DLIN p (pt_tangent_circle_pts h).right).toProj = (DLIN ω.center (pt_tangent_circle_pts h).right).toProj.perp calc - _ = (RAY p (pt_tangent_circle_pts h).right (tangents_ne_pt h).2).toProj := rfl - _ = (RAY (pt_tangent_circle_pts h).right p (tangents_ne_pt h).2.symm).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt - _ = (RAY (pt_tangent_circle_pts h).right ω.center (tangents_ne_center h).2.symm).toProj.perp := dvalue_eq_ang_rays_perp heq₂ - _ = (RAY ω.center (pt_tangent_circle_pts h).right (tangents_ne_center h).2).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] - _ = (DLIN ω.center (pt_tangent_circle_pts h).right (tangents_ne_center h).2).toProj.perp := rfl + _ = (RAY p (pt_tangent_circle_pts h).right).toProj := rfl + _ = (RAY (pt_tangent_circle_pts h).right p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt + _ = (RAY (pt_tangent_circle_pts h).right ω.center).toProj.perp := dvalue_eq_ang_rays_perp heq₂ + _ = (RAY ω.center (pt_tangent_circle_pts h).right).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] + _ = (DLIN ω.center (pt_tangent_circle_pts h).right).toProj.perp := rfl theorem line_tangent_circle {ω : Circle P} {p : P} (h : p LiesOut ω) : ((DLIN p (pt_tangent_circle_pts h).left (tangents_ne_pt h).1) Tangent ω) ∧ ((DLIN p (pt_tangent_circle_pts h).right (tangents_ne_pt h).2) Tangent ω) := by constructor @@ -153,7 +153,25 @@ theorem tangent_pts_eq_tangents {ω : Circle P} {p : P} (h : p LiesOut ω) : (Di symm apply pt_pt_perp_eq_tangent_pt h (tangents_lieson_circle h).2 (tangents_perp₂ h) -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 := sorry +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 + calc + _ = (dist p (perp_foot ω.center l)) ^ 2 := by rw [DirLC_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 - ω.radius ^ 2 := by + congr + exact (DirLC_intersected_pts_lieson_circle (DirLC_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 + apply (sq_eq_sq (by exact dist_nonneg) (by exact dist_nonneg)).mp + haveI : PtNe (pt_tangent_circle_pts h).left p := ⟨(tangents_ne_pt h).1⟩ + haveI : PtNe (pt_tangent_circle_pts h).right p := ⟨(tangents_ne_pt h).2⟩ + have hl₁ : p LiesOn (DLIN p (pt_tangent_circle_pts h).left) := DirLine.fst_pt_lies_on_mk_pt_pt + have hl₂ : p LiesOn (DLIN p (pt_tangent_circle_pts h).right) := DirLine.fst_pt_lies_on_mk_pt_pt + rw [← (tangent_pts_eq_tangents h).1, tangent_length_sq_eq_power _ hl₁, ← (tangent_pts_eq_tangents h).2, tangent_length_sq_eq_power _ hl₂] end Circle @@ -163,7 +181,51 @@ section power namespace Circle -theorem circle_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) : sorry := sorry +theorem circle_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) : ⟪VEC p (DirLC_Intersected_pts h₁).front, VEC p (DirLC_Intersected_pts h₁).back⟫_ℝ = power ω p := by + rcases DirLC_intersect_iff_tangent_or_secant.mp h₁ with h | h + · have heq : (DirLC_Intersected_pts h₁).back = (DirLC_Intersected_pts h₁).front := (DirLC_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 + rw [dist_comm, NormedAddTorsor.dist_eq_norm'] + rfl + _ = power ω p := tangent_length_sq_eq_power _ h₂ + haveI : PtNe (DirLC_Intersected_pts h₁).back (DirLC_Intersected_pts 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 + rw [this] + ⟩ + have heq : - VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front = VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).back := by + calc + _ = VEC (DirLC_Intersected_pts h₁).front (perp_foot ω.center l) := by rw [neg_vec] + _ = VEC (DirLC_Intersected_pts h₁).front (perp_foot ω.center (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back)) := by + congr; symm + apply Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_pts_lieson_dlin h₁).2 + _ = VEC (perp_foot ω.center (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back)) (DirLC_Intersected_pts h₁).back := by + apply pts_lieson_circle_vec_eq (DirLC_intersected_pts_lieson_circle h₁).1 (DirLC_intersected_pts_lieson_circle h₁).2 + _ = VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).back := by + congr + apply Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_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_Intersected_pts h₁).front (perp_foot ω.center l)) ^ 2 = (dist ω.center (DirLC_Intersected_pts 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_intersected_pts_lieson_dlin h₁).1 + calc + _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front, VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).back⟫_ℝ := by rw [vec_add_vec, vec_add_vec] + _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front, VEC p (perp_foot ω.center l) - VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front⟫_ℝ := by rw [← heq, sub_eq_add_neg] + _ = ‖VEC p (perp_foot ω.center l)‖ ^ 2 - ‖VEC (perp_foot ω.center l) (DirLC_Intersected_pts 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_Intersected_pts 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_Intersected_pts h₁).front) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2) := by rw [eq₁, eq₂] + _ = (dist ω.center p) ^ 2 - (dist ω.center (DirLC_Intersected_pts h₁).front) ^ 2 := by ring + _ = (dist ω.center p) ^ 2 - ω.radius ^ 2 := by rw [(DirLC_intersected_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_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) = - power ω p := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean index c0a8cf3d..62bb9795 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean @@ -90,7 +90,7 @@ lemma liesint_arc_not_lieson_dlin {β : Arc P} {p : P} (h : p LiesInt β) : ¬ ( intro hl have hl : p LiesOn (LIN β.source β.target) := hl have hco : colinear β.source β.target p := Line.pt_pt_linear hl - have hco' : ¬ (colinear β.source β.target p) := Circle.three_pts_lieson_circle_not_colinear (hne₂ := ⟨h.2.2⟩) (hne₃ := ⟨ h.2.1.symm ⟩ ) β.ison.1 β.ison.2 h.1.1 + have hco' : ¬ (colinear β.source β.target p) := Circle.three_pts_lieson_circle_not_colinear (hne₂ := ⟨h.2.2⟩) (hne₃ := ⟨h.2.1.symm⟩) β.ison.1 β.ison.2 h.1.1 tauto theorem liesint_arc_liesonright_dlin {β : Arc P} {p : P} (h : p LiesInt β) : p LiesOnRight (DLIN β.source β.target) := by @@ -183,7 +183,9 @@ theorem inscribed_angle_of_complementary_arc_is_negative {p : P} {β : Arc P} (h apply liesonright_angle_isneg (Arc.liesint_arc_liesonright_dlin h) theorem cangle_eq_two_times_inscribed_angle {p : P} {β : Arc P} (h₁ : p LiesOn β.circle) (h₂ : Arc.Isnot_arc_endpts p β) : β.cangle.value = 2 • (Arc.angle_mk_pt_arc p β h₂).value := by - haveI ne : p ≠ β.circle.center := (Circle.pt_lieson_ne_center h₁).out + haveI : PtNe p β.source := ⟨h₂.1⟩ + haveI : PtNe p β.target := ⟨h₂.2⟩ + haveI : PtNe p β.circle.center := Circle.pt_lieson_ne_center h₁ have hit₁ : (▵ β.circle.center β.target p).IsIsoceles := by unfold Triangle.IsIsoceles show (SEG p β.circle.center).length = (SEG β.circle.center β.target).length @@ -192,35 +194,35 @@ theorem cangle_eq_two_times_inscribed_angle {p : P} {β : Arc P} (h₁ : p LiesO unfold Triangle.IsIsoceles show (SEG β.source β.circle.center).length = (SEG β.circle.center p).length rw [Seg.length_eq_dist, Seg.length_eq_dist, dist_comm, h₁, β.ison.1] - have eq₁ : ∠ p β.target β.circle.center h₂.2 (Arc.center_isnot_arc_endpts β).2 = ∠ β.circle.center p β.target ne.symm h₂.2.symm := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₁ - have eq₂ : ∠ β.source p β.circle.center h₂.1.symm ne.symm = ∠ β.circle.center β.source p (Arc.center_isnot_arc_endpts β).1 h₂.1 := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₂ - have π₁ : ∠ β.target β.circle.center p (Arc.center_isnot_arc_endpts β).2.symm ne + ∠ p β.target β.circle.center h₂.2 (Arc.center_isnot_arc_endpts β).2 + ∠ β.circle.center p β.target ne.symm h₂.2.symm = π := by apply angle_sum_eq_pi_of_tri (▵ β.circle.center β.target p) - have π₂ : ∠ p β.circle.center β.source ne (Arc.center_isnot_arc_endpts β).1.symm + ∠ β.source p β.circle.center h₂.1.symm ne.symm + ∠ β.circle.center β.source p (Arc.center_isnot_arc_endpts β).1 h₂.1 = π := by apply angle_sum_eq_pi_of_tri (▵ β.circle.center p β.source) - have hsum₁ : ∠ β.target β.circle.center p (Arc.center_isnot_arc_endpts β).2.symm ne + ∠ p β.circle.center β.source ne (Arc.center_isnot_arc_endpts β).1.symm = ∠ β.target β.circle.center β.source (Arc.center_isnot_arc_endpts β).2.symm (Arc.center_isnot_arc_endpts β).1.symm := by - have : (ANG β.target β.circle.center p (Arc.center_isnot_arc_endpts β).2.symm ne).end_ray = (ANG p β.circle.center β.source ne (Arc.center_isnot_arc_endpts β).1.symm).start_ray := rfl - have hhs : (Angle.sum_adj this).value = ∠ β.target β.circle.center β.source (Arc.center_isnot_arc_endpts β).2.symm (Arc.center_isnot_arc_endpts β).1.symm := rfl + have eq₁ : ∠ p β.target β.circle.center = ∠ β.circle.center p β.target := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₁ + have eq₂ : ∠ β.source p β.circle.center = ∠ β.circle.center β.source p := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₂ + have π₁ : ∠ β.target β.circle.center p + ∠ p β.target β.circle.center + ∠ β.circle.center p β.target = π := by apply angle_sum_eq_pi_of_tri (▵ β.circle.center β.target p) + have π₂ : ∠ p β.circle.center β.source + ∠ β.source p β.circle.center + ∠ β.circle.center β.source p = π := by apply angle_sum_eq_pi_of_tri (▵ β.circle.center p β.source) + have hsum₁ : ∠ β.target β.circle.center p + ∠ p β.circle.center β.source = ∠ β.target β.circle.center β.source := by + have : (ANG β.target β.circle.center p).end_ray = (ANG p β.circle.center β.source).start_ray := rfl + have hhs : (Angle.sum_adj this).value = ∠ β.target β.circle.center β.source := rfl rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang] rfl - have hsum₂ : ∠ β.source p β.circle.center h₂.1.symm ne.symm + ∠ β.circle.center p β.target ne.symm h₂.2.symm = ∠ β.source p β.target h₂.1.symm h₂.2.symm := by - have : (ANG β.source p β.circle.center h₂.1.symm ne.symm).end_ray = (ANG β.circle.center p β.target ne.symm h₂.2.symm).start_ray := rfl - have hhs : (Angle.sum_adj this).value = ∠ β.source p β.target h₂.1.symm h₂.2.symm := rfl + have hsum₂ : ∠ β.source p β.circle.center + ∠ β.circle.center p β.target = ∠ β.source p β.target := by + have : (ANG β.source p β.circle.center).end_ray = (ANG β.circle.center p β.target).start_ray := rfl + have hhs : (Angle.sum_adj this).value = ∠ β.source p β.target := rfl rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang] rfl - have eq₃ : ∠ β.target β.circle.center β.source (Arc.center_isnot_arc_endpts β).2.symm (Arc.center_isnot_arc_endpts β).1.symm + 2 • (∠ β.source p β.target h₂.1.symm h₂.2.symm) = 0 := by + have eq₃ : ∠ β.target β.circle.center β.source + 2 • (∠ β.source p β.target) = 0 := by calc - _ = ∠ β.target β.circle.center p (Arc.center_isnot_arc_endpts β).2.symm ne + ∠ p β.circle.center β.source ne (Arc.center_isnot_arc_endpts β).1.symm + 2 • (∠ β.source p β.circle.center h₂.1.symm ne.symm + ∠ β.circle.center p β.target ne.symm h₂.2.symm) := by rw [hsum₁, hsum₂] - _ = ∠ β.target β.circle.center p (Arc.center_isnot_arc_endpts β).2.symm ne + ∠ p β.circle.center β.source ne (Arc.center_isnot_arc_endpts β).1.symm + (∠ p β.target β.circle.center h₂.2 (Arc.center_isnot_arc_endpts β).2 + ∠ β.circle.center p β.target ne.symm h₂.2.symm) + (∠ β.source p β.circle.center h₂.1.symm ne.symm + ∠ β.circle.center β.source p (Arc.center_isnot_arc_endpts β).1 h₂.1) := by + _ = ∠ β.target β.circle.center p + ∠ p β.circle.center β.source + 2 • (∠ β.source p β.circle.center + ∠ β.circle.center p β.target) := by rw [hsum₁, hsum₂] + _ = ∠ β.target β.circle.center p + ∠ p β.circle.center β.source + (∠ p β.target β.circle.center + ∠ β.circle.center p β.target) + (∠ β.source p β.circle.center + ∠ β.circle.center β.source p) := by rw [← eq₂, eq₁, two_smul] abel - _ = (∠ β.target β.circle.center p (Arc.center_isnot_arc_endpts β).2.symm ne + ∠ p β.target β.circle.center h₂.2 (Arc.center_isnot_arc_endpts β).2 + ∠ β.circle.center p β.target ne.symm h₂.2.symm) + (∠ p β.circle.center β.source ne (Arc.center_isnot_arc_endpts β).1.symm + ∠ β.source p β.circle.center h₂.1.symm ne.symm + ∠ β.circle.center β.source p (Arc.center_isnot_arc_endpts β).1 h₂.1) := by + _ = (∠ β.target β.circle.center p + ∠ p β.target β.circle.center + ∠ β.circle.center p β.target) + (∠ p β.circle.center β.source + ∠ β.source p β.circle.center + ∠ β.circle.center β.source p) := by rw [add_assoc, add_add_add_comm] abel _ = 0 := by rw [π₁, π₂, ← coe_two_pi, two_mul] simp calc - _ = - ∠ β.target β.circle.center β.source (Arc.center_isnot_arc_endpts β).2.symm (Arc.center_isnot_arc_endpts β).1.symm := by rw [← neg_value_of_rev_ang]; rfl - _ = 2 • (∠ β.source p β.target h₂.1.symm h₂.2.symm) := by rw [← zero_sub, ← eq₃, add_sub_cancel'] + _ = - ∠ β.target β.circle.center β.source := by rw [← neg_value_of_rev_ang]; rfl + _ = 2 • (∠ β.source p β.target) := by rw [← zero_sub, ← eq₃, add_sub_cancel'] _ = 2 • (Arc.angle_mk_pt_arc p β h₂).value := rfl theorem inscribed_angle_of_diameter_eq_mod_pi {p : P} {β : Arc P} (h₁ : p LiesOn β.circle) (h₂ : Arc.IsAntipode β.source β.target β.ison.1 β.ison.2) (h₃ : Arc.Isnot_arc_endpts p β) : (Arc.angle_mk_pt_arc p β h₃).dvalue = ∡[π / 2] := by diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index 92225ece..c083a1e8 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -69,14 +69,12 @@ lemma dist_pt_line_ineq {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersect apply norm_nonneg linarith -def DirLC_Intersected_pts {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : DirLCInxpts P where +def DirLC_Intersected_pts {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_intersected_pts_lieson_dlin {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((DirLC_Intersected_pts h).front LiesOn l) ∧ ((DirLC_Intersected_pts h).back LiesOn l) := by - have hl : perp_foot ω.center l.toLine LiesOn l := by - show perp_foot ω.center l.toLine LiesOn l.toLine - apply perp_foot_lies_on_line + have hl : perp_foot ω.center l.toLine LiesOn l := by apply perp_foot_lies_on_line constructor · have : (DirLC_Intersected_pts h).front LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl) := by apply Ray.lies_on_iff.mpr @@ -207,14 +205,16 @@ theorem DirLC_tangent_pt_center_perp_line {l : DirLine P} {ω : Circle P} (h : l 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 - have hp : (DLIN ω.center (DirLC_Tangent_pt h) (DirLC_tangent_pt_ne_center h)) ⟂ l := by - show (DLIN ω.center (DirLC_Tangent_pt h) (DirLC_tangent_pt_ne_center h)).toProj = l.toProj.perp + 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 calc - _ = (LIN ω.center (DirLC_Tangent_pt h) (DirLC_tangent_pt_ne_center h)).toProj := rfl + _ = (LIN ω.center (DirLC_Tangent_pt h)).toProj := rfl _ = l.toLine.toProj.perp := DirLC_tangent_pt_center_perp_line h _ = l.toProj.perp := by rw [DirLine.toLine_toProj_eq_toProj] symm - apply perp_foot_unique (DirLC_intersected_pts_lieson_dlin _).1 (DirLC_tangent_pt_ne_center h).symm hp + apply perp_foot_unique _ hp + exact (DirLC_intersected_pts_lieson_dlin _).1 @@ -274,31 +274,39 @@ theorem DirLC_intersection_eq_inxpts {l : DirLine P} {ω : Circle P} {A : P} (h 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 - rcases (DirLC_intersection_eq_inxpts (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl ht)) (DirLine.snd_pt_lies_on_mk_pt_pt (_h := (pt_liesout_ne_pt_lieson h₁ h₂).symm)) h₂) with heq | heq + 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 exact heq rw [(DirLC_inx_pts_same_iff_tangent _).mpr ht] at heq exact heq 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 - show (DLIN ω.center B (pt_lieson_ne_center h₂).out).toProj = (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm).toProj.perp + show (DLIN ω.center B).toProj = (DLIN A B).toProj.perp calc - _ = (DLIN ω.center (DirLC_Tangent_pt ht) (DirLC_tangent_pt_ne_center ht)).toProj := by congr - _ = (LIN ω.center (DirLC_Tangent_pt ht) (DirLC_tangent_pt_ne_center ht)).toProj := rfl - _ = (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm).toLine.toProj.perp := DirLC_tangent_pt_center_perp_line _ + _ = (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 _ 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 - have heq : perp_foot ω.center (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) = B := perp_foot_unique (DirLine.snd_pt_lies_on_mk_pt_pt (_h := ⟨ (pt_liesout_ne_pt_lieson h₁ h₂).out.symm ⟩ )) (pt_lieson_ne_center h₂).out.symm hp.symm - show dist_pt_line ω.center (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) = ω.radius + haveI : PtNe A B := pt_liesout_ne_pt_lieson h₁ h₂ + haveI : PtNe B ω.center := pt_lieson_ne_center h₂ + have heq : perp_foot ω.center (DLIN A B) = B := perp_foot_unique DirLine.snd_pt_lies_on_mk_pt_pt hp.symm + show dist_pt_line ω.center (DLIN A B) = ω.radius calc - _ = (SEG ω.center (perp_foot ω.center (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm))).length := rfl + _ = (SEG ω.center (perp_foot ω.center (DLIN A B))).length := rfl _ = (SEG ω.center B).length := by rw [heq] _ = 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 + 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 (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) := by rw [perp_foot_unique (DirLine.snd_pt_lies_on_mk_pt_pt (_h := ⟨(pt_liesout_ne_pt_lieson h₁ h₂).out.symm⟩)) (pt_lieson_ne_center h₂).out.symm hp.symm] + _ = 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 _] end Circle diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean index 42bd9e8a..91448872 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean @@ -7,7 +7,7 @@ open Line variable {P : Type _} [EuclideanPlane P] -theorem perp_foot_unique {A B : P} {l : DirLine P} (h : A LiesOn l) (hne : B ≠ A) (hp : (DLIN B A hne.symm) ⟂ l) : perp_foot B l = A := sorry +theorem perp_foot_unique {A B : P} {l : DirLine P} (h : A LiesOn l) [_hne : PtNe A B] (hp : (DLIN B A) ⟂ l) : perp_foot B l = A := sorry theorem eq_dist_eq_perp_foot {A B : P} {l : DirLine P} (h : A LiesOn l) (heq : dist B A = dist_pt_line B l) : A = perp_foot B l := sorry From f7c6ef48e72003cf48c815b596a64bcb2d5f49c3 Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Sun, 24 Dec 2023 16:33:07 +0800 Subject: [PATCH 2/8] 12.24 finish the proof of spacific circle power thm; finish the uniqueness of CC inx pts. --- .../Foundation/Axiom/Circle/Basic.lean | 19 +++ .../Foundation/Axiom/Circle/CCPosition.lean | 49 ++++++- .../Foundation/Axiom/Circle/CirclePower.lean | 138 +++++++++++++++++- .../Foundation/Axiom/Linear/Line_trash.lean | 53 ++++++- .../Axiom/Triangle/Congruence_trash.lean | 1 + 5 files changed, 251 insertions(+), 9 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean index 85edbe9e..43a436ec 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean @@ -108,6 +108,13 @@ instance pt_liesout_ne_pt_lieson {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) rw [hgt, heq] ⟩ +instance pt_liesint_ne_pt_lieson {A B : P} {ω : Circle P} (h₁ : A LiesInt ω) (h₂ : B LiesOn ω) : PtNe A B := ⟨by + have hgt : dist ω.center A < ω.radius := h₁ + have heq : dist ω.center B = ω.radius := h₂ + contrapose! hgt + rw [hgt, heq] + ⟩ + theorem interior_of_circle_iff_inside_not_on_circle (p : P) (ω : Circle P) : p LiesInt ω ↔ (p LiesIn ω) ∧ (¬ p LiesOn ω) := by show dist ω.center p < ω.radius ↔ (dist ω.center p ≤ ω.radius) ∧ (¬ dist ω.center p = ω.radius) push_neg @@ -181,6 +188,18 @@ lemma pts_lieson_circle_vec_eq {A B : P} {ω : Circle P} [hne : PtNe B A] (hl₁ _ = (dist A (perp_foot ω.center (LIN A B))) ^ 2 := by rw [← htri₁]; ring _ = (dist (perp_foot ω.center (LIN A B)) A) ^ 2 := by rw [dist_comm] +theorem pts_lieson_circle_perpfoot_eq_midpoint {A B : P} {ω : Circle P} [hne : PtNe B A] (hl₁ : A LiesOn ω) (hl₂ : B LiesOn ω) : perp_foot ω.center (LIN A B) = (SEG A B).midpoint := by + have eq₁ : VEC A (perp_foot ω.center (LIN A B)) = (1 / 2 : ℝ) • (VEC A B) := by + symm + calc + _ = (1 / 2 : ℝ) • (VEC A (perp_foot ω.center (LIN A B)) + VEC (perp_foot ω.center (LIN A B)) B) := by rw [vec_add_vec] + _ = (1 / 2 : ℝ) • ((2 : ℝ) • VEC A (perp_foot ω.center (LIN A B))) := by rw [← (pts_lieson_circle_vec_eq hl₁ hl₂), two_smul] + _ = VEC A (perp_foot ω.center (LIN A B)) := by simp + have eq₂ : VEC A (SEG A B).midpoint = (1 / 2 : ℝ) • (VEC A B) := Seg.vec_source_midpt + apply (eq_iff_vec_eq_zero _ _).mpr + calc + _ = VEC A (perp_foot ω.center (LIN A B)) - VEC A (SEG A B).midpoint := by rw [vec_sub_vec] + _ = 0 := by rw [eq₁, eq₂]; simp theorem three_pts_lieson_circle_not_colinear {A B C : P} {ω : Circle P} [hne₁ : PtNe B A] [hne₂ : PtNe C B] [hne₃ : PtNe A C] (hl₁ : A LiesOn ω) (hl₂ : B LiesOn ω) (hl₃ : C LiesOn ω) : ¬ (colinear A B C) := by intro h diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean index 176ee8f9..f452793a 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean @@ -1,4 +1,5 @@ import EuclideanGeometry.Foundation.Axiom.Circle.Basic +import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence_trash noncomputable section namespace EuclidGeom @@ -341,6 +342,31 @@ theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω apply Real.sqrt_sq (by linarith [ω₂.rad_pos]) apply mul_ne_zero (by norm_num) (dist_ne_zero.mpr (CC_intersected_centers_distinct h)) +lemma CC_inx_pts_not_colinear {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (¬ colinear (CC_Intersected_pts h).left ω₁.center ω₂.center) ∧ (¬ colinear (CC_Intersected_pts h).right ω₁.center ω₂.center) := by + constructor + · intro hc + -- Triangle.edge_sum_eq_edge_iff_colinear + sorry + sorry + +theorem CC_inx_pts_tri_acongr {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left) ≅ₐ (▵ ω₁.center ω₂.center (CC_Intersected_pts h).right) := by + haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩ + have he₁ : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left).edge₁.length = (▵ ω₁.center ω₂.center (CC_Intersected_pts h).right).edge₁.length := by + show (SEG ω₂.center (CC_Intersected_pts h).left).length = (SEG ω₂.center (CC_Intersected_pts h).right).length + simp + rw [(CC_inx_pts_lieson_circles h).2.1, (CC_inx_pts_lieson_circles h).2.2.2] + have he₂ : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left).edge₂.length = (▵ ω₁.center ω₂.center (CC_Intersected_pts h).right).edge₂.length := by + show (SEG (CC_Intersected_pts h).left ω₁.center).length = (SEG (CC_Intersected_pts h).right ω₁.center).length + simp + rw [dist_comm, (CC_inx_pts_lieson_circles h).1, dist_comm, (CC_inx_pts_lieson_circles h).2.2.1] + have he₃ : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left).edge₃.length = (▵ ω₁.center ω₂.center (CC_Intersected_pts h).right).edge₃.length := rfl + rcases Triangle.congr_or_acongr_of_SSS he₁ he₂ he₃ with hc | hac + · exfalso + have heq : (CC_Intersected_pts h).left = (CC_Intersected_pts h).right := by + apply Triangle.IsCongr.unique_of_eq_eq hc (by rfl) (by rfl) + apply CC_inx_pts_distinct h heq + exact hac + theorem CC_inx_pts_line_perp_center_line {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (LIN (CC_Intersected_pts h).left (CC_Intersected_pts h).right (CC_inx_pts_distinct h).symm) ⟂ (LIN ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm) := by haveI : PtNe (CC_Intersected_pts h).left (CC_Intersected_pts h).right := ⟨CC_inx_pts_distinct h⟩ haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩ @@ -384,11 +410,24 @@ theorem CC_inx_pts_line_perp_center_line {ω₁ : Circle P} {ω₂ : Circle P} ( /- different circles have at most two intersections -/ -lemma CC_inx_pt_not_lieson_center_line {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h : ω₁ Intersect ω₂) (h₁ : A LiesOn ω₁) (h₂ : A LiesOn ω₂) : ¬(A LiesOn (LIN ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm)) := sorry - -theorem CC_inx_pt_liesonleft_center_ray_eq_leftinxpt {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h : ω₁ Intersect ω₂) (h₁ : A LiesOn ω₁) (h₂ : A LiesOn ω₂) (h₃ : A LiesOnLeft (RAY ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm)) : A = (CC_Intersected_pts h).left := sorry - -theorem CC_inx_pt_liesonright_center_ray_eq_rightinxpt {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h : ω₁ Intersect ω₂) (h₁ : A LiesOn ω₁) (h₂ : A LiesOn ω₂) (h₃ : A LiesOnRight (RAY ω₁.center ω₂.center (CC_intersected_centers_distinct h).symm)) : A = (CC_Intersected_pts h).right := sorry +theorem CC_inx_pts_uniqueness {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h : ω₁ Intersect ω₂) (h₁ : A LiesOn ω₁) (h₂ : A LiesOn ω₂) : (A = (CC_Intersected_pts h).left) ∨ (A = (CC_Intersected_pts h).right) := by + haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩ + have hac : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left) ≅ₐ (▵ ω₁.center ω₂.center (CC_Intersected_pts h).right) := CC_inx_pts_tri_acongr h + have he₁ : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left).edge₁.length = (▵ ω₁.center ω₂.center A).edge₁.length := by + show (SEG ω₂.center (CC_Intersected_pts h).left).length = (SEG ω₂.center A).length + simp + rw [(CC_inx_pts_lieson_circles h).2.1, h₂] + have he₂ : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left).edge₂.length = (▵ ω₁.center ω₂.center A).edge₂.length := by + show (SEG (CC_Intersected_pts h).left ω₁.center).length = (SEG A ω₁.center).length + simp + rw [dist_comm, (CC_inx_pts_lieson_circles h).1, dist_comm, h₁] + have he₃ : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left).edge₃.length = (▵ ω₁.center ω₂.center A).edge₃.length := rfl + rcases Triangle.congr_or_acongr_of_SSS he₁ he₂ he₃ with hc | hc + · left; symm + apply Triangle.IsCongr.unique_of_eq_eq hc (by rfl) (by rfl) + right + have : (▵ ω₁.center ω₂.center A) ≅ (▵ ω₁.center ω₂.center (CC_Intersected_pts h).right) := Triangle.congr_of_acongr_acongr hc.symm hac + apply Triangle.IsCongr.unique_of_eq_eq this (by rfl) (by rfl) end Circle diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean index 5ec9a1e3..adcfc4f2 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean @@ -177,6 +177,91 @@ end Circle end tangent +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_Intersected_pts h₁).front) ∧ (p ≠ (DirLC_Intersected_pts h₁).back) := by + constructor + · apply (pt_liesout_ne_pt_lieson h₃ (DirLC_intersected_pts_lieson_circle h₁).1).out + apply (pt_liesout_ne_pt_lieson h₃ (DirLC_intersected_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_Intersected_pts h₁).front) ∧ (p ≠ (DirLC_Intersected_pts h₁).back) := by + constructor + · apply (pt_liesint_ne_pt_lieson h₃ (DirLC_intersected_pts_lieson_circle h₁).1).out + apply (pt_liesint_ne_pt_lieson h₃ (DirLC_intersected_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_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_pts h₁).front (liesout_ne_inxpts h₁ h₂ h₃).1.symm) := by + haveI : PtNe p (DirLC_Intersected_pts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ + by_cases heq : (DirLC_Intersected_pts h₁).front = (DirLC_Intersected_pts h₁).back + · simp_rw [← heq] + apply Ray.snd_pt_lies_on_mk_pt_pt + haveI : PtNe (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back := ⟨heq⟩ + have eq₁ : LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_pts_lieson_dlin h₁).2 + have h₂' : p LiesOn (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back) := by + rw [eq₁] + exact h₂ + have eq₂ : perp_foot ω.center l = (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by + rw [← pts_lieson_circle_perpfoot_eq_midpoint (DirLC_intersected_pts_lieson_circle h₁).1 (DirLC_intersected_pts_lieson_circle h₁).2, eq₁] + have trieq₁ : (dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center (DirLC_Intersected_pts h₁).front) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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_intersected_pts_lieson_dlin h₁).1 + have hgt : dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint > dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by + calc + _ = |dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] + _ > |dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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_intersected_pts_lieson_circle h₁).1] + exact h₃ + _ = dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_pts h₁).front (liesint_ne_inxpts h₁ h₂ h₃).1.symm).reverse := by + haveI : PtNe p (DirLC_Intersected_pts 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_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back := ⟨by + contrapose! hs + rw [(DirLC_inx_pts_same_iff_tangent h₁).mp hs.symm]⟩ + have eq₁ : LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_pts_lieson_dlin h₁).2 + have h₂' : p LiesOn (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back) := by + rw [eq₁] + exact h₂ + have eq₂ : perp_foot ω.center l = (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by + rw [← pts_lieson_circle_perpfoot_eq_midpoint (DirLC_intersected_pts_lieson_circle h₁).1 (DirLC_intersected_pts_lieson_circle h₁).2, eq₁] + have trieq₁ : (dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center (DirLC_Intersected_pts h₁).front) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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_intersected_pts_lieson_dlin h₁).1 + have hgt : dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint < dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by + calc + _ = |dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] + _ < |dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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_intersected_pts_lieson_circle h₁).1] + exact h₃ + _ = dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts 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 + +end Circle + +end position + section power namespace Circle @@ -227,9 +312,56 @@ theorem circle_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine _ = (dist ω.center p) ^ 2 - ω.radius ^ 2 := by rw [(DirLC_intersected_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_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) = - power ω p := sorry - -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_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) = power ω p := sorry +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_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) = - power ω p := by + haveI hne : PtNe p (DirLC_Intersected_pts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ + have hl : (DirLC_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_pts 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_Intersected_pts h₁).back = -t := by + calc + _ = ‖VEC p (DirLC_Intersected_pts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = ‖t • (RAY p (DirLC_Intersected_pts 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_Intersected_pts h₁).back = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by + calc + _ = t • (RAY p (DirLC_Intersected_pts h₁).front).toDir.unitVec := by rw [← ht]; rfl + _ = t • ((dist p (DirLC_Intersected_pts h₁).front)⁻¹ • (VEC p (DirLC_Intersected_pts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by rw [smul_smul] + symm + calc + _ = -⟪VEC p (DirLC_Intersected_pts h₁).front, VEC p (DirLC_Intersected_pts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] + _ = -⟪VEC p (DirLC_Intersected_pts h₁).front, (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front)⟫_ℝ := by rw [ht'] + _ = -(t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) * ‖VEC p (DirLC_Intersected_pts h₁).front‖ ^ 2 := by + rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] + simp + _ = (dist p (DirLC_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts 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_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) = power ω p := by + haveI hne : PtNe p (DirLC_Intersected_pts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ + have hl : (DirLC_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_pts 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_Intersected_pts h₁).back = t := by + calc + _ = ‖VEC p (DirLC_Intersected_pts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = ‖t • (RAY p (DirLC_Intersected_pts 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_Intersected_pts h₁).back = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by + calc + _ = t • (RAY p (DirLC_Intersected_pts h₁).front).toDir.unitVec := by rw [← ht]; rfl + _ = t • ((dist p (DirLC_Intersected_pts h₁).front)⁻¹ • (VEC p (DirLC_Intersected_pts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl + _ = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by rw [smul_smul] + symm + calc + _ = ⟪VEC p (DirLC_Intersected_pts h₁).front, VEC p (DirLC_Intersected_pts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] + _ = ⟪VEC p (DirLC_Intersected_pts h₁).front, (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front)⟫_ℝ := by rw [ht'] + _ = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) * ‖VEC p (DirLC_Intersected_pts h₁).front‖ ^ 2 := by rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] + _ = (dist p (DirLC_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts 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 end Circle diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean index f58490cb..f1e21b0e 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean @@ -21,7 +21,6 @@ theorem same_dist_eq_or_eq_neg {A B C : P} [hne : PtNe B A] (h : C LiesOn (LIN A simp apply sub_eq_zero.mpr rfl - right calc _ = (dist A C) • (RAY A B).reverse.2.unitVec := Ray.lieson_eq_dist h @@ -39,4 +38,56 @@ theorem distinct_pts_same_dist_vec_eq {A B C : P} [hne₁ : PtNe B A] [hne₂ : · exact absurd rfl hne₂.out exact hh.symm +theorem midpoint_dist_lt_iff_liesint {A B C : P} [hne : PtNe B C] (h : A LiesOn (LIN B C)) : dist A (SEG B C).midpoint < dist B (SEG B C).midpoint ↔ A LiesInt (SEG B C) := sorry + +theorem midpoint_dist_eq_iff_eq_endpts {A B C : P} [hne : PtNe B C] (h : A LiesOn (LIN B C)) : dist A (SEG B C).midpoint = dist B (SEG B C).midpoint ↔ (A = B) ∨ (A = C) := by + haveI : PtNe (SEG B C).midpoint B := ⟨SegND.midpt_ne_source (seg_nd := SEG_nd B C)⟩ + constructor + · intro hh + rw [dist_comm, ← Seg.length_eq_dist, dist_comm, Seg.length_eq_dist] at hh + have : A LiesOn (LIN (SEG B C).midpoint B) := by sorry + rcases same_dist_eq_or_eq_neg this hh with h₁ | h₂ + · left; exact h₁ + right + apply (eq_iff_vec_eq_zero _ _).mpr + calc + _ = VEC (SEG B C).midpoint A - VEC (SEG B C).midpoint C := by rw [vec_sub_vec] + _ = VEC B (SEG B C).midpoint - VEC (SEG B C).midpoint C := by rw [h₂] + _ = 0 := by + rw [Seg.vec_midpt_eq (seg := SEG B C)] + simp + intro hh + rcases hh with hh | hh + · rw [hh] + rw [hh, dist_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist] + symm + apply dist_target_eq_dist_source_of_midpt (seg := (SEG B C)) + +theorem midpoint_dist_gt_iff_liesout {A B C : P} [hne : PtNe B C] (h : A LiesOn (LIN B C)) : dist A (SEG B C).midpoint > dist B (SEG B C).midpoint ↔ ¬ (A LiesOn (SEG B C)) := by + apply Iff.not_right + push_neg + apply Iff.trans le_iff_lt_or_eq + constructor + · intro heq + rcases heq with heq | heq + · have : A LiesInt (SEG B C) := (midpoint_dist_lt_iff_liesint h).mp heq + exact this.1 + rcases (midpoint_dist_eq_iff_eq_endpts h).mp heq with heq | heq + · rw [heq] + apply Seg.source_lies_on + rw [heq] + apply Seg.target_lies_on + intro hh + by_cases hh' : A LiesInt (SEG B C) + · left + exact (midpoint_dist_lt_iff_liesint h).mpr hh' + right + apply (midpoint_dist_eq_iff_eq_endpts h).mpr + contrapose! hh' + exact ⟨hh, hh'⟩ + +theorem liesint_segnd_iff_lieson_ray_reverse {A B C : P} [hne₁ : PtNe B C] [hne₂ : PtNe A B] (h : A LiesOn (LIN B C)) : A LiesInt (SEG B C) ↔ C LiesOn (RAY A B).reverse := sorry + +theorem not_lies_on_segnd_iff_lieson_ray {A B C : P} [hne₁ : PtNe B C] [hne₂ : PtNe A B] (h : A LiesOn (LIN B C)) : ¬ (A LiesOn (SEG B C)) ↔ C LiesOn (RAY A B) := sorry + end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean index 94ccf54e..1141baf8 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean @@ -5,5 +5,6 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] +theorem Triangle.IsCongr.unique_of_eq_eq {tr₁ tr₂ : Triangle P} (h : tr₁.IsCongr tr₂) (p₁ : tr₁.point₁ = tr₂.point₁) (p₂ : tr₁.point₂ = tr₂.point₂) [hne : PtNe tr₁.point₁ tr₁.point₂] : tr₁.point₃ = tr₂.point₃ := sorry end EuclidGeom From a4d83818a610444adc1945e1e4151f83bb972437 Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Sun, 24 Dec 2023 23:44:11 +0800 Subject: [PATCH 3/8] 12.24-2 fix finish a proof in CCPosition --- .../Foundation/Axiom/Circle/CCPosition.lean | 72 ++++++++++++++++++- .../Foundation/Axiom/Circle/LCPosition.lean | 7 +- .../Foundation/Axiom/Linear/Line_trash.lean | 2 +- 3 files changed, 71 insertions(+), 10 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean index f452793a..3edcd92f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean @@ -345,9 +345,75 @@ theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω lemma CC_inx_pts_not_colinear {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (¬ colinear (CC_Intersected_pts h).left ω₁.center ω₂.center) ∧ (¬ colinear (CC_Intersected_pts h).right ω₁.center ω₂.center) := by constructor · intro hc - -- Triangle.edge_sum_eq_edge_iff_colinear - sorry - sorry + set tri : Triangle P := ▵ (CC_Intersected_pts h).left ω₁.center ω₂.center with tri_def + have : colinear tri.1 tri.2 tri.3 := hc + rw [Triangle.edge_sum_eq_edge_iff_colinear] at this + rcases this with heq | (heq | heq) + · rw [tri_def] at heq + have heq : dist ω₁.center ω₂.center + dist ω₂.center (CC_Intersected_pts h).left = dist (CC_Intersected_pts h).left ω₁.center := heq + have hgt : dist ω₁.center ω₂.center > dist ω₁.center ω₂.center := by + calc + _ > abs (ω₂.radius - ω₁.radius) := h.2 + _ = abs (dist ω₂.center (CC_Intersected_pts h).left - dist (CC_Intersected_pts h).left ω₁.center) := by rw [← (CC_inx_pts_lieson_circles h).1, dist_comm, (CC_inx_pts_lieson_circles h).2.1] + _ = dist ω₁.center ω₂.center := by + rw [← heq] + ring_nf + rw [abs_neg, abs_of_nonneg dist_nonneg] + linarith + · rw [tri_def] at heq + have heq : dist ω₂.center (CC_Intersected_pts h).left + dist (CC_Intersected_pts h).left ω₁.center = dist ω₁.center ω₂.center := heq + have hlt : dist ω₁.center ω₂.center < dist ω₁.center ω₂.center := by + calc + _ < ω₁.radius + ω₂.radius := h.1 + _ = dist (CC_Intersected_pts h).left ω₁.center + dist ω₂.center (CC_Intersected_pts h).left := by rw [← (CC_inx_pts_lieson_circles h).1, dist_comm, (CC_inx_pts_lieson_circles h).2.1] + _ = dist ω₁.center ω₂.center := by rw [← heq]; ring + linarith + rw [tri_def] at heq + have heq : dist (CC_Intersected_pts h).left ω₁.center + dist ω₁.center ω₂.center = dist ω₂.center (CC_Intersected_pts h).left := heq + have hgt : dist ω₁.center ω₂.center > dist ω₁.center ω₂.center := by + calc + _ > abs (ω₂.radius - ω₁.radius) := h.2 + _ = abs (dist ω₂.center (CC_Intersected_pts h).left - dist (CC_Intersected_pts h).left ω₁.center) := by rw [← (CC_inx_pts_lieson_circles h).1, dist_comm, (CC_inx_pts_lieson_circles h).2.1] + _ = dist ω₁.center ω₂.center := by + rw [← heq] + ring_nf + rw [abs_of_nonneg dist_nonneg] + linarith + intro hc + set tri : Triangle P := ▵ (CC_Intersected_pts h).right ω₁.center ω₂.center with tri_def + have : colinear tri.1 tri.2 tri.3 := hc + rw [Triangle.edge_sum_eq_edge_iff_colinear] at this + rcases this with heq | (heq | heq) + · rw [tri_def] at heq + have heq : dist ω₁.center ω₂.center + dist ω₂.center (CC_Intersected_pts h).right = dist (CC_Intersected_pts h).right ω₁.center := heq + have hgt : dist ω₁.center ω₂.center > dist ω₁.center ω₂.center := by + calc + _ > abs (ω₂.radius - ω₁.radius) := h.2 + _ = abs (dist ω₂.center (CC_Intersected_pts h).right - dist (CC_Intersected_pts h).right ω₁.center) := by rw [← (CC_inx_pts_lieson_circles h).2.2.1, dist_comm, (CC_inx_pts_lieson_circles h).2.2.2] + _ = dist ω₁.center ω₂.center := by + rw [← heq] + ring_nf + rw [abs_neg, abs_of_nonneg dist_nonneg] + linarith + · rw [tri_def] at heq + have heq : dist ω₂.center (CC_Intersected_pts h).right + dist (CC_Intersected_pts h).right ω₁.center = dist ω₁.center ω₂.center := heq + have hlt : dist ω₁.center ω₂.center < dist ω₁.center ω₂.center := by + calc + _ < ω₁.radius + ω₂.radius := h.1 + _ = dist (CC_Intersected_pts h).right ω₁.center + dist ω₂.center (CC_Intersected_pts h).right := by rw [← (CC_inx_pts_lieson_circles h).2.2.1, dist_comm, (CC_inx_pts_lieson_circles h).2.2.2] + _ = dist ω₁.center ω₂.center := by rw [← heq]; ring + linarith + rw [tri_def] at heq + have heq : dist (CC_Intersected_pts h).right ω₁.center + dist ω₁.center ω₂.center = dist ω₂.center (CC_Intersected_pts h).right := heq + have hgt : dist ω₁.center ω₂.center > dist ω₁.center ω₂.center := by + calc + _ > abs (ω₂.radius - ω₁.radius) := h.2 + _ = abs (dist ω₂.center (CC_Intersected_pts h).right - dist (CC_Intersected_pts h).right ω₁.center) := by rw [← (CC_inx_pts_lieson_circles h).2.2.1, dist_comm, (CC_inx_pts_lieson_circles h).2.2.2] + _ = dist ω₁.center ω₂.center := by + rw [← heq] + ring_nf + rw [abs_of_nonneg dist_nonneg] + linarith theorem CC_inx_pts_tri_acongr {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (▵ ω₁.center ω₂.center (CC_Intersected_pts h).left) ≅ₐ (▵ ω₁.center ω₂.center (CC_Intersected_pts h).right) := by haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩ diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index a5a34090..72ff4e74 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -214,9 +214,7 @@ theorem DirLC_tangent_pt_eq_perp_foot {l : DirLine P} {ω : Circle P} (h : l Tan _ = l.toLine.toProj.perp := DirLC_tangent_pt_center_perp_line h _ = l.toProj.perp := by rw [DirLine.toLine_toProj_eq_toProj] symm - apply perp_foot_unique _ hp - exact (DirLC_intersected_pts_lieson_dlin _).1 - exact perp_foot_unique (DirLC_intersected_pts_lieson_dlin _).1 (hne := ⟨(DirLC_tangent_pt_ne_center h)⟩) hp + exact perp_foot_unique (DirLC_intersected_pts_lieson_dlin _).1 hp @@ -298,8 +296,6 @@ theorem pt_pt_perp_tangent {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ haveI : PtNe B ω.center := pt_lieson_ne_center h₂ have heq : perp_foot ω.center (DLIN A B) = B := perp_foot_unique DirLine.snd_pt_lies_on_mk_pt_pt hp.symm show dist_pt_line ω.center (DLIN A B) = ω.radius - have heq : perp_foot ω.center (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) = B := perp_foot_unique (DirLine.snd_pt_lies_on_mk_pt_pt (_h := ⟨ (pt_liesout_ne_pt_lieson h₁ h₂).out.symm ⟩ )) (hne := (pt_lieson_ne_center h₂)) hp.symm - show dist_pt_line ω.center (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) = ω.radius calc _ = (SEG ω.center (perp_foot ω.center (DLIN A B))).length := rfl _ = (SEG ω.center B).length := by rw [heq] @@ -311,7 +307,6 @@ theorem pt_pt_perp_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) 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] - _ = perp_foot ω.center (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) := by rw [perp_foot_unique (DirLine.snd_pt_lies_on_mk_pt_pt (_h := ⟨(pt_liesout_ne_pt_lieson h₁ h₂).out.symm⟩)) (hne := (pt_lieson_ne_center h₂)) hp.symm] _ = DirLC_Tangent_pt (pt_pt_perp_tangent h₁ h₂ hp) := by rw [DirLC_tangent_pt_eq_perp_foot _] end Circle diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean index 5bc9761a..167a05f7 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean @@ -94,7 +94,7 @@ theorem midpoint_dist_gt_iff_liesout {A B C : P} [hne : PtNe B C] (h : A LiesOn right apply (midpoint_dist_eq_iff_eq_endpts h).mpr contrapose! hh' - exact ⟨hh, hh'⟩ + exact ⟨hh, hh'.1, hh'.2⟩ theorem liesint_segnd_iff_lieson_ray_reverse {A B C : P} [hne₁ : PtNe B C] [hne₂ : PtNe A B] (h : A LiesOn (LIN B C)) : A LiesInt (SEG B C) ↔ C LiesOn (RAY A B).reverse := sorry From ee31ec99245a451cf60d1adb27bef2f2e7892ea3 Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Sat, 6 Jan 2024 23:13:30 +0800 Subject: [PATCH 4/8] 1.6 some adjustment --- .../Foundation/Axiom/Circle/Basic.lean | 52 +++++++++++++++++++ .../Foundation/Axiom/Circle/LCPosition.lean | 3 ++ 2 files changed, 55 insertions(+) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean index 43a436ec..b12a4669 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean @@ -115,6 +115,14 @@ instance pt_liesint_ne_pt_lieson {A B : P} {ω : Circle P} (h₁ : A LiesInt ω) rw [hgt, heq] ⟩ +instance pt_liesout_ne_pt_liesint {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesInt ω) : PtNe A B := ⟨by + have hgt : dist ω.center A > ω.radius := h₁ + have hlt : dist ω.center B < ω.radius := h₂ + contrapose! hgt + rw [hgt] + linarith + ⟩ + theorem interior_of_circle_iff_inside_not_on_circle (p : P) (ω : Circle P) : p LiesInt ω ↔ (p LiesIn ω) ∧ (¬ p LiesOn ω) := by show dist ω.center p < ω.radius ↔ (dist ω.center p ≤ ω.radius) ∧ (¬ dist ω.center p = ω.radius) push_neg @@ -220,4 +228,48 @@ end Circle end colinear +section antipode + +namespace Circle + +def antipode (A : P) (ω : Circle P) : P := VEC A ω.center +ᵥ ω.center + +@[simp] +theorem antipode_lieson_circle {A : P} {ω : Circle P} {ha : A LiesOn ω} : (antipode A ω) LiesOn ω := by + show dist ω.center (antipode A ω) = ω.radius + rw [NormedAddTorsor.dist_eq_norm', antipode, vsub_vadd_eq_vsub_sub] + simp + show ‖ω.center -ᵥ A‖ = ω.radius + rw [← NormedAddTorsor.dist_eq_norm', ha] + +theorem antipode_symm {A B : P} {ω : Circle P} {ha : A LiesOn ω} (h : antipode A ω = B) : antipode B ω = A := by + show VEC B ω.center +ᵥ ω.center = A + symm + apply (eq_vadd_iff_vsub_eq _ _ _).mpr + show VEC ω.center A = VEC B ω.center + have : VEC ω.center B = VEC A ω.center := by + show B -ᵥ ω.center = VEC A ω.center + apply (eq_vadd_iff_vsub_eq _ _ _).mp h.symm + rw [← neg_vec, ← this, neg_vec] + +@[simp] +theorem antipode_distinct {A : P} {ω : Circle P} {ha : A LiesOn ω} : antipode A ω ≠ A := by + intro eq + have : VEC ω.center A = VEC A ω.center := by + show A -ᵥ ω.center = VEC A ω.center + apply (eq_vadd_iff_vsub_eq _ _ _).mp eq.symm + have neq : A ≠ ω.center := (pt_lieson_ne_center ha).out + contrapose! neq + apply (eq_iff_vec_eq_zero _ _).mpr + have : 2 • (VEC ω.center A) = 0 := by + rw [two_smul] + nth_rw 1 [this] + rw [vec_add_vec] + simp + apply (two_nsmul_eq_zero ℝ _).mp this + +end Circle + +end antipode + end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index 72ff4e74..c129ec78 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -51,12 +51,15 @@ theorem DirLC_intersect_iff_tangent_or_secant {l : DirLine P} {ω : Circle P} : have : dist_pt_line ω.center l.toLine < ω.radius := h linarith +end Circle @[ext] structure DirLCInxpts (P : Type _) [EuclideanPlane P] where front : P back : P +namespace Circle + 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 have : (dist_pt_line ω.center l.toLine) ^ 2 ≤ ω.radius ^ 2 := by From 47b9532afee6dd39e3f904b77034e3691b8d98d3 Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Sun, 7 Jan 2024 10:06:59 +0800 Subject: [PATCH 5/8] name changed --- .../Foundation/Axiom/Circle/CirclePower.lean | 172 +++++++++--------- .../Foundation/Axiom/Circle/LCPosition.lean | 75 ++++---- 2 files changed, 122 insertions(+), 125 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean index adcfc4f2..c951d545 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean @@ -162,7 +162,7 @@ lemma tangent_length_sq_eq_power {p : P} {l : DirLine P} {ω : Circle P} (h₁ : _ = (dist ω.center p) ^ 2 - (dist ω.center (DirLC_Tangent_pt h₁)) ^ 2 := by rw [DirLC_tangent_pt_eq_perp_foot] _ = (dist ω.center p) ^ 2 - ω.radius ^ 2 := by congr - exact (DirLC_intersected_pts_lieson_circle (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h₁))).1 + exact (DirLC_inx_pts_lieson_circle (DirLC_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 +181,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_Intersected_pts h₁).front) ∧ (p ≠ (DirLC_Intersected_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 ≠ (DirLC_inx_pts h₁).front) ∧ (p ≠ (DirLC_inx_pts h₁).back) := by constructor - · apply (pt_liesout_ne_pt_lieson h₃ (DirLC_intersected_pts_lieson_circle h₁).1).out - apply (pt_liesout_ne_pt_lieson h₃ (DirLC_intersected_pts_lieson_circle h₁).2).out + · 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 -lemma liesint_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (p ≠ (DirLC_Intersected_pts h₁).front) ∧ (p ≠ (DirLC_Intersected_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 ≠ (DirLC_inx_pts h₁).front) ∧ (p ≠ (DirLC_inx_pts h₁).back) := by constructor - · apply (pt_liesint_ne_pt_lieson h₃ (DirLC_intersected_pts_lieson_circle h₁).1).out - apply (pt_liesint_ne_pt_lieson h₃ (DirLC_intersected_pts_lieson_circle h₁).2).out + · 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 -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_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_pts h₁).front (liesout_ne_inxpts h₁ h₂ h₃).1.symm) := by - haveI : PtNe p (DirLC_Intersected_pts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ - by_cases heq : (DirLC_Intersected_pts h₁).front = (DirLC_Intersected_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 ω) : (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 · simp_rw [← heq] apply Ray.snd_pt_lies_on_mk_pt_pt - haveI : PtNe (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back := ⟨heq⟩ - have eq₁ : LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_pts_lieson_dlin h₁).2 - have h₂' : p LiesOn (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back) := by + 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 rw [eq₁] exact h₂ - have eq₂ : perp_foot ω.center l = (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by - rw [← pts_lieson_circle_perpfoot_eq_midpoint (DirLC_intersected_pts_lieson_circle h₁).1 (DirLC_intersected_pts_lieson_circle h₁).2, eq₁] - have trieq₁ : (dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 := by + 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 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_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center (DirLC_Intersected_pts h₁).front) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 := by + 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 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_intersected_pts_lieson_dlin h₁).1 - have hgt : dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint > dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by + 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 calc - _ = |dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] - _ > |dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint| := by + _ = |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 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_intersected_pts_lieson_circle h₁).1] + rw [abs_of_nonneg dist_nonneg, abs_of_nonneg dist_nonneg, (DirLC_inx_pts_lieson_circle h₁).1] exact h₃ - _ = dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_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 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_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_pts h₁).front (liesint_ne_inxpts h₁ h₂ h₃).1.symm).reverse := by - haveI : PtNe p (DirLC_Intersected_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 ω) : (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⟩ have hs : dist_pt_line ω.center l.toLine < ω.radius := by calc _ ≤ dist ω.center p := dist_pt_line_shortest _ _ h₂ _ < ω.radius := h₃ - haveI : PtNe (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back := ⟨by + haveI : PtNe (DirLC_inx_pts h₁).front (DirLC_inx_pts h₁).back := ⟨by contrapose! hs rw [(DirLC_inx_pts_same_iff_tangent h₁).mp hs.symm]⟩ - have eq₁ : LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back = l := Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_pts_lieson_dlin h₁).2 - have h₂' : p LiesOn (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back) := by + 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 [eq₁] exact h₂ - have eq₂ : perp_foot ω.center l = (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by - rw [← pts_lieson_circle_perpfoot_eq_midpoint (DirLC_intersected_pts_lieson_circle h₁).1 (DirLC_intersected_pts_lieson_circle h₁).2, eq₁] - have trieq₁ : (dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center p) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 := by + 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 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_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 = (dist ω.center (DirLC_Intersected_pts h₁).front) ^ 2 - (dist ω.center (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint) ^ 2 := by + 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 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_intersected_pts_lieson_dlin h₁).1 - have hgt : dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint < dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint := by + 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 calc - _ = |dist p (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint| := by rw [abs_of_nonneg dist_nonneg] - _ < |dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back).midpoint| := by + _ = |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 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_intersected_pts_lieson_circle h₁).1] + rw [abs_of_nonneg dist_nonneg, abs_of_nonneg dist_nonneg, (DirLC_inx_pts_lieson_circle h₁).1] exact h₃ - _ = dist (DirLC_Intersected_pts h₁).front (SEG (DirLC_Intersected_pts h₁).front (DirLC_Intersected_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 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 +266,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_Intersected_pts h₁).front, VEC p (DirLC_Intersected_pts h₁).back⟫_ℝ = power ω p := by +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_Intersected_pts h₁).back = (DirLC_Intersected_pts h₁).front := (DirLC_inx_pts_same_iff_tangent h₁).mpr h + · have heq : (DirLC_inx_pts h₁).back = (DirLC_inx_pts h₁).front := (DirLC_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 rw [dist_comm, NormedAddTorsor.dist_eq_norm'] rfl _ = power ω p := tangent_length_sq_eq_power _ h₂ - haveI : PtNe (DirLC_Intersected_pts h₁).back (DirLC_Intersected_pts h₁).front := ⟨by + haveI : PtNe (DirLC_inx_pts h₁).back (DirLC_inx_pts 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 rw [this] ⟩ - have heq : - VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front = VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).back := by + have heq : - VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).front = VEC (perp_foot ω.center l) (DirLC_inx_pts h₁).back := by calc - _ = VEC (DirLC_Intersected_pts h₁).front (perp_foot ω.center l) := by rw [neg_vec] - _ = VEC (DirLC_Intersected_pts h₁).front (perp_foot ω.center (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back)) := by + _ = 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 congr; symm - apply Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_pts_lieson_dlin h₁).2 - _ = VEC (perp_foot ω.center (LIN (DirLC_Intersected_pts h₁).front (DirLC_Intersected_pts h₁).back)) (DirLC_Intersected_pts h₁).back := by - apply pts_lieson_circle_vec_eq (DirLC_intersected_pts_lieson_circle h₁).1 (DirLC_intersected_pts_lieson_circle h₁).2 - _ = VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).back := by + 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 congr - apply Line.eq_line_of_pt_pt_of_ne (DirLC_intersected_pts_lieson_dlin h₁).1 (DirLC_intersected_pts_lieson_dlin h₁).2 + apply Line.eq_line_of_pt_pt_of_ne (DirLC_inx_pts_lieson_dlin h₁).1 (DirLC_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_Intersected_pts h₁).front (perp_foot ω.center l)) ^ 2 = (dist ω.center (DirLC_Intersected_pts h₁).front) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2 := by + 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 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_intersected_pts_lieson_dlin h₁).1 + apply Pythagoras_of_perp_foot _ _ (DirLC_inx_pts_lieson_dlin h₁).1 calc - _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front, VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).back⟫_ℝ := by rw [vec_add_vec, vec_add_vec] - _ = ⟪VEC p (perp_foot ω.center l) + VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front, VEC p (perp_foot ω.center l) - VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front⟫_ℝ := by rw [← heq, sub_eq_add_neg] - _ = ‖VEC p (perp_foot ω.center l)‖ ^ 2 - ‖VEC (perp_foot ω.center l) (DirLC_Intersected_pts h₁).front‖ ^ 2 := by + _ = ⟪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 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_Intersected_pts h₁).front (perp_foot ω.center l)) ^ 2 := by + _ = (dist p (perp_foot ω.center l)) ^ 2 - (dist (DirLC_inx_pts 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_Intersected_pts h₁).front) ^ 2 - (dist ω.center (perp_foot ω.center l)) ^ 2) := by rw [eq₁, eq₂] - _ = (dist ω.center p) ^ 2 - (dist ω.center (DirLC_Intersected_pts h₁).front) ^ 2 := by ring - _ = (dist ω.center p) ^ 2 - ω.radius ^ 2 := by rw [(DirLC_intersected_pts_lieson_circle h₁).1] + _ = ((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] _ = 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_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) = - power ω p := by - haveI hne : PtNe p (DirLC_Intersected_pts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ - have hl : (DirLC_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_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 (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₃ rcases pt_lies_on_ray_rev_iff_vec_opposite_dir.mp hl with ⟨t, tnonpos, ht⟩ - have heq : dist p (DirLC_Intersected_pts h₁).back = -t := by + have heq : dist p (DirLC_inx_pts h₁).back = -t := by calc - _ = ‖VEC p (DirLC_Intersected_pts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = ‖t • (RAY p (DirLC_Intersected_pts h₁).front).toDir.unitVec‖ := by rw [← ht]; rfl + _ = ‖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 _ = -t := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonpos tnonpos] - have ht' : VEC p (DirLC_Intersected_pts h₁).back = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by + 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 calc - _ = t • (RAY p (DirLC_Intersected_pts h₁).front).toDir.unitVec := by rw [← ht]; rfl - _ = t • ((dist p (DirLC_Intersected_pts h₁).front)⁻¹ • (VEC p (DirLC_Intersected_pts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by rw [smul_smul] + _ = 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] symm calc - _ = -⟪VEC p (DirLC_Intersected_pts h₁).front, VEC p (DirLC_Intersected_pts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] - _ = -⟪VEC p (DirLC_Intersected_pts h₁).front, (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front)⟫_ℝ := by rw [ht'] - _ = -(t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) * ‖VEC p (DirLC_Intersected_pts h₁).front‖ ^ 2 := by + _ = -⟪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] simp - _ = (dist p (DirLC_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) := by + _ = (dist p (DirLC_inx_pts h₁).front) * (dist p (DirLC_inx_pts 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_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) = power ω p := by - haveI hne : PtNe p (DirLC_Intersected_pts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ - have hl : (DirLC_Intersected_pts h₁).back LiesOn (RAY p (DirLC_Intersected_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 (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₃ rcases Ray.lies_on_iff.mp hl with ⟨t, tnonneg, ht⟩ - have heq : dist p (DirLC_Intersected_pts h₁).back = t := by + have heq : dist p (DirLC_inx_pts h₁).back = t := by calc - _ = ‖VEC p (DirLC_Intersected_pts h₁).back‖ := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = ‖t • (RAY p (DirLC_Intersected_pts h₁).front).toDir.unitVec‖ := by rw [← ht]; rfl + _ = ‖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 _ = t := by rw [norm_smul, Dir.norm_unitVec, mul_one, Real.norm_of_nonneg tnonneg] - have ht' : VEC p (DirLC_Intersected_pts h₁).back = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by + 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 calc - _ = t • (RAY p (DirLC_Intersected_pts h₁).front).toDir.unitVec := by rw [← ht]; rfl - _ = t • ((dist p (DirLC_Intersected_pts h₁).front)⁻¹ • (VEC p (DirLC_Intersected_pts h₁).front)) := by rw [dist_comm, NormedAddTorsor.dist_eq_norm']; rfl - _ = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front) := by rw [smul_smul] + _ = 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] symm calc - _ = ⟪VEC p (DirLC_Intersected_pts h₁).front, VEC p (DirLC_Intersected_pts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] - _ = ⟪VEC p (DirLC_Intersected_pts h₁).front, (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) • (VEC p (DirLC_Intersected_pts h₁).front)⟫_ℝ := by rw [ht'] - _ = (t * (dist p (DirLC_Intersected_pts h₁).front)⁻¹) * ‖VEC p (DirLC_Intersected_pts h₁).front‖ ^ 2 := by rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] - _ = (dist p (DirLC_Intersected_pts h₁).front) * (dist p (DirLC_Intersected_pts h₁).back) := by + _ = ⟪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 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 c129ec78..d405cb4f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -70,57 +70,57 @@ lemma dist_pt_line_ineq {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersect exact length_nonneg linarith -def DirLC_Intersected_pts {l : DirLine P} {ω : Circle P} (_h : DirLine.IsIntersected l ω) : DirLCInxpts P where +def DirLC_inx_pts {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_intersected_pts_lieson_dlin {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((DirLC_Intersected_pts h).front LiesOn l) ∧ ((DirLC_Intersected_pts h).back LiesOn l) := by +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 have hl : perp_foot ω.center l.toLine LiesOn l := by apply perp_foot_lies_on_line constructor - · have : (DirLC_Intersected_pts h).front LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl) := by + · have : (DirLC_inx_pts 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_Intersected_pts Vec.mkPtPt + unfold DirLC_inx_pts 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_Intersected_pts h).front LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).toDirLine := by + have : (DirLC_inx_pts 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_Intersected_pts h).back LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).reverse := by + have : (DirLC_inx_pts 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_Intersected_pts Vec.mkPtPt + unfold DirLC_inx_pts 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_Intersected_pts h).back LiesOn (Ray.mk_pt_dirline (perp_foot ω.center l.toLine) l hl).toDirLine := by + have : (DirLC_inx_pts 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_intersected_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : ((DirLC_Intersected_pts h).front LiesOn ω) ∧ ((DirLC_Intersected_pts h).back LiesOn ω) := by +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 constructor - · have : (SEG ω.center (perp_foot ω.center l.toLine)).length ^ 2 + (SEG (DirLC_Intersected_pts h).front (perp_foot ω.center l.toLine)).length ^ 2 = (SEG ω.center (DirLC_Intersected_pts h).front).length ^ 2 := by apply Pythagoras_of_perp_foot _ _ (DirLC_intersected_pts_lieson_dlin h).1 + · 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 rw [← dist_pt_line] at this - show dist ω.center (DirLC_Intersected_pts h).front = ω.radius + show dist ω.center (DirLC_inx_pts h).front = ω.radius apply (sq_eq_sq _ _).mp calc - _ = (dist_pt_line ω.center l.toLine) ^ 2 + (SEG (DirLC_Intersected_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_Intersected_pts h).front (perp_foot ω.center l.toLine)‖ ^ 2 := by + _ = (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 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_Intersected_pts + unfold DirLC_inx_pts 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 +129,17 @@ theorem DirLC_intersected_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : 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_Intersected_pts h).back (perp_foot ω.center l.toLine)).length ^ 2 = (SEG ω.center (DirLC_Intersected_pts h).back).length ^ 2 := by apply Pythagoras_of_perp_foot _ _ (DirLC_intersected_pts_lieson_dlin h).2 + 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 rw [← dist_pt_line] at this - show dist ω.center (DirLC_Intersected_pts h).back = ω.radius + show dist ω.center (DirLC_inx_pts h).back = ω.radius apply (sq_eq_sq _ _).mp calc - _ = (dist_pt_line ω.center l.toLine) ^ 2 + (SEG (DirLC_Intersected_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_Intersected_pts h).back (perp_foot ω.center l.toLine)‖ ^ 2 := by + _ = (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 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_Intersected_pts + unfold DirLC_inx_pts 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 +149,8 @@ theorem DirLC_intersected_pts_lieson_circle {l : DirLine P} {ω : Circle P} (h : 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_Intersected_pts h).back = (DirLC_Intersected_pts h).front ↔ (l Tangent ω) := by - unfold DirLC_Intersected_pts +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 simp apply Iff.trans (neg_eq_self ℝ _) apply Iff.trans smul_eq_zero @@ -175,21 +175,18 @@ theorem DirLC_inx_pts_same_iff_tangent {l : DirLine P} {ω : Circle P} (h : DirL left; rw [this, sub_self] simp -def DirLC_Tangent_pt {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : P := (DirLC_Intersected_pts (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h))).front +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 lemma DirLC_tangent_pt_ne_center {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : DirLC_Tangent_pt h ≠ ω.center := by - apply dist_pos.mp have : DirLC_Tangent_pt h LiesOn ω := by - rcases DirLC_intersected_pts_lieson_circle (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h)) with ⟨h₁, _⟩ + rcases DirLC_inx_pts_lieson_circle (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h)) with ⟨h₁, _⟩ exact h₁ - have : dist ω.center (DirLC_Tangent_pt h) = ω.radius := this - rw [dist_comm, this] - exact ω.rad_pos + exact (pt_lieson_ne_center this).out 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 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_Intersected_pts + unfold DirLC_Tangent_pt DirLC_inx_pts simp apply (Real.sqrt_eq_zero _).mpr rw [h]; ring @@ -217,7 +214,7 @@ theorem DirLC_tangent_pt_eq_perp_foot {l : DirLine P} {ω : Circle P} (h : l Tan _ = l.toLine.toProj.perp := DirLC_tangent_pt_center_perp_line h _ = l.toProj.perp := by rw [DirLine.toLine_toProj_eq_toProj] symm - exact perp_foot_unique (DirLC_intersected_pts_lieson_dlin _).1 hp + exact perp_foot_unique (DirLC_inx_pts_lieson_dlin _).1 hp @@ -231,8 +228,8 @@ 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_Intersected_pts h).front - exact ⟨(DirLC_intersected_pts_lieson_dlin h).1, (DirLC_intersected_pts_lieson_circle h).1⟩ + use (DirLC_inx_pts h).front + exact ⟨(DirLC_inx_pts_lieson_dlin h).1, (DirLC_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 @@ -241,8 +238,8 @@ If we need, we can add some coercion to state that inx_pts with respect to "InxW -/ -- def DirLC_Inx_pts {l : DirLine P} {ω : Circle P} (h : l InxWith ω) : DirLCInxpts P where --- front := (DirLC_Intersected_pts (DirLC_inxwith_iff_intersect.mp h)).front --- back := (DirLC_Intersected_pts (DirLC_inxwith_iff_intersect.mp h)).back +-- front := (DirLC_inx_pts (DirLC_inxwith_iff_intersect.mp h)).front +-- back := (DirLC_inx_pts (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 @@ -253,7 +250,7 @@ If we need, we can add some coercion to state that inx_pts with respect to "InxW /- 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_Intersected_pts h).front) ∨ (A = (DirLC_Intersected_pts h).back) := by +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' · left show A = DirLC_Tangent_pt h' @@ -264,16 +261,16 @@ theorem DirLC_intersection_eq_inxpts {l : DirLine P} {ω : Circle P} {A : P} (h _ = DirLC_Tangent_pt h' := by rw [DirLC_tangent_pt_eq_perp_foot _] contrapose! h₂ intro h₃ - haveI hne₁ : PtNe A (DirLC_Intersected_pts h).front := ⟨h₂.1⟩ - haveI hne₂ : PtNe A (DirLC_Intersected_pts h).back := ⟨h₂.2⟩ - haveI hne₃ : PtNe (DirLC_Intersected_pts h).back (DirLC_Intersected_pts h).front := ⟨ by + 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 intro eq have h'' : l Tangent ω := (DirLC_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_Intersected_pts h).front (DirLC_Intersected_pts h).back := Line.linear h₁ (DirLC_intersected_pts_lieson_dlin h).1 (DirLC_intersected_pts_lieson_dlin h).2 - have hnc : ¬ (colinear A (DirLC_Intersected_pts h).front (DirLC_Intersected_pts h).back) := three_pts_lieson_circle_not_colinear h₃ (DirLC_intersected_pts_lieson_circle h).1 (DirLC_intersected_pts_lieson_circle h).2 + 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 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 From 75ba6fa307d52212a88ffe333544dd5471f41100 Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Sun, 7 Jan 2024 10:59:30 +0800 Subject: [PATCH 6/8] 1.7 some adjustment in LCPosition --- .../Foundation/Axiom/Circle/LCPosition.lean | 44 ++++++++++--------- 1 file changed, 24 insertions(+), 20 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index d405cb4f..9393c526 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -175,13 +175,30 @@ 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 + 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 + +theorem DirLC_inxwith_iff_intersect {l : DirLine P} {ω : Circle P} : l InxWith ω ↔ DirLine.IsIntersected l ω := by + unfold intersect + constructor + · rintro ⟨A, ⟨h₁, h₂⟩⟩ + show dist_pt_line ω.center l.toLine ≤ ω.radius + calc + _ ≤ 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⟩ + +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 + + +/- 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 -lemma DirLC_tangent_pt_ne_center {l : DirLine P} {ω : Circle P} (h : l Tangent ω) : DirLC_Tangent_pt h ≠ ω.center := by - have : DirLC_Tangent_pt h LiesOn ω := by - rcases DirLC_inx_pts_lieson_circle (DirLC_intersect_iff_tangent_or_secant.mpr (Or.inl h)) with ⟨h₁, _⟩ - exact h₁ - exact (pt_lieson_ne_center this).out +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 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 have h : dist_pt_line ω.center l.toLine = ω.radius := h @@ -218,21 +235,6 @@ theorem DirLC_tangent_pt_eq_perp_foot {l : DirLine P} {ω : Circle P} (h : l Tan - -theorem DirLC_inxwith_iff_intersect {l : DirLine P} {ω : Circle P} : l InxWith ω ↔ DirLine.IsIntersected l ω := by - unfold intersect - constructor - · rintro ⟨A, ⟨h₁, h₂⟩⟩ - show dist_pt_line ω.center l.toLine ≤ ω.radius - calc - _ ≤ 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⟩ - -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 - /- If we need, we can add some coercion to state that inx_pts with respect to "InxWith". -/ @@ -280,6 +282,8 @@ theorem pt_pt_tangent_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut rw [(DirLC_inx_pts_same_iff_tangent _).mpr ht] at heq exact heq + +/- Equivalent condition for tangency -/ 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₂ From 9ad02a612f4d6d2dd4e92737e318e11bd9142d1b Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Thu, 11 Jan 2024 23:10:43 +0800 Subject: [PATCH 7/8] 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 From 1f42b6989e26a0a32942d5aff908af487f0b09ab Mon Sep 17 00:00:00 2001 From: Noaillesss Date: Fri, 12 Jan 2024 15:00:26 +0800 Subject: [PATCH 8/8] 1.12 fix --- .../Axiom/Basic/Angle/AddToMathlib.lean | 2 ++ .../Foundation/Axiom/Basic/Vector.lean | 8 ++++---- .../Foundation/Axiom/Circle/CCPosition.lean | 16 +++++++--------- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean index 001f0314..cf1e229c 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean @@ -1,4 +1,5 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Angle.FromMathlib +import Mathlib.Data.Int.Parity /-! # Theorems that should exist in Mathlib @@ -7,6 +8,7 @@ Maybe we can create some PRs to mathlib in the future. -/ open Real +attribute [ext] Complex.ext /-! ## More theorems about trigonometric functions in Mathlib diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean index b281f8c4..4463af3f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean @@ -184,7 +184,7 @@ lemma toComplex_inv (z : 𝕜) : ↑(z⁻¹) = (z : ℂ)⁻¹ := by ext <;> simp @[simp, norm_cast] lemma abs_toComplex (z : 𝕜) : Complex.abs (z : ℂ) = ‖z‖ := by - rw [← pow_left_inj (map_nonneg _ _) (norm_nonneg _) zero_lt_two, + rw [← pow_left_inj (map_nonneg _ _) (norm_nonneg _) two_ne_zero, Complex.sq_abs, Complex.normSq_apply, norm_sq_eq_def] rfl @@ -400,7 +400,7 @@ instance innerProductSpace' : InnerProductSpace ℝ Vec where norm_sq_eq_inner v := by simp [norm_sq] conj_symm v₁ v₂ := by simp [Complex.conj_ofReal, mul_comm] add_left v₁ v₂ v₃ := by dsimp; ring - smul_left v₁ v₂ z := by dsimp; ring + smul_left v₁ v₂ z := by dsimp; simp; ring lemma real_inner_apply (v₁ v₂ : Vec) : ⟪v₁, v₂⟫_ℝ = v₁.fst * v₂.fst + v₁.snd * v₂.snd := @@ -694,7 +694,7 @@ lemma cdiv_eq_cdiv_iff_cdiv_eq_cdiv {v₁ v₂ v₃ v₄ : Vec} (hv₂ : v₂ @[simp] lemma abs_inner (v₁ v₂ : Vec) : Complex.abs ⟪v₁, v₂⟫_ℂ = ‖v₁‖ * ‖v₂‖ := by - rw [← pow_left_inj (by simp) (by positivity) zero_lt_two] + rw [← pow_left_inj (by simp) (by positivity) two_ne_zero] rw [Complex.abs_apply, sq_sqrt (Complex.normSq_nonneg _)] dsimp [inner, det] rw [mul_pow, norm_sq, norm_sq] @@ -1582,7 +1582,7 @@ theorem map_trans (f g : Dir ≃ Dir) {_ : Dir.NegCommute f} {_ : Dir.NegCommute Proj.map (f.trans g) = (Proj.map f).trans (Proj.map g) := by ext p induction p using Proj.ind - + simp instance : Nonempty Proj := (nonempty_quotient_iff _).mpr <| inferInstanceAs (Nonempty Dir) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean index 3edcd92f..f2831ebf 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean @@ -170,7 +170,7 @@ theorem CC_inscribe_point_centers_colinear {ω₁ : Circle P} {ω₂ : Circle P} apply colinear_of_vec_eq_smul_vec this -theorem CC_included_pt_isint_second_circle {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h₁ : ω₁ IncludeIn ω₂) (h₂ : A LiesOn ω₁) : Circle.IsInt A ω₂ := by +theorem CC_included_pt_isint_second_circle {ω₁ : Circle P} {ω₂ : Circle P} {A : P} (h₁ : ω₁ IncludeIn ω₂) (h₂ : A LiesOn ω₁) : A LiesInt ω₂ := by have : dist ω₂.center A < ω₂.radius := by calc _ ≤ dist ω₁.center ω₂.center + dist ω₁.center A := by apply dist_triangle_left @@ -253,14 +253,12 @@ theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Int rw [← sub_smul] simp push_neg - constructor - · apply Real.sqrt_ne_zero'.mpr - have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by - apply sq_lt_sq.mpr - rw [abs_of_pos ω₁.rad_pos] - exact radical_axis_dist_lt_radius h - linarith - exact Complex.I_ne_zero + apply Real.sqrt_ne_zero'.mpr + have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by + apply sq_lt_sq.mpr + rw [abs_of_pos ω₁.rad_pos] + exact radical_axis_dist_lt_radius h + linarith theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : ((CC_Intersected_pts h).left LiesOn ω₁) ∧ ((CC_Intersected_pts h).left LiesOn ω₂) ∧ ((CC_Intersected_pts h).right LiesOn ω₁) ∧ ((CC_Intersected_pts h).right LiesOn ω₂) := by haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩