/- SPDX-FileCopyrightText: 2026 Advameg, Inc. SPDX-License-Identifier: Apache-2.0 -/ import Mathlib.Data.Fin.Basic import Mathlib.Tactic /-! # Butterfly Theorem Seed This file prepares a proof-facing analytic-coordinate statement for the classical butterfly theorem. -/ namespace AtlasKnownTheorems.ButterflyTheorem abbrev Point : Type := Fin 2 → ℝ def point (x y : ℝ) : Point := fun i => if i = 0 then x else y theorem point_eta (p : Point) : point (p 0) (p 1) = p := by ext i fin_cases i <;> simp [point] def vsub (p q : Point) : Point := fun i => p i - q i def vadd (p q : Point) : Point := fun i => p i + q i noncomputable def midpoint (p q : Point) : Point := fun i => (p i + q i) / 2 def det2 (u v : Point) : ℝ := u 0 * v 1 - u 1 * v 0 def dot2 (u v : Point) : ℝ := u 0 * v 0 + u 1 * v 1 def Collinear (p q r : Point) : Prop := det2 (vsub q p) (vsub r p) = 0 def UniqueIntersection (p q r s x : Point) : Prop := Collinear p q x ∧ Collinear r s x ∧ ∀ z : Point, Collinear p q z → Collinear r s z → z = x def sqNorm (p : Point) : ℝ := p 0 ^ 2 + p 1 ^ 2 theorem dot2_self (p : Point) : dot2 p p = sqNorm p := by unfold dot2 sqNorm ring theorem det2_self (p : Point) : det2 p p = 0 := by unfold det2 ring theorem vsub_vadd_same_left (p q : Point) : vsub (vadd p q) p = q := by ext i simp [vsub, vadd] def sqDist (p q : Point) : ℝ := sqNorm (vsub p q) noncomputable def baseCoord (e z : Point) : Point := point (dot2 z e / sqNorm e) (det2 e z / sqNorm e) def baseUncoord (e z : Point) : Point := point (z 0 * e 0 - z 1 * e 1) (z 0 * e 1 + z 1 * e 0) noncomputable def baseNormalize (m q z : Point) : Point := baseCoord (vsub q m) (vsub z m) def baseUnnormalize (m q z : Point) : Point := vadd m (baseUncoord (vsub q m) z) def OnCircleSq (O : Point) (R : ℝ) (P : Point) : Prop := sqDist P O = R def IsMidpoint (m p q : Point) : Prop := m = midpoint p q structure ButterflyConfiguration where center : Point radiusSq : ℝ M : Point P : Point Q : Point A : Point B : Point C : Point D : Point X : Point Y : Point def DistinctChordEndpoints (cfg : ButterflyConfiguration) : Prop := cfg.P ≠ cfg.Q ∧ cfg.A ≠ cfg.B ∧ cfg.C ≠ cfg.D theorem normalized_base_a_ne_of_distinct {a : ℝ} (h : point (-a) 0 ≠ point a 0) : a ≠ 0 := by intro ha apply h ext i fin_cases i <;> simp [point, ha] theorem y_ne_of_point_ne_of_x_eq {p q : Point} (hpq : p ≠ q) (hx : p 0 = q 0) : p 1 ≠ q 1 := by intro hy apply hpq ext i fin_cases i · exact hx · exact hy /-- Hypotheses for the coordinate butterfly theorem. -/ def ButterflyHyp (cfg : ButterflyConfiguration) : Prop := 0 < cfg.radiusSq ∧ OnCircleSq cfg.center cfg.radiusSq cfg.P ∧ OnCircleSq cfg.center cfg.radiusSq cfg.Q ∧ OnCircleSq cfg.center cfg.radiusSq cfg.A ∧ OnCircleSq cfg.center cfg.radiusSq cfg.B ∧ OnCircleSq cfg.center cfg.radiusSq cfg.C ∧ OnCircleSq cfg.center cfg.radiusSq cfg.D ∧ IsMidpoint cfg.M cfg.P cfg.Q ∧ Collinear cfg.A cfg.M cfg.B ∧ Collinear cfg.C cfg.M cfg.D ∧ Collinear cfg.A cfg.D cfg.X ∧ Collinear cfg.B cfg.C cfg.Y ∧ Collinear cfg.P cfg.Q cfg.X ∧ Collinear cfg.P cfg.Q cfg.Y /-- Minimum butterfly target. -/ def ButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, ButterflyHyp cfg → IsMidpoint cfg.M cfg.X cfg.Y theorem midpoint_comm (p q : Point) : midpoint p q = midpoint q p := by funext i simp [midpoint, add_comm] theorem sqNorm_vsub_ne_zero_of_ne {p q : Point} (hpq : p ≠ q) : sqNorm (vsub p q) ≠ 0 := by intro hnorm have hx : p 0 - q 0 = 0 := by unfold sqNorm vsub at hnorm nlinarith [sq_nonneg (p 0 - q 0), sq_nonneg (p 1 - q 1)] have hy : p 1 - q 1 = 0 := by unfold sqNorm vsub at hnorm nlinarith [sq_nonneg (p 0 - q 0), sq_nonneg (p 1 - q 1)] apply hpq ext i fin_cases i · exact sub_eq_zero.mp hx · exact sub_eq_zero.mp hy theorem eq_of_sqDist_eq_zero {p q : Point} (h : sqDist p q = 0) : p = q := by by_contra hpq exact (sqNorm_vsub_ne_zero_of_ne hpq) h theorem det2_baseCoord {e u v : Point} (he : sqNorm e ≠ 0) : det2 (baseCoord e u) (baseCoord e v) = det2 u v / sqNorm e := by have hnum : dot2 u e * det2 e v - det2 e u * dot2 v e = det2 u v * sqNorm e := by unfold dot2 det2 sqNorm ring unfold baseCoord point calc dot2 u e / sqNorm e * (det2 e v / sqNorm e) - det2 e u / sqNorm e * (dot2 v e / sqNorm e) = (dot2 u e * det2 e v - det2 e u * dot2 v e) / (sqNorm e * sqNorm e) := by ring _ = (det2 u v * sqNorm e) / (sqNorm e * sqNorm e) := by rw [hnum] _ = det2 u v / sqNorm e := by field_simp [he] theorem dot2_sq_add_det2_sq (e u : Point) : dot2 u e ^ 2 + det2 e u ^ 2 = sqNorm u * sqNorm e := by unfold dot2 det2 sqNorm ring theorem sqNorm_baseCoord {e u : Point} (he : sqNorm e ≠ 0) : sqNorm (baseCoord e u) = sqNorm u / sqNorm e := by unfold baseCoord point sqNorm calc (dot2 u e / sqNorm e) ^ 2 + (det2 e u / sqNorm e) ^ 2 = (dot2 u e ^ 2 + det2 e u ^ 2) / (sqNorm e * sqNorm e) := by ring _ = (sqNorm u * sqNorm e) / (sqNorm e * sqNorm e) := by rw [dot2_sq_add_det2_sq] _ = sqNorm u / sqNorm e := by field_simp [he] theorem baseCoord_baseUncoord {e z : Point} (he : sqNorm e ≠ 0) : baseCoord e (baseUncoord e z) = z := by ext i fin_cases i · change dot2 (baseUncoord e z) e / sqNorm e = z 0 have hdot : dot2 (baseUncoord e z) e = z 0 * sqNorm e := by unfold dot2 baseUncoord sqNorm simp [point] ring rw [hdot] field_simp [he] · change det2 e (baseUncoord e z) / sqNorm e = z 1 have hdet : det2 e (baseUncoord e z) = z 1 * sqNorm e := by unfold det2 baseUncoord sqNorm simp [point] ring rw [hdet] field_simp [he] theorem vsub_vsub_same_right (p q r : Point) : vsub (vsub p r) (vsub q r) = vsub p q := by ext i simp [vsub] theorem vsub_baseCoord (e u v : Point) : vsub (baseCoord e u) (baseCoord e v) = baseCoord e (vsub u v) := by ext i fin_cases i <;> simp [baseCoord, vsub, dot2, det2, point] <;> ring theorem det2_baseNormalize_vsub {m q p r s : Point} (hqm : q ≠ m) : det2 (vsub (baseNormalize m q r) (baseNormalize m q p)) (vsub (baseNormalize m q s) (baseNormalize m q p)) = det2 (vsub r p) (vsub s p) / sqNorm (vsub q m) := by have hden : sqNorm (vsub q m) ≠ 0 := sqNorm_vsub_ne_zero_of_ne hqm rw [baseNormalize, baseNormalize, baseNormalize] rw [vsub_baseCoord, vsub_baseCoord] rw [vsub_vsub_same_right, vsub_vsub_same_right] exact det2_baseCoord hden theorem collinear_baseNormalize_iff {m q p r s : Point} (hqm : q ≠ m) : Collinear (baseNormalize m q p) (baseNormalize m q r) (baseNormalize m q s) ↔ Collinear p r s := by have hden : sqNorm (vsub q m) ≠ 0 := sqNorm_vsub_ne_zero_of_ne hqm unfold Collinear rw [det2_baseNormalize_vsub hqm] constructor · intro h field_simp [hden] at h simpa using h · intro h rw [h] simp theorem sqDist_baseNormalize {m q p r : Point} (hqm : q ≠ m) : sqDist (baseNormalize m q p) (baseNormalize m q r) = sqDist p r / sqNorm (vsub q m) := by have hden : sqNorm (vsub q m) ≠ 0 := sqNorm_vsub_ne_zero_of_ne hqm rw [sqDist, sqDist, baseNormalize, baseNormalize, vsub_baseCoord, vsub_vsub_same_right] exact sqNorm_baseCoord hden theorem onCircleSq_baseNormalize {m q o p : Point} {R : ℝ} (hqm : q ≠ m) (h : OnCircleSq o R p) : OnCircleSq (baseNormalize m q o) (R / sqNorm (vsub q m)) (baseNormalize m q p) := by unfold OnCircleSq at * rw [sqDist_baseNormalize hqm, h] theorem baseNormalize_baseUnnormalize {m q z : Point} (hqm : q ≠ m) : baseNormalize m q (baseUnnormalize m q z) = z := by have hden : sqNorm (vsub q m) ≠ 0 := sqNorm_vsub_ne_zero_of_ne hqm rw [baseNormalize, baseUnnormalize, vsub_vadd_same_left] exact baseCoord_baseUncoord hden theorem baseNormalize_surjective {m q : Point} (hqm : q ≠ m) : Function.Surjective (baseNormalize m q) := by intro z exact ⟨baseUnnormalize m q z, baseNormalize_baseUnnormalize hqm⟩ theorem baseNormalize_injective {m q : Point} (hqm : q ≠ m) : Function.Injective (baseNormalize m q) := by intro p r hpr have hdist_img : sqDist (baseNormalize m q p) (baseNormalize m q r) = 0 := by rw [hpr] simp [sqDist, sqNorm, vsub] have hden : sqNorm (vsub q m) ≠ 0 := sqNorm_vsub_ne_zero_of_ne hqm rw [sqDist_baseNormalize hqm] at hdist_img field_simp [hden] at hdist_img exact eq_of_sqDist_eq_zero (by simpa using hdist_img) theorem baseNormalize_midpoint (m q p r : Point) : baseNormalize m q (midpoint p r) = midpoint (baseNormalize m q p) (baseNormalize m q r) := by ext i fin_cases i <;> simp [baseNormalize, baseCoord, midpoint, vsub, dot2, det2, point] <;> ring theorem isMidpoint_of_baseNormalize {m q p r : Point} (hqm : q ≠ m) (h : IsMidpoint (baseNormalize m q m) (baseNormalize m q p) (baseNormalize m q r)) : IsMidpoint m p r := by unfold IsMidpoint at * have hmap : baseNormalize m q (midpoint p r) = baseNormalize m q m := by rw [baseNormalize_midpoint, ← h] exact (baseNormalize_injective hqm hmap).symm theorem uniqueIntersection_baseNormalize {m q u v r s x : Point} (hqm : q ≠ m) (h : UniqueIntersection u v r s x) : UniqueIntersection (baseNormalize m q u) (baseNormalize m q v) (baseNormalize m q r) (baseNormalize m q s) (baseNormalize m q x) := by rcases h with ⟨huv, hrs, huniq⟩ constructor · exact (collinear_baseNormalize_iff hqm).2 huv constructor · exact (collinear_baseNormalize_iff hqm).2 hrs · intro z hz_uv hz_rs rcases baseNormalize_surjective hqm z with ⟨z0, rfl⟩ have hz_uv0 : Collinear u v z0 := (collinear_baseNormalize_iff hqm).1 hz_uv have hz_rs0 : Collinear r s z0 := (collinear_baseNormalize_iff hqm).1 hz_rs rw [huniq z0 hz_uv0 hz_rs0] theorem baseNormalize_self (m q : Point) : baseNormalize m q m = point 0 0 := by ext i fin_cases i <;> simp [baseNormalize, baseCoord, dot2, det2, sqNorm, vsub, point] theorem baseNormalize_right {m q : Point} (hqm : q ≠ m) : baseNormalize m q q = point 1 0 := by have hden : sqNorm (vsub q m) ≠ 0 := sqNorm_vsub_ne_zero_of_ne hqm ext i fin_cases i · change dot2 (vsub q m) (vsub q m) / sqNorm (vsub q m) = 1 rw [dot2_self] exact div_self hden · change det2 (vsub q m) (vsub q m) / sqNorm (vsub q m) = 0 rw [det2_self] simp theorem right_ne_midpoint_of_left_ne_right {m p q : Point} (hmid : IsMidpoint m p q) (hpq : p ≠ q) : q ≠ m := by intro hqm apply hpq unfold IsMidpoint midpoint at hmid ext i have hi := congrFun hmid i rw [← hqm] at hi nlinarith theorem baseNormalize_left_of_midpoint {m p q : Point} (hmid : IsMidpoint m p q) (hpq : p ≠ q) : baseNormalize m q p = point (-1) 0 := by have hqm : q ≠ m := right_ne_midpoint_of_left_ne_right hmid hpq have hden : sqNorm (vsub q m) ≠ 0 := sqNorm_vsub_ne_zero_of_ne hqm unfold IsMidpoint midpoint at hmid have hm0 := congrFun hmid 0 have hm1 := congrFun hmid 1 have hleft0 : p 0 - m 0 = -(q 0 - m 0) := by nlinarith have hleft1 : p 1 - m 1 = -(q 1 - m 1) := by nlinarith have hdot : dot2 (vsub p m) (vsub q m) = -sqNorm (vsub q m) := by unfold dot2 sqNorm vsub rw [hleft0, hleft1] ring have hdet : det2 (vsub q m) (vsub p m) = 0 := by unfold det2 vsub rw [hleft0, hleft1] ring ext i fin_cases i · change dot2 (vsub p m) (vsub q m) / sqNorm (vsub q m) = -1 rw [hdot] field_simp [hden] · change det2 (vsub q m) (vsub p m) / sqNorm (vsub q m) = 0 rw [hdet] simp theorem dot2_center_vsub_midpoint_right_eq_zero {o m p q : Point} {R : ℝ} (hp : OnCircleSq o R p) (hq : OnCircleSq o R q) (hmid : IsMidpoint m p q) : dot2 (vsub o m) (vsub q m) = 0 := by unfold OnCircleSq sqDist sqNorm vsub at hp hq unfold IsMidpoint midpoint at hmid have hm0 := congrFun hmid 0 have hm1 := congrFun hmid 1 have hdist : ((q 0 - o 0) ^ 2 + (q 1 - o 1) ^ 2) - ((p 0 - o 0) ^ 2 + (p 1 - o 1) ^ 2) = 0 := by rw [hq, hp] ring have hscaled : 4 * ((o 0 - m 0) * (q 0 - m 0) + (o 1 - m 1) * (q 1 - m 1)) = -(((q 0 - o 0) ^ 2 + (q 1 - o 1) ^ 2) - ((p 0 - o 0) ^ 2 + (p 1 - o 1) ^ 2)) := by rw [hm0, hm1] ring unfold dot2 vsub nlinarith theorem baseNormalize_center_x_eq_zero {o m p q : Point} {R : ℝ} (hp : OnCircleSq o R p) (hq : OnCircleSq o R q) (hmid : IsMidpoint m p q) : (baseNormalize m q o) 0 = 0 := by have hdot := dot2_center_vsub_midpoint_right_eq_zero hp hq hmid simp [baseNormalize, baseCoord, point, hdot] theorem baseNormalize_center_eq_point {o m p q : Point} {R : ℝ} (hp : OnCircleSq o R p) (hq : OnCircleSq o R q) (hmid : IsMidpoint m p q) : baseNormalize m q o = point 0 ((baseNormalize m q o) 1) := by ext i fin_cases i · exact baseNormalize_center_x_eq_zero hp hq hmid · simp [point] theorem onCircleSq_point_one_zero_radius {k R : ℝ} (h : OnCircleSq (point 0 k) R (point 1 0)) : R = 1 ^ 2 + k ^ 2 := by unfold OnCircleSq sqDist sqNorm vsub point at h norm_num at h nlinarith theorem onCircleSq_baseNormalize_normalized {o m p q z : Point} {R : ℝ} (hqm : q ≠ m) (hmid : IsMidpoint m p q) (hp : OnCircleSq o R p) (hq : OnCircleSq o R q) (hz : OnCircleSq o R z) : OnCircleSq (point 0 ((baseNormalize m q o) 1)) (1 ^ 2 + ((baseNormalize m q o) 1) ^ 2) (baseNormalize m q z) := by have hcenter : point 0 ((baseNormalize m q o) 1) = baseNormalize m q o := by ext i fin_cases i · simp [point, baseNormalize_center_x_eq_zero hp hq hmid] · simp [point] have hz' := onCircleSq_baseNormalize hqm hz have hq' := onCircleSq_baseNormalize hqm hq have hq_img := baseNormalize_right hqm have hradius : R / sqNorm (vsub q m) = 1 ^ 2 + ((baseNormalize m q o) 1) ^ 2 := by have hq_on : OnCircleSq (point 0 ((baseNormalize m q o) 1)) (R / sqNorm (vsub q m)) (point 1 0) := by rw [hcenter, ← hq_img] exact hq' exact onCircleSq_point_one_zero_radius hq_on rw [hcenter, ← hradius] exact hz' theorem collinear_refl_left (p q : Point) : Collinear p p q := by simp [Collinear, det2, vsub] theorem collinear_swap {p q r : Point} (h : Collinear p q r) : Collinear q p r := by unfold Collinear det2 vsub at * nlinarith theorem collinear_origin_finite_slope {u y v z : ℝ} (hu : u ≠ 0) (h : Collinear (point u y) (point 0 0) (point v z)) : z = (y / u) * v := by unfold Collinear det2 vsub point at h norm_num at h field_simp [hu] nlinarith theorem finite_slope_x_ne_of_point_ne {u y v z : ℝ} (hu : u ≠ 0) (hcol : Collinear (point u y) (point 0 0) (point v z)) (hne : point u y ≠ point v z) : u ≠ v := by intro huv have hz : z = y := by have hslope := collinear_origin_finite_slope hu hcol rw [huv] at hslope have hv : v ≠ 0 := by rwa [← huv] field_simp [hv] at hslope exact hslope apply hne ext i fin_cases i · simp [point, huv] · simp [point, hz] theorem collinear_origin_vertical_x_eq_zero {s v z : ℝ} (hs : s ≠ 0) (h : Collinear (point 0 s) (point 0 0) (point v z)) : v = 0 := by unfold Collinear det2 vsub point at h norm_num at h exact Or.resolve_left h hs theorem vertical_y_ne_of_point_ne {s v z : ℝ} (hs : s ≠ 0) (hcol : Collinear (point 0 s) (point 0 0) (point v z)) (hne : point 0 s ≠ point v z) : s ≠ z := by intro hsz have hv := collinear_origin_vertical_x_eq_zero hs hcol apply hne ext i fin_cases i · simp [point, hv] · simp [point, hsz] theorem collinear_origin_finite_slope_point {p q : Point} (hp : p 0 ≠ 0) (h : Collinear p (point 0 0) q) : q 1 = (p 1 / p 0) * q 0 := by have hpoint : Collinear (point (p 0) (p 1)) (point 0 0) (point (q 0) (q 1)) := by simpa [point_eta] using h exact collinear_origin_finite_slope hp hpoint theorem finite_slope_x_ne_of_point_ne_point {p q : Point} (hp : p 0 ≠ 0) (hcol : Collinear p (point 0 0) q) (hne : p ≠ q) : p 0 ≠ q 0 := by have hpoint : Collinear (point (p 0) (p 1)) (point 0 0) (point (q 0) (q 1)) := by simpa [point_eta] using hcol exact finite_slope_x_ne_of_point_ne hp hpoint (by simpa [point_eta] using hne) theorem collinear_origin_vertical_x_eq_zero_point {p q : Point} (hp0 : p 0 = 0) (hp1 : p 1 ≠ 0) (h : Collinear p (point 0 0) q) : q 0 = 0 := by have hp_eq : p = point 0 (p 1) := by ext i fin_cases i <;> simp [point, hp0] have hpoint : Collinear (point 0 (p 1)) (point 0 0) (point (q 0) (q 1)) := by rw [← hp_eq, point_eta q] exact h exact collinear_origin_vertical_x_eq_zero hp1 hpoint theorem vertical_y_ne_of_point_ne_point {p q : Point} (hp0 : p 0 = 0) (hp1 : p 1 ≠ 0) (hcol : Collinear p (point 0 0) q) (hne : p ≠ q) : p 1 ≠ q 1 := by have hp_eq : p = point 0 (p 1) := by ext i fin_cases i <;> simp [point, hp0] have hpoint : Collinear (point 0 (p 1)) (point 0 0) (point (q 0) (q 1)) := by rw [← hp_eq, point_eta q] exact hcol have hnepoint : point 0 (p 1) ≠ point (q 0) (q 1) := by intro hpq apply hne rw [hp_eq, ← point_eta q] exact hpq exact vertical_y_ne_of_point_ne hp1 hpoint hnepoint /-- Checked statement wrapper for the minimum theorem. -/ theorem butterflyTheorem_statement : ButterflyTheoremStatement ↔ ButterflyTheoremStatement := by rfl theorem secant_parameter_sum_prod {a k m u v : ℝ} (hu : (1 + m ^ 2) * u ^ 2 - 2 * m * k * u - a ^ 2 = 0) (hv : (1 + m ^ 2) * v ^ 2 - 2 * m * k * v - a ^ 2 = 0) (huv : u ≠ v) : (1 + m ^ 2) * (u + v) = 2 * m * k ∧ (1 + m ^ 2) * (u * v) = -a ^ 2 := by have hsub : (u - v) * ((1 + m ^ 2) * (u + v) - 2 * m * k) = 0 := by calc (u - v) * ((1 + m ^ 2) * (u + v) - 2 * m * k) = ((1 + m ^ 2) * u ^ 2 - 2 * m * k * u - a ^ 2) - ((1 + m ^ 2) * v ^ 2 - 2 * m * k * v - a ^ 2) := by ring _ = 0 := by rw [hu, hv]; ring have hsum_zero : (1 + m ^ 2) * (u + v) - 2 * m * k = 0 := Or.resolve_left (mul_eq_zero.mp hsub) (sub_ne_zero.mpr huv) constructor · nlinarith · have hprod_zero : (1 + m ^ 2) * (u * v) + a ^ 2 = 0 := by have hcalc : -((1 + m ^ 2) * (u * v) + a ^ 2) = ((1 + m ^ 2) * u ^ 2 - 2 * m * k * u - a ^ 2) - (((1 + m ^ 2) * (u + v) - 2 * m * k) * u) := by ring rw [hu, hsum_zero] at hcalc nlinarith nlinarith theorem base_line_intersection_formula {m n u w x : ℝ} (h : Collinear (point u (m * u)) (point w (n * w)) (point x 0)) : x * (n * w - m * u) = u * w * (n - m) := by unfold Collinear det2 vsub point at h norm_num at h nlinarith theorem collinear_base_y_eq_zero {a : ℝ} {z : Point} (ha : a ≠ 0) (h : Collinear (point (-a) 0) (point a 0) z) : z 1 = 0 := by unfold Collinear det2 vsub point at h norm_num at h exact Or.resolve_left h ha theorem collinear_same_y_of_base_point {r s x z : Point} (hy : r 1 = s 1) (hx_y : x 1 = 0) (hz_y : z 1 = 0) (hcol : Collinear r s x) : Collinear r s z := by unfold Collinear det2 vsub at * rw [hy, hx_y] at hcol rw [hy, hz_y] nlinarith theorem unique_intersection_base_not_same_y {a : ℝ} {r s x : Point} (ha : a ≠ 0) (huniq : UniqueIntersection (point (-a) 0) (point a 0) r s x) : r 1 ≠ s 1 := by intro hy have hx_y : x 1 = 0 := collinear_base_y_eq_zero ha huniq.1 have hp_base : Collinear (point (-a) 0) (point a 0) (point (-a) 0) := by norm_num [Collinear, det2, vsub, point] have hq_base : Collinear (point (-a) 0) (point a 0) (point a 0) := by norm_num [Collinear, det2, vsub, point] have hp_rs : Collinear r s (point (-a) 0) := collinear_same_y_of_base_point hy hx_y (by simp [point]) huniq.2.1 have hq_rs : Collinear r s (point a 0) := collinear_same_y_of_base_point hy hx_y (by simp [point]) huniq.2.1 have hp_eq := huniq.2.2 (point (-a) 0) hp_base hp_rs have hq_eq := huniq.2.2 (point a 0) hq_base hq_rs have hpq : point (-a) 0 = point a 0 := hp_eq.trans hq_eq.symm have h0 := congrFun hpq 0 norm_num [point] at h0 exact ha (by nlinarith) theorem unique_intersection_base_finite_finite_den_ne {a m n u w x : ℝ} (ha : a ≠ 0) (huniq : UniqueIntersection (point (-a) 0) (point a 0) (point u (m * u)) (point w (n * w)) (point x 0)) : n * w - m * u ≠ 0 := by intro hden have hy := unique_intersection_base_not_same_y ha huniq apply hy simp [point] nlinarith theorem unique_intersection_base_vertical_finite_den_ne {a n s w x : ℝ} (ha : a ≠ 0) (huniq : UniqueIntersection (point (-a) 0) (point a 0) (point 0 s) (point w (n * w)) (point x 0)) : n * w - s ≠ 0 := by intro hden have hy := unique_intersection_base_not_same_y ha huniq apply hy simp [point] nlinarith theorem unique_intersection_base_finite_vertical_den_ne {a m u t x : ℝ} (ha : a ≠ 0) (huniq : UniqueIntersection (point (-a) 0) (point a 0) (point u (m * u)) (point 0 t) (point x 0)) : m * u - t ≠ 0 := by intro hden have hy := unique_intersection_base_not_same_y ha huniq apply hy simp [point] nlinarith theorem unique_intersection_base_vertical_vertical_y_ne {a s w x : ℝ} (ha : a ≠ 0) (huniq : UniqueIntersection (point (-a) 0) (point a 0) (point 0 s) (point 0 w) (point x 0)) : s ≠ w := by intro hsw have hy := unique_intersection_base_not_same_y ha huniq apply hy simp [point, hsw] theorem base_line_intersection_formula_of_y_eq_zero {m n u w : ℝ} {z : Point} (hz_y : z 1 = 0) (h : Collinear (point u (m * u)) (point w (n * w)) z) : z 0 * (n * w - m * u) = u * w * (n - m) := by unfold Collinear det2 vsub point at h norm_num at h rw [hz_y] at h nlinarith theorem normalized_base_intersection_unique {a m n u w x : ℝ} {z : Point} (ha : a ≠ 0) (hden : n * w - m * u ≠ 0) (hx_col : Collinear (point u (m * u)) (point w (n * w)) (point x 0)) (hz_base : Collinear (point (-a) 0) (point a 0) z) (hz_secant : Collinear (point u (m * u)) (point w (n * w)) z) : z = point x 0 := by have hz_y : z 1 = 0 := collinear_base_y_eq_zero ha hz_base have hz_formula := base_line_intersection_formula_of_y_eq_zero hz_y hz_secant have hx_formula := base_line_intersection_formula hx_col have hmul : (z 0 - x) * (n * w - m * u) = 0 := by nlinarith have hdiff : z 0 - x = 0 := Or.resolve_right (mul_eq_zero.mp hmul) hden ext i fin_cases i · simp [point] nlinarith · simpa [point] using hz_y theorem normalized_circle_equation {a k m u : ℝ} : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point u (m * u)) ↔ (1 + m ^ 2) * u ^ 2 - 2 * m * k * u - a ^ 2 = 0 := by unfold OnCircleSq sqDist sqNorm vsub point norm_num constructor <;> intro h <;> nlinarith theorem butterfly_algebra_core {a k m n u v r w x y : ℝ} (hab_sum : (1 + m ^ 2) * (u + v) = 2 * m * k) (hab_prod : (1 + m ^ 2) * (u * v) = -a ^ 2) (hcd_sum : (1 + n ^ 2) * (r + w) = 2 * n * k) (hcd_prod : (1 + n ^ 2) * (r * w) = -a ^ 2) (hx_den : n * w - m * u ≠ 0) (hy_den : n * r - m * v ≠ 0) (hx : x * (n * w - m * u) = u * w * (n - m)) (hy : y * (n * r - m * v) = v * r * (n - m)) : x + y = 0 := by have hm_ne : 1 + m ^ 2 ≠ 0 := by positivity have hn_ne : 1 + n ^ 2 ≠ 0 := by positivity have hcore : r * w * n * (u + v) - u * v * m * (r + w) = 0 := by have hscaled : (1 + m ^ 2) * (1 + n ^ 2) * (r * w * n * (u + v) - u * v * m * (r + w)) = 0 := by calc (1 + m ^ 2) * (1 + n ^ 2) * (r * w * n * (u + v) - u * v * m * (r + w)) = (1 + n ^ 2) * (r * w) * n * ((1 + m ^ 2) * (u + v)) - (1 + m ^ 2) * (u * v) * m * ((1 + n ^ 2) * (r + w)) := by ring _ = 0 := by rw [hab_sum, hab_prod, hcd_sum, hcd_prod] ring exact Or.resolve_left (mul_eq_zero.mp hscaled) (mul_ne_zero hm_ne hn_ne) have hnum : u * w * (n - m) * (n * r - m * v) + v * r * (n - m) * (n * w - m * u) = 0 := by calc u * w * (n - m) * (n * r - m * v) + v * r * (n - m) * (n * w - m * u) = (n - m) * (r * w * n * (u + v) - u * v * m * (r + w)) := by ring _ = 0 := by rw [hcore, mul_zero] have hmul : (x + y) * ((n * w - m * u) * (n * r - m * v)) = 0 := by calc (x + y) * ((n * w - m * u) * (n * r - m * v)) = x * (n * w - m * u) * (n * r - m * v) + y * (n * r - m * v) * (n * w - m * u) := by ring _ = u * w * (n - m) * (n * r - m * v) + v * r * (n - m) * (n * w - m * u) := by rw [hx, hy] _ = 0 := hnum exact Or.resolve_right (mul_eq_zero.mp hmul) (mul_ne_zero hx_den hy_den) theorem normalized_butterfly_algebra {a k m n u v r w x y : ℝ} (hu : (1 + m ^ 2) * u ^ 2 - 2 * m * k * u - a ^ 2 = 0) (hv : (1 + m ^ 2) * v ^ 2 - 2 * m * k * v - a ^ 2 = 0) (hr : (1 + n ^ 2) * r ^ 2 - 2 * n * k * r - a ^ 2 = 0) (hw : (1 + n ^ 2) * w ^ 2 - 2 * n * k * w - a ^ 2 = 0) (huv : u ≠ v) (hrw : r ≠ w) (hx_den : n * w - m * u ≠ 0) (hy_den : n * r - m * v ≠ 0) (hx_col : Collinear (point u (m * u)) (point w (n * w)) (point x 0)) (hy_col : Collinear (point v (m * v)) (point r (n * r)) (point y 0)) : x + y = 0 := by have hab := secant_parameter_sum_prod hu hv huv have hcd := secant_parameter_sum_prod hr hw hrw exact butterfly_algebra_core hab.1 hab.2 hcd.1 hcd.2 hx_den hy_den (base_line_intersection_formula hx_col) (base_line_intersection_formula hy_col) theorem normalized_butterfly_from_circle {a k m n u v r w x y : ℝ} (hu : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point u (m * u))) (hv : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point v (m * v))) (hr : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point r (n * r))) (hw : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point w (n * w))) (huv : u ≠ v) (hrw : r ≠ w) (hx_den : n * w - m * u ≠ 0) (hy_den : n * r - m * v ≠ 0) (hx_col : Collinear (point u (m * u)) (point w (n * w)) (point x 0)) (hy_col : Collinear (point v (m * v)) (point r (n * r)) (point y 0)) : x + y = 0 := by exact normalized_butterfly_algebra (normalized_circle_equation.mp hu) (normalized_circle_equation.mp hv) (normalized_circle_equation.mp hr) (normalized_circle_equation.mp hw) huv hrw hx_den hy_den hx_col hy_col theorem x_axis_midpoint_of_add_eq_zero {x y : ℝ} (h : x + y = 0) : IsMidpoint (point 0 0) (point x 0) (point y 0) := by unfold IsMidpoint midpoint point ext i fin_cases i · norm_num nlinarith · norm_num theorem normalized_butterfly_midpoint_from_circle {a k m n u v r w x y : ℝ} (hu : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point u (m * u))) (hv : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point v (m * v))) (hr : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point r (n * r))) (hw : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point w (n * w))) (huv : u ≠ v) (hrw : r ≠ w) (hx_den : n * w - m * u ≠ 0) (hy_den : n * r - m * v ≠ 0) (hx_col : Collinear (point u (m * u)) (point w (n * w)) (point x 0)) (hy_col : Collinear (point v (m * v)) (point r (n * r)) (point y 0)) : IsMidpoint (point 0 0) (point x 0) (point y 0) := x_axis_midpoint_of_add_eq_zero (normalized_butterfly_from_circle hu hv hr hw huv hrw hx_den hy_den hx_col hy_col) theorem vertical_parameter_sum_prod {a k s t : ℝ} (hs : s ^ 2 - 2 * k * s - a ^ 2 = 0) (ht : t ^ 2 - 2 * k * t - a ^ 2 = 0) (hst : s ≠ t) : s + t = 2 * k ∧ s * t = -a ^ 2 := by have hsub : (s - t) * ((s + t) - 2 * k) = 0 := by calc (s - t) * ((s + t) - 2 * k) = (s ^ 2 - 2 * k * s - a ^ 2) - (t ^ 2 - 2 * k * t - a ^ 2) := by ring _ = 0 := by rw [hs, ht]; ring have hsum_zero : (s + t) - 2 * k = 0 := Or.resolve_left (mul_eq_zero.mp hsub) (sub_ne_zero.mpr hst) constructor · nlinarith · have hprod_zero : s * t + a ^ 2 = 0 := by have hcalc : -(s * t + a ^ 2) = (s ^ 2 - 2 * k * s - a ^ 2) - (((s + t) - 2 * k) * s) := by ring rw [hs, hsum_zero] at hcalc nlinarith nlinarith theorem vertical_base_intersection_formula {n s w x : ℝ} (h : Collinear (point 0 s) (point w (n * w)) (point x 0)) : x * (n * w - s) = -s * w := by unfold Collinear det2 vsub point at h norm_num at h nlinarith theorem vertical_base_intersection_formula_of_y_eq_zero {n s w : ℝ} {z : Point} (hz_y : z 1 = 0) (h : Collinear (point 0 s) (point w (n * w)) z) : z 0 * (n * w - s) = -s * w := by unfold Collinear det2 vsub point at h norm_num at h rw [hz_y] at h nlinarith theorem vertical_base_intersection_unique {a n s w x : ℝ} {z : Point} (ha : a ≠ 0) (hden : n * w - s ≠ 0) (hx_col : Collinear (point 0 s) (point w (n * w)) (point x 0)) (hz_base : Collinear (point (-a) 0) (point a 0) z) (hz_secant : Collinear (point 0 s) (point w (n * w)) z) : z = point x 0 := by have hz_y : z 1 = 0 := collinear_base_y_eq_zero ha hz_base have hz_formula := vertical_base_intersection_formula_of_y_eq_zero hz_y hz_secant have hx_formula := vertical_base_intersection_formula hx_col have hmul : (z 0 - x) * (n * w - s) = 0 := by nlinarith have hdiff : z 0 - x = 0 := Or.resolve_right (mul_eq_zero.mp hmul) hden ext i fin_cases i · simp [point] nlinarith · simpa [point] using hz_y theorem vertical_line_x_eq_zero {s w : ℝ} {z : Point} (hsw : s ≠ w) (h : Collinear (point 0 s) (point 0 w) z) : z 0 = 0 := by unfold Collinear det2 vsub point at h norm_num at h exact Or.resolve_left h (sub_ne_zero.mpr (Ne.symm hsw)) theorem vertical_line_base_intersection_zero {s w x : ℝ} (hsw : s ≠ w) (h : Collinear (point 0 s) (point 0 w) (point x 0)) : x = 0 := by have hx := vertical_line_x_eq_zero (z := point x 0) hsw h simpa [point] using hx theorem vertical_line_base_intersection_unique {a s w x : ℝ} {z : Point} (ha : a ≠ 0) (hsw : s ≠ w) (hx_col : Collinear (point 0 s) (point 0 w) (point x 0)) (hz_base : Collinear (point (-a) 0) (point a 0) z) (hz_secant : Collinear (point 0 s) (point 0 w) z) : z = point x 0 := by have hz_y : z 1 = 0 := collinear_base_y_eq_zero ha hz_base have hz_x : z 0 = 0 := vertical_line_x_eq_zero hsw hz_secant have hx0 : x = 0 := vertical_line_base_intersection_zero hsw hx_col ext i fin_cases i · simp [point] rw [hz_x, hx0] · simpa [point] using hz_y theorem vertical_circle_equation {a k s : ℝ} : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s) ↔ s ^ 2 - 2 * k * s - a ^ 2 = 0 := by unfold OnCircleSq sqDist sqNorm vsub point norm_num constructor <;> intro h <;> nlinarith theorem vertical_coord_ne_zero_of_on_normalized_circle {a k s : ℝ} (ha : a ≠ 0) (h : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s)) : s ≠ 0 := by intro hs have hquad := vertical_circle_equation.mp h rw [hs] at hquad norm_num at hquad have hsqa : a ^ 2 = 0 := by nlinarith exact ha (sq_eq_zero_iff.mp hsqa) theorem vertical_butterfly_algebra_core {a k n s t r w x y : ℝ} (hab_sum : s + t = 2 * k) (hab_prod : s * t = -a ^ 2) (hcd_sum : (1 + n ^ 2) * (r + w) = 2 * n * k) (hcd_prod : (1 + n ^ 2) * (r * w) = -a ^ 2) (hx_den : n * w - s ≠ 0) (hy_den : n * r - t ≠ 0) (hx : x * (n * w - s) = -s * w) (hy : y * (n * r - t) = -t * r) : x + y = 0 := by have hn_ne : 1 + n ^ 2 ≠ 0 := by positivity have hcore : n * (r * w) * (s + t) - (s * t) * (r + w) = 0 := by have hscaled : (1 + n ^ 2) * (n * (r * w) * (s + t) - (s * t) * (r + w)) = 0 := by calc (1 + n ^ 2) * (n * (r * w) * (s + t) - (s * t) * (r + w)) = n * ((1 + n ^ 2) * (r * w)) * (s + t) - (s * t) * ((1 + n ^ 2) * (r + w)) := by ring _ = 0 := by rw [hcd_prod, hcd_sum, hab_sum, hab_prod] ring exact Or.resolve_left (mul_eq_zero.mp hscaled) hn_ne have hnum : (-s * w) * (n * r - t) + (-t * r) * (n * w - s) = 0 := by calc (-s * w) * (n * r - t) + (-t * r) * (n * w - s) = -(n * (r * w) * (s + t) - (s * t) * (r + w)) := by ring _ = 0 := by rw [hcore]; ring have hmul : (x + y) * ((n * w - s) * (n * r - t)) = 0 := by calc (x + y) * ((n * w - s) * (n * r - t)) = x * (n * w - s) * (n * r - t) + y * (n * r - t) * (n * w - s) := by ring _ = (-s * w) * (n * r - t) + (-t * r) * (n * w - s) := by rw [hx, hy] _ = 0 := hnum exact Or.resolve_right (mul_eq_zero.mp hmul) (mul_ne_zero hx_den hy_den) theorem vertical_butterfly_algebra {a k n s t r w x y : ℝ} (hs : s ^ 2 - 2 * k * s - a ^ 2 = 0) (ht : t ^ 2 - 2 * k * t - a ^ 2 = 0) (hr : (1 + n ^ 2) * r ^ 2 - 2 * n * k * r - a ^ 2 = 0) (hw : (1 + n ^ 2) * w ^ 2 - 2 * n * k * w - a ^ 2 = 0) (hst : s ≠ t) (hrw : r ≠ w) (hx_den : n * w - s ≠ 0) (hy_den : n * r - t ≠ 0) (hx_col : Collinear (point 0 s) (point w (n * w)) (point x 0)) (hy_col : Collinear (point 0 t) (point r (n * r)) (point y 0)) : x + y = 0 := by have hab := vertical_parameter_sum_prod hs ht hst have hcd := secant_parameter_sum_prod hr hw hrw exact vertical_butterfly_algebra_core hab.1 hab.2 hcd.1 hcd.2 hx_den hy_den (vertical_base_intersection_formula hx_col) (vertical_base_intersection_formula hy_col) theorem vertical_butterfly_from_circle {a k n s t r w x y : ℝ} (hs : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s)) (ht : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 t)) (hr : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point r (n * r))) (hw : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point w (n * w))) (hst : s ≠ t) (hrw : r ≠ w) (hx_den : n * w - s ≠ 0) (hy_den : n * r - t ≠ 0) (hx_col : Collinear (point 0 s) (point w (n * w)) (point x 0)) (hy_col : Collinear (point 0 t) (point r (n * r)) (point y 0)) : x + y = 0 := by exact vertical_butterfly_algebra (vertical_circle_equation.mp hs) (vertical_circle_equation.mp ht) (normalized_circle_equation.mp hr) (normalized_circle_equation.mp hw) hst hrw hx_den hy_den hx_col hy_col theorem vertical_butterfly_midpoint_from_circle {a k n s t r w x y : ℝ} (hs : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s)) (ht : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 t)) (hr : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point r (n * r))) (hw : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point w (n * w))) (hst : s ≠ t) (hrw : r ≠ w) (hx_den : n * w - s ≠ 0) (hy_den : n * r - t ≠ 0) (hx_col : Collinear (point 0 s) (point w (n * w)) (point x 0)) (hy_col : Collinear (point 0 t) (point r (n * r)) (point y 0)) : IsMidpoint (point 0 0) (point x 0) (point y 0) := x_axis_midpoint_of_add_eq_zero (vertical_butterfly_from_circle hs ht hr hw hst hrw hx_den hy_den hx_col hy_col) theorem reverse_vertical_butterfly_midpoint_from_circle {a k m u v s t x y : ℝ} (hu : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point u (m * u))) (hv : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point v (m * v))) (hs : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s)) (ht : OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 t)) (huv : u ≠ v) (hst : s ≠ t) (hx_den : m * u - t ≠ 0) (hy_den : m * v - s ≠ 0) (hx_col : Collinear (point u (m * u)) (point 0 t) (point x 0)) (hy_col : Collinear (point v (m * v)) (point 0 s) (point y 0)) : IsMidpoint (point 0 0) (point x 0) (point y 0) := vertical_butterfly_midpoint_from_circle (a := a) (k := k) (n := m) (s := t) (t := s) (r := v) (w := u) ht hs hv hu (Ne.symm hst) (Ne.symm huv) hx_den hy_den (collinear_swap hx_col) (collinear_swap hy_col) theorem both_vertical_butterfly_midpoint_from_collinear {s t r w x y : ℝ} (hsw : s ≠ w) (htr : t ≠ r) (hx_col : Collinear (point 0 s) (point 0 w) (point x 0)) (hy_col : Collinear (point 0 t) (point 0 r) (point y 0)) : IsMidpoint (point 0 0) (point x 0) (point y 0) := by have hx0 := vertical_line_base_intersection_zero hsw hx_col have hy0 := vertical_line_base_intersection_zero htr hy_col apply x_axis_midpoint_of_add_eq_zero nlinarith def VerticalNormalizedButterflyTheoremStatement : Prop := ∀ a k n s t r w x y : ℝ, OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 t) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point r (n * r)) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point w (n * w)) → s ≠ t → r ≠ w → n * w - s ≠ 0 → n * r - t ≠ 0 → Collinear (point 0 s) (point w (n * w)) (point x 0) → Collinear (point 0 t) (point r (n * r)) (point y 0) → IsMidpoint (point 0 0) (point x 0) (point y 0) theorem verticalNormalizedButterflyTheorem : VerticalNormalizedButterflyTheoremStatement := by intro a k n s t r w x y hs ht hr hw hst hrw hx_den hy_den hx_col hy_col exact vertical_butterfly_midpoint_from_circle hs ht hr hw hst hrw hx_den hy_den hx_col hy_col def ReverseVerticalNormalizedButterflyTheoremStatement : Prop := ∀ a k m u v s t x y : ℝ, OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point u (m * u)) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point v (m * v)) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 t) → u ≠ v → s ≠ t → m * u - t ≠ 0 → m * v - s ≠ 0 → Collinear (point u (m * u)) (point 0 t) (point x 0) → Collinear (point v (m * v)) (point 0 s) (point y 0) → IsMidpoint (point 0 0) (point x 0) (point y 0) theorem reverseVerticalNormalizedButterflyTheorem : ReverseVerticalNormalizedButterflyTheoremStatement := by intro a k m u v s t x y hu hv hs ht huv hst hx_den hy_den hx_col hy_col exact reverse_vertical_butterfly_midpoint_from_circle hu hv hs ht huv hst hx_den hy_den hx_col hy_col def BothVerticalNormalizedButterflyTheoremStatement : Prop := ∀ a k s t r w x y : ℝ, OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 s) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 t) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 r) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point 0 w) → s ≠ t → r ≠ w → s ≠ w → t ≠ r → Collinear (point 0 s) (point 0 w) (point x 0) → Collinear (point 0 t) (point 0 r) (point y 0) → IsMidpoint (point 0 0) (point x 0) (point y 0) theorem bothVerticalNormalizedButterflyTheorem : BothVerticalNormalizedButterflyTheoremStatement := by intro a k s t r w x y _hs _ht _hr _hw _hst _hrw hsw htr hx_col hy_col exact both_vertical_butterfly_midpoint_from_collinear hsw htr hx_col hy_col structure VerticalNormalizedButterflyConfiguration where a : ℝ k : ℝ n : ℝ s : ℝ t : ℝ r : ℝ w : ℝ x : ℝ y : ℝ def VerticalNormalizedButterflyHyp (cfg : VerticalNormalizedButterflyConfiguration) : Prop := OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.s) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.t) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.r (cfg.n * cfg.r)) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.w (cfg.n * cfg.w)) ∧ cfg.s ≠ cfg.t ∧ cfg.r ≠ cfg.w ∧ cfg.n * cfg.w - cfg.s ≠ 0 ∧ cfg.n * cfg.r - cfg.t ≠ 0 ∧ Collinear (point 0 cfg.s) (point cfg.w (cfg.n * cfg.w)) (point cfg.x 0) ∧ Collinear (point 0 cfg.t) (point cfg.r (cfg.n * cfg.r)) (point cfg.y 0) def VerticalNormalizedButterflyConclusion (cfg : VerticalNormalizedButterflyConfiguration) : Prop := IsMidpoint (point 0 0) (point cfg.x 0) (point cfg.y 0) def VerticalNormalizedButterflyConfigurationStatement : Prop := ∀ cfg : VerticalNormalizedButterflyConfiguration, VerticalNormalizedButterflyHyp cfg → VerticalNormalizedButterflyConclusion cfg theorem verticalNormalizedButterflyTheorem_config : VerticalNormalizedButterflyConfigurationStatement := by intro cfg hcfg rcases hcfg with ⟨hs, ht, hr, hw, hst, hrw, hx_den, hy_den, hx_col, hy_col⟩ exact vertical_butterfly_midpoint_from_circle hs ht hr hw hst hrw hx_den hy_den hx_col hy_col structure ReverseVerticalNormalizedButterflyConfiguration where a : ℝ k : ℝ m : ℝ u : ℝ v : ℝ s : ℝ t : ℝ x : ℝ y : ℝ def ReverseVerticalNormalizedButterflyHyp (cfg : ReverseVerticalNormalizedButterflyConfiguration) : Prop := OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.u (cfg.m * cfg.u)) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.v (cfg.m * cfg.v)) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.s) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.t) ∧ cfg.u ≠ cfg.v ∧ cfg.s ≠ cfg.t ∧ cfg.m * cfg.u - cfg.t ≠ 0 ∧ cfg.m * cfg.v - cfg.s ≠ 0 ∧ Collinear (point cfg.u (cfg.m * cfg.u)) (point 0 cfg.t) (point cfg.x 0) ∧ Collinear (point cfg.v (cfg.m * cfg.v)) (point 0 cfg.s) (point cfg.y 0) def ReverseVerticalNormalizedButterflyConclusion (cfg : ReverseVerticalNormalizedButterflyConfiguration) : Prop := IsMidpoint (point 0 0) (point cfg.x 0) (point cfg.y 0) def ReverseVerticalNormalizedButterflyConfigurationStatement : Prop := ∀ cfg : ReverseVerticalNormalizedButterflyConfiguration, ReverseVerticalNormalizedButterflyHyp cfg → ReverseVerticalNormalizedButterflyConclusion cfg theorem reverseVerticalNormalizedButterflyTheorem_config : ReverseVerticalNormalizedButterflyConfigurationStatement := by intro cfg hcfg rcases hcfg with ⟨hu, hv, hs, ht, huv, hst, hx_den, hy_den, hx_col, hy_col⟩ exact reverse_vertical_butterfly_midpoint_from_circle hu hv hs ht huv hst hx_den hy_den hx_col hy_col structure BothVerticalNormalizedButterflyConfiguration where a : ℝ k : ℝ s : ℝ t : ℝ r : ℝ w : ℝ x : ℝ y : ℝ def BothVerticalNormalizedButterflyHyp (cfg : BothVerticalNormalizedButterflyConfiguration) : Prop := OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.s) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.t) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.r) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point 0 cfg.w) ∧ cfg.s ≠ cfg.t ∧ cfg.r ≠ cfg.w ∧ cfg.s ≠ cfg.w ∧ cfg.t ≠ cfg.r ∧ Collinear (point 0 cfg.s) (point 0 cfg.w) (point cfg.x 0) ∧ Collinear (point 0 cfg.t) (point 0 cfg.r) (point cfg.y 0) def BothVerticalNormalizedButterflyConclusion (cfg : BothVerticalNormalizedButterflyConfiguration) : Prop := IsMidpoint (point 0 0) (point cfg.x 0) (point cfg.y 0) def BothVerticalNormalizedButterflyConfigurationStatement : Prop := ∀ cfg : BothVerticalNormalizedButterflyConfiguration, BothVerticalNormalizedButterflyHyp cfg → BothVerticalNormalizedButterflyConclusion cfg theorem bothVerticalNormalizedButterflyTheorem_config : BothVerticalNormalizedButterflyConfigurationStatement := by intro cfg hcfg rcases hcfg with ⟨_hs, _ht, _hr, _hw, _hst, _hrw, hsw, htr, hx_col, hy_col⟩ exact both_vertical_butterfly_midpoint_from_collinear hsw htr hx_col hy_col def VerticalNormalizedButterflyConfiguration.toButterflyConfiguration (cfg : VerticalNormalizedButterflyConfiguration) : ButterflyConfiguration where center := point 0 cfg.k radiusSq := cfg.a ^ 2 + cfg.k ^ 2 M := point 0 0 P := point (-cfg.a) 0 Q := point cfg.a 0 A := point 0 cfg.s B := point 0 cfg.t C := point cfg.r (cfg.n * cfg.r) D := point cfg.w (cfg.n * cfg.w) X := point cfg.x 0 Y := point cfg.y 0 def ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration (cfg : ReverseVerticalNormalizedButterflyConfiguration) : ButterflyConfiguration where center := point 0 cfg.k radiusSq := cfg.a ^ 2 + cfg.k ^ 2 M := point 0 0 P := point (-cfg.a) 0 Q := point cfg.a 0 A := point cfg.u (cfg.m * cfg.u) B := point cfg.v (cfg.m * cfg.v) C := point 0 cfg.s D := point 0 cfg.t X := point cfg.x 0 Y := point cfg.y 0 def BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration (cfg : BothVerticalNormalizedButterflyConfiguration) : ButterflyConfiguration where center := point 0 cfg.k radiusSq := cfg.a ^ 2 + cfg.k ^ 2 M := point 0 0 P := point (-cfg.a) 0 Q := point cfg.a 0 A := point 0 cfg.s B := point 0 cfg.t C := point 0 cfg.r D := point 0 cfg.w X := point cfg.x 0 Y := point cfg.y 0 theorem vertical_radiusSq_pos (cfg : VerticalNormalizedButterflyConfiguration) (hcfg : VerticalNormalizedButterflyHyp cfg) : 0 < cfg.a ^ 2 + cfg.k ^ 2 := by rcases hcfg with ⟨hs, ht, _hr, _hw, hst, _hrw, _hx_den, _hy_den, _hx_col, _hy_col⟩ have hnonneg : 0 ≤ cfg.a ^ 2 + cfg.k ^ 2 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hne : cfg.a ^ 2 + cfg.k ^ 2 ≠ 0 := by intro hzero have hs_eq := vertical_circle_equation.mp hs have ht_eq := vertical_circle_equation.mp ht have ha0 : cfg.a = 0 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hk0 : cfg.k = 0 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hs0 : cfg.s = 0 := by nlinarith [hs_eq, ha0, hk0, sq_nonneg cfg.s] have ht0 : cfg.t = 0 := by nlinarith [ht_eq, ha0, hk0, sq_nonneg cfg.t] exact hst (by rw [hs0, ht0]) exact lt_of_le_of_ne hnonneg (Ne.symm hne) theorem reverseVertical_radiusSq_pos (cfg : ReverseVerticalNormalizedButterflyConfiguration) (hcfg : ReverseVerticalNormalizedButterflyHyp cfg) : 0 < cfg.a ^ 2 + cfg.k ^ 2 := by rcases hcfg with ⟨hu, hv, _hs, _ht, huv, _hst, _hx_den, _hy_den, _hx_col, _hy_col⟩ have hnonneg : 0 ≤ cfg.a ^ 2 + cfg.k ^ 2 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hne : cfg.a ^ 2 + cfg.k ^ 2 ≠ 0 := by intro hzero have hu_dist : cfg.u ^ 2 + (cfg.m * cfg.u - cfg.k) ^ 2 = cfg.a ^ 2 + cfg.k ^ 2 := by simpa [OnCircleSq, sqDist, sqNorm, vsub, point] using hu have hv_dist : cfg.v ^ 2 + (cfg.m * cfg.v - cfg.k) ^ 2 = cfg.a ^ 2 + cfg.k ^ 2 := by simpa [OnCircleSq, sqDist, sqNorm, vsub, point] using hv have hu0 : cfg.u = 0 := by nlinarith [hu_dist, hzero, sq_nonneg cfg.u, sq_nonneg (cfg.m * cfg.u - cfg.k)] have hv0 : cfg.v = 0 := by nlinarith [hv_dist, hzero, sq_nonneg cfg.v, sq_nonneg (cfg.m * cfg.v - cfg.k)] exact huv (by rw [hu0, hv0]) exact lt_of_le_of_ne hnonneg (Ne.symm hne) theorem bothVertical_radiusSq_pos (cfg : BothVerticalNormalizedButterflyConfiguration) (hcfg : BothVerticalNormalizedButterflyHyp cfg) : 0 < cfg.a ^ 2 + cfg.k ^ 2 := by rcases hcfg with ⟨hs, ht, _hr, _hw, hst, _hrw, _hsw, _htr, _hx_col, _hy_col⟩ have hnonneg : 0 ≤ cfg.a ^ 2 + cfg.k ^ 2 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hne : cfg.a ^ 2 + cfg.k ^ 2 ≠ 0 := by intro hzero have hs_eq := vertical_circle_equation.mp hs have ht_eq := vertical_circle_equation.mp ht have ha0 : cfg.a = 0 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hk0 : cfg.k = 0 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hs0 : cfg.s = 0 := by nlinarith [hs_eq, ha0, hk0, sq_nonneg cfg.s] have ht0 : cfg.t = 0 := by nlinarith [ht_eq, ha0, hk0, sq_nonneg cfg.t] exact hst (by rw [hs0, ht0]) exact lt_of_le_of_ne hnonneg (Ne.symm hne) theorem vertical_toButterflyConfiguration_hyp (cfg : VerticalNormalizedButterflyConfiguration) (hcfg : VerticalNormalizedButterflyHyp cfg) : ButterflyHyp cfg.toButterflyConfiguration := by have hradius := vertical_radiusSq_pos cfg hcfg rcases hcfg with ⟨hs, ht, hr, hw, _hst, _hrw, _hx_den, _hy_den, hx_col, hy_col⟩ unfold ButterflyHyp constructor · exact hradius constructor · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · exact hs constructor · exact ht constructor · exact hr constructor · exact hw constructor · unfold IsMidpoint ext i fin_cases i <;> norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, midpoint, point] constructor · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] ring constructor · exact hx_col constructor · exact hy_col constructor · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] theorem reverseVertical_toButterflyConfiguration_hyp (cfg : ReverseVerticalNormalizedButterflyConfiguration) (hcfg : ReverseVerticalNormalizedButterflyHyp cfg) : ButterflyHyp cfg.toButterflyConfiguration := by have hradius := reverseVertical_radiusSq_pos cfg hcfg rcases hcfg with ⟨hu, hv, hs, ht, _huv, _hst, _hx_den, _hy_den, hx_col, hy_col⟩ unfold ButterflyHyp constructor · exact hradius constructor · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · exact hu constructor · exact hv constructor · exact hs constructor · exact ht constructor · unfold IsMidpoint ext i fin_cases i <;> norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, midpoint, point] constructor · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] ring constructor · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hx_col constructor · exact hy_col constructor · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] theorem bothVertical_toButterflyConfiguration_hyp (cfg : BothVerticalNormalizedButterflyConfiguration) (hcfg : BothVerticalNormalizedButterflyHyp cfg) : ButterflyHyp cfg.toButterflyConfiguration := by have hradius := bothVertical_radiusSq_pos cfg hcfg rcases hcfg with ⟨hs, ht, hr, hw, _hst, _hrw, _hsw, _htr, hx_col, hy_col⟩ unfold ButterflyHyp constructor · exact hradius constructor · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · exact hs constructor · exact ht constructor · exact hr constructor · exact hw constructor · unfold IsMidpoint ext i fin_cases i <;> norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, midpoint, point] constructor · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hx_col constructor · exact hy_col constructor · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] theorem vertical_toButterflyConfiguration_conclusion (cfg : VerticalNormalizedButterflyConfiguration) (hcfg : VerticalNormalizedButterflyHyp cfg) : IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y := verticalNormalizedButterflyTheorem_config cfg hcfg theorem reverseVertical_toButterflyConfiguration_conclusion (cfg : ReverseVerticalNormalizedButterflyConfiguration) (hcfg : ReverseVerticalNormalizedButterflyHyp cfg) : IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y := reverseVerticalNormalizedButterflyTheorem_config cfg hcfg theorem bothVertical_toButterflyConfiguration_conclusion (cfg : BothVerticalNormalizedButterflyConfiguration) (hcfg : BothVerticalNormalizedButterflyHyp cfg) : IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y := bothVerticalNormalizedButterflyTheorem_config cfg hcfg def VerticalNormalizedEmbeddedButterflyStatement : Prop := ∀ cfg : VerticalNormalizedButterflyConfiguration, VerticalNormalizedButterflyHyp cfg → ButterflyHyp cfg.toButterflyConfiguration ∧ IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y theorem verticalNormalizedEmbeddedButterflyTheorem : VerticalNormalizedEmbeddedButterflyStatement := by intro cfg hcfg exact ⟨vertical_toButterflyConfiguration_hyp cfg hcfg, vertical_toButterflyConfiguration_conclusion cfg hcfg⟩ def ReverseVerticalNormalizedEmbeddedButterflyStatement : Prop := ∀ cfg : ReverseVerticalNormalizedButterflyConfiguration, ReverseVerticalNormalizedButterflyHyp cfg → ButterflyHyp cfg.toButterflyConfiguration ∧ IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y theorem reverseVerticalNormalizedEmbeddedButterflyTheorem : ReverseVerticalNormalizedEmbeddedButterflyStatement := by intro cfg hcfg exact ⟨reverseVertical_toButterflyConfiguration_hyp cfg hcfg, reverseVertical_toButterflyConfiguration_conclusion cfg hcfg⟩ def BothVerticalNormalizedEmbeddedButterflyStatement : Prop := ∀ cfg : BothVerticalNormalizedButterflyConfiguration, BothVerticalNormalizedButterflyHyp cfg → ButterflyHyp cfg.toButterflyConfiguration ∧ IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y theorem bothVerticalNormalizedEmbeddedButterflyTheorem : BothVerticalNormalizedEmbeddedButterflyStatement := by intro cfg hcfg exact ⟨bothVertical_toButterflyConfiguration_hyp cfg hcfg, bothVertical_toButterflyConfiguration_conclusion cfg hcfg⟩ def HasVerticalNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ vcfg : VerticalNormalizedButterflyConfiguration, VerticalNormalizedButterflyHyp vcfg ∧ cfg = vcfg.toButterflyConfiguration theorem hasVerticalNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasVerticalNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨vcfg, hvcfg, rfl⟩ exact vertical_toButterflyConfiguration_hyp vcfg hvcfg theorem hasVerticalNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasVerticalNormalizedButterflyModel cfg) : IsMidpoint cfg.M cfg.X cfg.Y := by rcases hmodel with ⟨vcfg, hvcfg, rfl⟩ exact vertical_toButterflyConfiguration_conclusion vcfg hvcfg def VerticalNormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasVerticalNormalizedButterflyModel cfg def VerticalNormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, VerticalNormalizedModelButterflyHyp cfg → IsMidpoint cfg.M cfg.X cfg.Y theorem verticalNormalizedModelButterflyTheorem : VerticalNormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasVerticalNormalizedButterflyModel_conclusion hcfg.2 theorem vertical_toButterflyConfiguration_hasVerticalNormalizedButterflyModel (cfg : VerticalNormalizedButterflyConfiguration) (hcfg : VerticalNormalizedButterflyHyp cfg) : HasVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ def HasReverseVerticalNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ rvcfg : ReverseVerticalNormalizedButterflyConfiguration, ReverseVerticalNormalizedButterflyHyp rvcfg ∧ cfg = rvcfg.toButterflyConfiguration def ReverseVerticalNormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasReverseVerticalNormalizedButterflyModel cfg def ReverseVerticalNormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, ReverseVerticalNormalizedModelButterflyHyp cfg → IsMidpoint cfg.M cfg.X cfg.Y theorem hasReverseVerticalNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasReverseVerticalNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨rvcfg, hrvcfg, rfl⟩ exact reverseVertical_toButterflyConfiguration_hyp rvcfg hrvcfg theorem hasReverseVerticalNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasReverseVerticalNormalizedButterflyModel cfg) : IsMidpoint cfg.M cfg.X cfg.Y := by rcases hmodel with ⟨rvcfg, hrvcfg, rfl⟩ exact reverseVertical_toButterflyConfiguration_conclusion rvcfg hrvcfg theorem reverseVerticalNormalizedModelButterflyTheorem : ReverseVerticalNormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasReverseVerticalNormalizedButterflyModel_conclusion hcfg.2 theorem reverseVertical_toButterflyConfiguration_hasReverseVerticalNormalizedButterflyModel (cfg : ReverseVerticalNormalizedButterflyConfiguration) (hcfg : ReverseVerticalNormalizedButterflyHyp cfg) : HasReverseVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ def HasBothVerticalNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ bvcfg : BothVerticalNormalizedButterflyConfiguration, BothVerticalNormalizedButterflyHyp bvcfg ∧ cfg = bvcfg.toButterflyConfiguration def BothVerticalNormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasBothVerticalNormalizedButterflyModel cfg def BothVerticalNormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, BothVerticalNormalizedModelButterflyHyp cfg → IsMidpoint cfg.M cfg.X cfg.Y theorem hasBothVerticalNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasBothVerticalNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨bvcfg, hbvcfg, rfl⟩ exact bothVertical_toButterflyConfiguration_hyp bvcfg hbvcfg theorem hasBothVerticalNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasBothVerticalNormalizedButterflyModel cfg) : IsMidpoint cfg.M cfg.X cfg.Y := by rcases hmodel with ⟨bvcfg, hbvcfg, rfl⟩ exact bothVertical_toButterflyConfiguration_conclusion bvcfg hbvcfg theorem bothVerticalNormalizedModelButterflyTheorem : BothVerticalNormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasBothVerticalNormalizedButterflyModel_conclusion hcfg.2 theorem bothVertical_toButterflyConfiguration_hasBothVerticalNormalizedButterflyModel (cfg : BothVerticalNormalizedButterflyConfiguration) (hcfg : BothVerticalNormalizedButterflyHyp cfg) : HasBothVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ theorem vertical_toButterflyConfiguration_uniqueIntersections (cfg : VerticalNormalizedButterflyConfiguration) (hcfg : VerticalNormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y := by rcases hcfg with ⟨_hs, _ht, _hr, _hw, _hst, _hrw, hx_den, hy_den, hx_col, hy_col⟩ constructor · unfold UniqueIntersection constructor · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hx_col · intro z hz_base hz_ad exact vertical_base_intersection_unique ha hx_den hx_col hz_base hz_ad · unfold UniqueIntersection constructor · norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hy_col · intro z hz_base hz_bc exact vertical_base_intersection_unique (a := cfg.a) (n := cfg.n) (s := cfg.t) (w := cfg.r) (x := cfg.y) ha hy_den hy_col hz_base hz_bc theorem vertical_toButterflyConfiguration_distinctChordEndpoints (cfg : VerticalNormalizedButterflyConfiguration) (hcfg : VerticalNormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : DistinctChordEndpoints cfg.toButterflyConfiguration := by rcases hcfg with ⟨_hs, _ht, _hr, _hw, hst, hrw, _hx_den, _hy_den, _hx_col, _hy_col⟩ unfold DistinctChordEndpoints constructor · intro hpq have h0 := congrFun hpq 0 norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 have ha0 : cfg.a = 0 := by nlinarith exact ha ha0 constructor · intro hab have h1 := congrFun hab 1 norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h1 exact hst h1 · intro hcd have h0 := congrFun hcd 0 norm_num [VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 exact hrw h0 theorem reverseVertical_toButterflyConfiguration_uniqueIntersections (cfg : ReverseVerticalNormalizedButterflyConfiguration) (hcfg : ReverseVerticalNormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y := by rcases hcfg with ⟨_hu, _hv, _hs, _ht, _huv, _hst, hx_den, hy_den, hx_col, hy_col⟩ constructor · unfold UniqueIntersection constructor · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hx_col · intro z hz_base hz_ad exact vertical_base_intersection_unique (a := cfg.a) (n := cfg.m) (s := cfg.t) (w := cfg.u) (x := cfg.x) ha hx_den (collinear_swap hx_col) hz_base (collinear_swap hz_ad) · unfold UniqueIntersection constructor · norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hy_col · intro z hz_base hz_bc exact vertical_base_intersection_unique (a := cfg.a) (n := cfg.m) (s := cfg.s) (w := cfg.v) (x := cfg.y) ha hy_den (collinear_swap hy_col) hz_base (collinear_swap hz_bc) theorem reverseVertical_toButterflyConfiguration_distinctChordEndpoints (cfg : ReverseVerticalNormalizedButterflyConfiguration) (hcfg : ReverseVerticalNormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : DistinctChordEndpoints cfg.toButterflyConfiguration := by rcases hcfg with ⟨_hu, _hv, _hs, _ht, huv, hst, _hx_den, _hy_den, _hx_col, _hy_col⟩ unfold DistinctChordEndpoints constructor · intro hpq have h0 := congrFun hpq 0 norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 have ha0 : cfg.a = 0 := by nlinarith exact ha ha0 constructor · intro hab have h0 := congrFun hab 0 norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 exact huv h0 · intro hcd have h1 := congrFun hcd 1 norm_num [ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h1 exact hst h1 theorem bothVertical_toButterflyConfiguration_uniqueIntersections (cfg : BothVerticalNormalizedButterflyConfiguration) (hcfg : BothVerticalNormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y := by rcases hcfg with ⟨_hs, _ht, _hr, _hw, _hst, _hrw, hsw, htr, hx_col, hy_col⟩ constructor · unfold UniqueIntersection constructor · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hx_col · intro z hz_base hz_ad exact vertical_line_base_intersection_unique (a := cfg.a) (s := cfg.s) (w := cfg.w) (x := cfg.x) ha hsw hx_col hz_base hz_ad · unfold UniqueIntersection constructor · norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hy_col · intro z hz_base hz_bc exact vertical_line_base_intersection_unique (a := cfg.a) (s := cfg.t) (w := cfg.r) (x := cfg.y) ha htr hy_col hz_base hz_bc theorem bothVertical_toButterflyConfiguration_distinctChordEndpoints (cfg : BothVerticalNormalizedButterflyConfiguration) (hcfg : BothVerticalNormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : DistinctChordEndpoints cfg.toButterflyConfiguration := by rcases hcfg with ⟨_hs, _ht, _hr, _hw, hst, hrw, _hsw, _htr, _hx_col, _hy_col⟩ unfold DistinctChordEndpoints constructor · intro hpq have h0 := congrFun hpq 0 norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 have ha0 : cfg.a = 0 := by nlinarith exact ha ha0 constructor · intro hab have h1 := congrFun hab 1 norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h1 exact hst h1 · intro hcd have h1 := congrFun hcd 1 norm_num [BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h1 exact hrw h1 def StrictVerticalNormalizedButterflyHyp (cfg : VerticalNormalizedButterflyConfiguration) : Prop := VerticalNormalizedButterflyHyp cfg ∧ cfg.a ≠ 0 def StrictVerticalNormalizedButterflyConclusion (cfg : VerticalNormalizedButterflyConfiguration) : Prop := VerticalNormalizedButterflyConclusion cfg ∧ DistinctChordEndpoints cfg.toButterflyConfiguration ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y def StrictVerticalNormalizedButterflyConfigurationStatement : Prop := ∀ cfg : VerticalNormalizedButterflyConfiguration, StrictVerticalNormalizedButterflyHyp cfg → StrictVerticalNormalizedButterflyConclusion cfg theorem strictVerticalNormalizedButterflyTheorem_config : StrictVerticalNormalizedButterflyConfigurationStatement := by intro cfg hcfg have huniq := vertical_toButterflyConfiguration_uniqueIntersections cfg hcfg.1 hcfg.2 exact ⟨verticalNormalizedButterflyTheorem_config cfg hcfg.1, vertical_toButterflyConfiguration_distinctChordEndpoints cfg hcfg.1 hcfg.2, huniq.1, huniq.2⟩ def StrictReverseVerticalNormalizedButterflyHyp (cfg : ReverseVerticalNormalizedButterflyConfiguration) : Prop := ReverseVerticalNormalizedButterflyHyp cfg ∧ cfg.a ≠ 0 def StrictReverseVerticalNormalizedButterflyConclusion (cfg : ReverseVerticalNormalizedButterflyConfiguration) : Prop := ReverseVerticalNormalizedButterflyConclusion cfg ∧ DistinctChordEndpoints cfg.toButterflyConfiguration ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y def StrictReverseVerticalNormalizedButterflyConfigurationStatement : Prop := ∀ cfg : ReverseVerticalNormalizedButterflyConfiguration, StrictReverseVerticalNormalizedButterflyHyp cfg → StrictReverseVerticalNormalizedButterflyConclusion cfg theorem strictReverseVerticalNormalizedButterflyTheorem_config : StrictReverseVerticalNormalizedButterflyConfigurationStatement := by intro cfg hcfg have huniq := reverseVertical_toButterflyConfiguration_uniqueIntersections cfg hcfg.1 hcfg.2 exact ⟨reverseVerticalNormalizedButterflyTheorem_config cfg hcfg.1, reverseVertical_toButterflyConfiguration_distinctChordEndpoints cfg hcfg.1 hcfg.2, huniq.1, huniq.2⟩ def StrictBothVerticalNormalizedButterflyHyp (cfg : BothVerticalNormalizedButterflyConfiguration) : Prop := BothVerticalNormalizedButterflyHyp cfg ∧ cfg.a ≠ 0 def StrictBothVerticalNormalizedButterflyConclusion (cfg : BothVerticalNormalizedButterflyConfiguration) : Prop := BothVerticalNormalizedButterflyConclusion cfg ∧ DistinctChordEndpoints cfg.toButterflyConfiguration ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y def StrictBothVerticalNormalizedButterflyConfigurationStatement : Prop := ∀ cfg : BothVerticalNormalizedButterflyConfiguration, StrictBothVerticalNormalizedButterflyHyp cfg → StrictBothVerticalNormalizedButterflyConclusion cfg theorem strictBothVerticalNormalizedButterflyTheorem_config : StrictBothVerticalNormalizedButterflyConfigurationStatement := by intro cfg hcfg have huniq := bothVertical_toButterflyConfiguration_uniqueIntersections cfg hcfg.1 hcfg.2 exact ⟨bothVerticalNormalizedButterflyTheorem_config cfg hcfg.1, bothVertical_toButterflyConfiguration_distinctChordEndpoints cfg hcfg.1 hcfg.2, huniq.1, huniq.2⟩ def NormalizedButterflyTheoremStatement : Prop := ∀ a k m n u v r w x y : ℝ, OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point u (m * u)) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point v (m * v)) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point r (n * r)) → OnCircleSq (point 0 k) (a ^ 2 + k ^ 2) (point w (n * w)) → u ≠ v → r ≠ w → n * w - m * u ≠ 0 → n * r - m * v ≠ 0 → Collinear (point u (m * u)) (point w (n * w)) (point x 0) → Collinear (point v (m * v)) (point r (n * r)) (point y 0) → IsMidpoint (point 0 0) (point x 0) (point y 0) theorem normalizedButterflyTheorem : NormalizedButterflyTheoremStatement := by intro a k m n u v r w x y hu hv hr hw huv hrw hx_den hy_den hx_col hy_col exact normalized_butterfly_midpoint_from_circle hu hv hr hw huv hrw hx_den hy_den hx_col hy_col structure NormalizedButterflyConfiguration where a : ℝ k : ℝ m : ℝ n : ℝ u : ℝ v : ℝ r : ℝ w : ℝ x : ℝ y : ℝ def NormalizedButterflyHyp (cfg : NormalizedButterflyConfiguration) : Prop := OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.u (cfg.m * cfg.u)) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.v (cfg.m * cfg.v)) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.r (cfg.n * cfg.r)) ∧ OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) (point cfg.w (cfg.n * cfg.w)) ∧ cfg.u ≠ cfg.v ∧ cfg.r ≠ cfg.w ∧ cfg.n * cfg.w - cfg.m * cfg.u ≠ 0 ∧ cfg.n * cfg.r - cfg.m * cfg.v ≠ 0 ∧ Collinear (point cfg.u (cfg.m * cfg.u)) (point cfg.w (cfg.n * cfg.w)) (point cfg.x 0) ∧ Collinear (point cfg.v (cfg.m * cfg.v)) (point cfg.r (cfg.n * cfg.r)) (point cfg.y 0) def NormalizedButterflyConclusion (cfg : NormalizedButterflyConfiguration) : Prop := IsMidpoint (point 0 0) (point cfg.x 0) (point cfg.y 0) def NormalizedButterflyConfigurationStatement : Prop := ∀ cfg : NormalizedButterflyConfiguration, NormalizedButterflyHyp cfg → NormalizedButterflyConclusion cfg theorem normalizedButterflyTheorem_config : NormalizedButterflyConfigurationStatement := by intro cfg hcfg rcases hcfg with ⟨hu, hv, hr, hw, huv, hrw, hx_den, hy_den, hx_col, hy_col⟩ exact normalized_butterfly_midpoint_from_circle hu hv hr hw huv hrw hx_den hy_den hx_col hy_col theorem normalizedButterflyTheoremStatement_iff_config : NormalizedButterflyTheoremStatement ↔ NormalizedButterflyConfigurationStatement := by constructor · intro h cfg hcfg rcases hcfg with ⟨hu, hv, hr, hw, huv, hrw, hx_den, hy_den, hx_col, hy_col⟩ exact h cfg.a cfg.k cfg.m cfg.n cfg.u cfg.v cfg.r cfg.w cfg.x cfg.y hu hv hr hw huv hrw hx_den hy_den hx_col hy_col · intro h a k m n u v r w x y hu hv hr hw huv hrw hx_den hy_den hx_col hy_col exact h { a := a, k := k, m := m, n := n, u := u, v := v, r := r, w := w, x := x, y := y } ⟨hu, hv, hr, hw, huv, hrw, hx_den, hy_den, hx_col, hy_col⟩ def NormalizedButterflyConfiguration.toButterflyConfiguration (cfg : NormalizedButterflyConfiguration) : ButterflyConfiguration where center := point 0 cfg.k radiusSq := cfg.a ^ 2 + cfg.k ^ 2 M := point 0 0 P := point (-cfg.a) 0 Q := point cfg.a 0 A := point cfg.u (cfg.m * cfg.u) B := point cfg.v (cfg.m * cfg.v) C := point cfg.r (cfg.n * cfg.r) D := point cfg.w (cfg.n * cfg.w) X := point cfg.x 0 Y := point cfg.y 0 theorem normalized_radiusSq_pos (cfg : NormalizedButterflyConfiguration) (hcfg : NormalizedButterflyHyp cfg) : 0 < cfg.a ^ 2 + cfg.k ^ 2 := by rcases hcfg with ⟨hu, hv, _hr, _hw, huv, _hrw, _hx_den, _hy_den, _hx_col, _hy_col⟩ have hnonneg : 0 ≤ cfg.a ^ 2 + cfg.k ^ 2 := by nlinarith [sq_nonneg cfg.a, sq_nonneg cfg.k] have hne : cfg.a ^ 2 + cfg.k ^ 2 ≠ 0 := by intro hzero have hu_dist : cfg.u ^ 2 + (cfg.m * cfg.u - cfg.k) ^ 2 = cfg.a ^ 2 + cfg.k ^ 2 := by simpa [OnCircleSq, sqDist, sqNorm, vsub, point] using hu have hv_dist : cfg.v ^ 2 + (cfg.m * cfg.v - cfg.k) ^ 2 = cfg.a ^ 2 + cfg.k ^ 2 := by simpa [OnCircleSq, sqDist, sqNorm, vsub, point] using hv have hu0 : cfg.u = 0 := by nlinarith [hu_dist, hzero, sq_nonneg cfg.u, sq_nonneg (cfg.m * cfg.u - cfg.k)] have hv0 : cfg.v = 0 := by nlinarith [hv_dist, hzero, sq_nonneg cfg.v, sq_nonneg (cfg.m * cfg.v - cfg.k)] exact huv (by rw [hu0, hv0]) exact lt_of_le_of_ne hnonneg (Ne.symm hne) theorem normalized_toButterflyConfiguration_hyp (cfg : NormalizedButterflyConfiguration) (hcfg : NormalizedButterflyHyp cfg) : ButterflyHyp cfg.toButterflyConfiguration := by have hradius := normalized_radiusSq_pos cfg hcfg rcases hcfg with ⟨hu, hv, hr, hw, _huv, _hrw, _hx_den, _hy_den, hx_col, hy_col⟩ unfold ButterflyHyp constructor · exact hradius constructor · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · exact hu constructor · exact hv constructor · exact hr constructor · exact hw constructor · unfold IsMidpoint ext i fin_cases i <;> norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, midpoint, point] constructor · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] ring constructor · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] ring constructor · exact hx_col constructor · exact hy_col constructor · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] theorem normalized_toButterflyConfiguration_conclusion (cfg : NormalizedButterflyConfiguration) (hcfg : NormalizedButterflyHyp cfg) : IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y := normalizedButterflyTheorem_config cfg hcfg theorem normalized_toButterflyConfiguration_uniqueIntersections (cfg : NormalizedButterflyConfiguration) (hcfg : NormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y := by rcases hcfg with ⟨_hu, _hv, _hr, _hw, _huv, _hrw, hx_den, hy_den, hx_col, hy_col⟩ constructor · unfold UniqueIntersection constructor · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hx_col · intro z hz_base hz_ad exact normalized_base_intersection_unique ha hx_den hx_col hz_base hz_ad · unfold UniqueIntersection constructor · norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · exact hy_col · intro z hz_base hz_bc exact normalized_base_intersection_unique (a := cfg.a) (m := cfg.m) (n := cfg.n) (u := cfg.v) (w := cfg.r) (x := cfg.y) ha hy_den hy_col hz_base hz_bc theorem normalized_toButterflyConfiguration_distinctChordEndpoints (cfg : NormalizedButterflyConfiguration) (hcfg : NormalizedButterflyHyp cfg) (ha : cfg.a ≠ 0) : DistinctChordEndpoints cfg.toButterflyConfiguration := by rcases hcfg with ⟨_hu, _hv, _hr, _hw, huv, hrw, _hx_den, _hy_den, _hx_col, _hy_col⟩ unfold DistinctChordEndpoints constructor · intro hpq have h0 := congrFun hpq 0 norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 have ha0 : cfg.a = 0 := by nlinarith exact ha ha0 constructor · intro hab have h0 := congrFun hab 0 norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 exact huv h0 · intro hcd have h0 := congrFun hcd 0 norm_num [NormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 exact hrw h0 def StrictNormalizedButterflyHyp (cfg : NormalizedButterflyConfiguration) : Prop := NormalizedButterflyHyp cfg ∧ cfg.a ≠ 0 def StrictNormalizedButterflyConclusion (cfg : NormalizedButterflyConfiguration) : Prop := NormalizedButterflyConclusion cfg ∧ DistinctChordEndpoints cfg.toButterflyConfiguration ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.A cfg.toButterflyConfiguration.D cfg.toButterflyConfiguration.X ∧ UniqueIntersection cfg.toButterflyConfiguration.P cfg.toButterflyConfiguration.Q cfg.toButterflyConfiguration.B cfg.toButterflyConfiguration.C cfg.toButterflyConfiguration.Y def StrictNormalizedButterflyConfigurationStatement : Prop := ∀ cfg : NormalizedButterflyConfiguration, StrictNormalizedButterflyHyp cfg → StrictNormalizedButterflyConclusion cfg theorem strictNormalizedButterflyTheorem_config : StrictNormalizedButterflyConfigurationStatement := by intro cfg hcfg have huniq := normalized_toButterflyConfiguration_uniqueIntersections cfg hcfg.1 hcfg.2 exact ⟨normalizedButterflyTheorem_config cfg hcfg.1, normalized_toButterflyConfiguration_distinctChordEndpoints cfg hcfg.1 hcfg.2, huniq.1, huniq.2⟩ def NormalizedEmbeddedButterflyStatement : Prop := ∀ cfg : NormalizedButterflyConfiguration, NormalizedButterflyHyp cfg → ButterflyHyp cfg.toButterflyConfiguration ∧ IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y theorem normalizedEmbeddedButterflyTheorem : NormalizedEmbeddedButterflyStatement := by intro cfg hcfg exact ⟨normalized_toButterflyConfiguration_hyp cfg hcfg, normalized_toButterflyConfiguration_conclusion cfg hcfg⟩ /-- A v0 record is covered by the checked normalized nondegenerate model. -/ def HasNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ ncfg : NormalizedButterflyConfiguration, NormalizedButterflyHyp ncfg ∧ cfg = ncfg.toButterflyConfiguration theorem hasNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨ncfg, hncfg, rfl⟩ exact normalized_toButterflyConfiguration_hyp ncfg hncfg theorem hasNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasNormalizedButterflyModel cfg) : IsMidpoint cfg.M cfg.X cfg.Y := by rcases hmodel with ⟨ncfg, hncfg, rfl⟩ exact normalized_toButterflyConfiguration_conclusion ncfg hncfg def NormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasNormalizedButterflyModel cfg /-- Review-facing candidate strengthening; this is not the public v0 wrapper. -/ def NormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, NormalizedModelButterflyHyp cfg → IsMidpoint cfg.M cfg.X cfg.Y theorem normalizedModelButterflyTheorem : NormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasNormalizedButterflyModel_conclusion hcfg.2 theorem hasNormalizedButterflyModel_to_normalizedModelButterflyHyp {cfg : ButterflyConfiguration} (hmodel : HasNormalizedButterflyModel cfg) : NormalizedModelButterflyHyp cfg := ⟨hasNormalizedButterflyModel_hyp hmodel, hmodel⟩ theorem normalized_toButterflyConfiguration_hasNormalizedButterflyModel (cfg : NormalizedButterflyConfiguration) (hcfg : NormalizedButterflyHyp cfg) : HasNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ def HasStrictNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ ncfg : NormalizedButterflyConfiguration, StrictNormalizedButterflyHyp ncfg ∧ cfg = ncfg.toButterflyConfiguration def StrictNormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasStrictNormalizedButterflyModel cfg def StrictNormalizedModelButterflyConclusion (cfg : ButterflyConfiguration) : Prop := IsMidpoint cfg.M cfg.X cfg.Y ∧ DistinctChordEndpoints cfg ∧ UniqueIntersection cfg.P cfg.Q cfg.A cfg.D cfg.X ∧ UniqueIntersection cfg.P cfg.Q cfg.B cfg.C cfg.Y def StrictNormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, StrictNormalizedModelButterflyHyp cfg → StrictNormalizedModelButterflyConclusion cfg theorem hasStrictNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasStrictNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨ncfg, hncfg, rfl⟩ exact normalized_toButterflyConfiguration_hyp ncfg hncfg.1 theorem hasStrictNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasStrictNormalizedButterflyModel cfg) : StrictNormalizedModelButterflyConclusion cfg := by rcases hmodel with ⟨ncfg, hncfg, rfl⟩ have huniq := normalized_toButterflyConfiguration_uniqueIntersections ncfg hncfg.1 hncfg.2 exact ⟨normalized_toButterflyConfiguration_conclusion ncfg hncfg.1, normalized_toButterflyConfiguration_distinctChordEndpoints ncfg hncfg.1 hncfg.2, huniq.1, huniq.2⟩ theorem strictNormalizedModelButterflyTheorem : StrictNormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasStrictNormalizedButterflyModel_conclusion hcfg.2 theorem normalized_toButterflyConfiguration_hasStrictNormalizedButterflyModel (cfg : NormalizedButterflyConfiguration) (hcfg : StrictNormalizedButterflyHyp cfg) : HasStrictNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ def HasStrictVerticalNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ vcfg : VerticalNormalizedButterflyConfiguration, StrictVerticalNormalizedButterflyHyp vcfg ∧ cfg = vcfg.toButterflyConfiguration def StrictVerticalNormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasStrictVerticalNormalizedButterflyModel cfg def StrictVerticalNormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, StrictVerticalNormalizedModelButterflyHyp cfg → StrictNormalizedModelButterflyConclusion cfg theorem hasStrictVerticalNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasStrictVerticalNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨vcfg, hvcfg, rfl⟩ exact vertical_toButterflyConfiguration_hyp vcfg hvcfg.1 theorem hasStrictVerticalNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasStrictVerticalNormalizedButterflyModel cfg) : StrictNormalizedModelButterflyConclusion cfg := by rcases hmodel with ⟨vcfg, hvcfg, rfl⟩ have hconcl := strictVerticalNormalizedButterflyTheorem_config vcfg hvcfg exact ⟨vertical_toButterflyConfiguration_conclusion vcfg hvcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ theorem strictVerticalNormalizedModelButterflyTheorem : StrictVerticalNormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasStrictVerticalNormalizedButterflyModel_conclusion hcfg.2 theorem vertical_toButterflyConfiguration_hasStrictVerticalNormalizedButterflyModel (cfg : VerticalNormalizedButterflyConfiguration) (hcfg : StrictVerticalNormalizedButterflyHyp cfg) : HasStrictVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ def HasStrictReverseVerticalNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ rvcfg : ReverseVerticalNormalizedButterflyConfiguration, StrictReverseVerticalNormalizedButterflyHyp rvcfg ∧ cfg = rvcfg.toButterflyConfiguration def StrictReverseVerticalNormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasStrictReverseVerticalNormalizedButterflyModel cfg def StrictReverseVerticalNormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, StrictReverseVerticalNormalizedModelButterflyHyp cfg → StrictNormalizedModelButterflyConclusion cfg theorem hasStrictReverseVerticalNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasStrictReverseVerticalNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨rvcfg, hrvcfg, rfl⟩ exact reverseVertical_toButterflyConfiguration_hyp rvcfg hrvcfg.1 theorem hasStrictReverseVerticalNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasStrictReverseVerticalNormalizedButterflyModel cfg) : StrictNormalizedModelButterflyConclusion cfg := by rcases hmodel with ⟨rvcfg, hrvcfg, rfl⟩ have hconcl := strictReverseVerticalNormalizedButterflyTheorem_config rvcfg hrvcfg exact ⟨reverseVertical_toButterflyConfiguration_conclusion rvcfg hrvcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ theorem strictReverseVerticalNormalizedModelButterflyTheorem : StrictReverseVerticalNormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasStrictReverseVerticalNormalizedButterflyModel_conclusion hcfg.2 theorem reverseVertical_toButterflyConfiguration_hasStrictReverseVerticalNormalizedButterflyModel (cfg : ReverseVerticalNormalizedButterflyConfiguration) (hcfg : StrictReverseVerticalNormalizedButterflyHyp cfg) : HasStrictReverseVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ def HasStrictBothVerticalNormalizedButterflyModel (cfg : ButterflyConfiguration) : Prop := ∃ bvcfg : BothVerticalNormalizedButterflyConfiguration, StrictBothVerticalNormalizedButterflyHyp bvcfg ∧ cfg = bvcfg.toButterflyConfiguration def StrictBothVerticalNormalizedModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ HasStrictBothVerticalNormalizedButterflyModel cfg def StrictBothVerticalNormalizedModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, StrictBothVerticalNormalizedModelButterflyHyp cfg → StrictNormalizedModelButterflyConclusion cfg theorem hasStrictBothVerticalNormalizedButterflyModel_hyp {cfg : ButterflyConfiguration} (hmodel : HasStrictBothVerticalNormalizedButterflyModel cfg) : ButterflyHyp cfg := by rcases hmodel with ⟨bvcfg, hbvcfg, rfl⟩ exact bothVertical_toButterflyConfiguration_hyp bvcfg hbvcfg.1 theorem hasStrictBothVerticalNormalizedButterflyModel_conclusion {cfg : ButterflyConfiguration} (hmodel : HasStrictBothVerticalNormalizedButterflyModel cfg) : StrictNormalizedModelButterflyConclusion cfg := by rcases hmodel with ⟨bvcfg, hbvcfg, rfl⟩ have hconcl := strictBothVerticalNormalizedButterflyTheorem_config bvcfg hbvcfg exact ⟨bothVertical_toButterflyConfiguration_conclusion bvcfg hbvcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ theorem strictBothVerticalNormalizedModelButterflyTheorem : StrictBothVerticalNormalizedModelButterflyTheoremStatement := by intro cfg hcfg exact hasStrictBothVerticalNormalizedButterflyModel_conclusion hcfg.2 theorem bothVertical_toButterflyConfiguration_hasStrictBothVerticalNormalizedButterflyModel (cfg : BothVerticalNormalizedButterflyConfiguration) (hcfg : StrictBothVerticalNormalizedButterflyHyp cfg) : HasStrictBothVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := ⟨cfg, hcfg, rfl⟩ def StrictCheckedChartModelButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ (HasStrictNormalizedButterflyModel cfg ∨ HasStrictVerticalNormalizedButterflyModel cfg ∨ HasStrictReverseVerticalNormalizedButterflyModel cfg ∨ HasStrictBothVerticalNormalizedButterflyModel cfg) def StrictCheckedChartModelButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, StrictCheckedChartModelButterflyHyp cfg → StrictNormalizedModelButterflyConclusion cfg theorem strictCheckedChartModelButterflyTheorem : StrictCheckedChartModelButterflyTheoremStatement := by intro cfg hcfg rcases hcfg.2 with hnorm | hvert | hrev | hboth · exact strictNormalizedModelButterflyTheorem cfg ⟨hcfg.1, hnorm⟩ · exact strictVerticalNormalizedModelButterflyTheorem cfg ⟨hcfg.1, hvert⟩ · exact strictReverseVerticalNormalizedModelButterflyTheorem cfg ⟨hcfg.1, hrev⟩ · exact strictBothVerticalNormalizedModelButterflyTheorem cfg ⟨hcfg.1, hboth⟩ def NondegenerateButterflyHyp (cfg : ButterflyConfiguration) : Prop := ButterflyHyp cfg ∧ DistinctChordEndpoints cfg ∧ UniqueIntersection cfg.P cfg.Q cfg.A cfg.D cfg.X ∧ UniqueIntersection cfg.P cfg.Q cfg.B cfg.C cfg.Y def NondegenerateButterflyTheoremStatement : Prop := ∀ cfg : ButterflyConfiguration, NondegenerateButterflyHyp cfg → IsMidpoint cfg.M cfg.X cfg.Y structure BaseNormalizedButterflyConfiguration where a : ℝ k : ℝ A : Point B : Point C : Point D : Point x : ℝ y : ℝ noncomputable def baseNormalizedConfiguration (cfg : ButterflyConfiguration) : BaseNormalizedButterflyConfiguration where a := 1 k := (baseNormalize cfg.M cfg.Q cfg.center) 1 A := baseNormalize cfg.M cfg.Q cfg.A B := baseNormalize cfg.M cfg.Q cfg.B C := baseNormalize cfg.M cfg.Q cfg.C D := baseNormalize cfg.M cfg.Q cfg.D x := (baseNormalize cfg.M cfg.Q cfg.X) 0 y := (baseNormalize cfg.M cfg.Q cfg.Y) 0 def BaseNormalizedButterflyConfiguration.toButterflyConfiguration (cfg : BaseNormalizedButterflyConfiguration) : ButterflyConfiguration where center := point 0 cfg.k radiusSq := cfg.a ^ 2 + cfg.k ^ 2 M := point 0 0 P := point (-cfg.a) 0 Q := point cfg.a 0 A := cfg.A B := cfg.B C := cfg.C D := cfg.D X := point cfg.x 0 Y := point cfg.y 0 def BaseNormalizedButterflyHyp (cfg : BaseNormalizedButterflyConfiguration) : Prop := NondegenerateButterflyHyp cfg.toButterflyConfiguration def BaseNormalizedCheckedChartCoverageStatement : Prop := ∀ cfg : BaseNormalizedButterflyConfiguration, BaseNormalizedButterflyHyp cfg → StrictCheckedChartModelButterflyHyp cfg.toButterflyConfiguration def BaseNormalizedButterflyTheoremStatement : Prop := ∀ cfg : BaseNormalizedButterflyConfiguration, BaseNormalizedButterflyHyp cfg → IsMidpoint cfg.toButterflyConfiguration.M cfg.toButterflyConfiguration.X cfg.toButterflyConfiguration.Y theorem baseNormalized_a_ne (cfg : BaseNormalizedButterflyConfiguration) (hcfg : BaseNormalizedButterflyHyp cfg) : cfg.a ≠ 0 := by have hbase : point (-cfg.a) 0 ≠ point cfg.a 0 := by simpa [BaseNormalizedButterflyHyp, NondegenerateButterflyHyp, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.1 exact normalized_base_a_ne_of_distinct hbase theorem baseNormalized_hasStrictNormalizedModel_of_finite_finite (cfg : BaseNormalizedButterflyConfiguration) (hcfg : BaseNormalizedButterflyHyp cfg) (hA0 : cfg.A 0 ≠ 0) (hC0 : cfg.C 0 ≠ 0) : HasStrictNormalizedButterflyModel cfg.toButterflyConfiguration := by have ha : cfg.a ≠ 0 := baseNormalized_a_ne cfg hcfg rcases hcfg.1 with ⟨_hradius, _hP, _hQ, hAon, hBon, hCon, hDon, _hmid, hAB, hCD, _hAD, _hBC, _hPX, _hPY⟩ have hdistAB : cfg.A ≠ cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.1 have hdistCD : cfg.C ≠ cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.2 have hAon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.A := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAon have hBon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hBon have hCon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.C := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCon have hDon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hDon have hAB0 : Collinear cfg.A (point 0 0) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAB have hCD0 : Collinear cfg.C (point 0 0) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCD have huniqX : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.A cfg.D (point cfg.x 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.1 have huniqY : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.B cfg.C (point cfg.y 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.2 let ncfg : NormalizedButterflyConfiguration := { a := cfg.a k := cfg.k m := cfg.A 1 / cfg.A 0 n := cfg.C 1 / cfg.C 0 u := cfg.A 0 v := cfg.B 0 r := cfg.C 0 w := cfg.D 0 x := cfg.x y := cfg.y } have hA_point : point (cfg.A 0) (ncfg.m * cfg.A 0) = cfg.A := by ext i fin_cases i · simp [point] · simp [point, ncfg] field_simp [hA0] have hB_y : cfg.B 1 = ncfg.m * cfg.B 0 := by simpa [ncfg] using collinear_origin_finite_slope_point hA0 hAB0 have hB_point : point (cfg.B 0) (ncfg.m * cfg.B 0) = cfg.B := by ext i fin_cases i · simp [point] · simp [point, hB_y] have hC_point : point (cfg.C 0) (ncfg.n * cfg.C 0) = cfg.C := by ext i fin_cases i · simp [point] · simp [point, ncfg] field_simp [hC0] have hD_y : cfg.D 1 = ncfg.n * cfg.D 0 := by simpa [ncfg] using collinear_origin_finite_slope_point hC0 hCD0 have hD_point : point (cfg.D 0) (ncfg.n * cfg.D 0) = cfg.D := by ext i fin_cases i · simp [point] · simp [point, hD_y] have huv : ncfg.u ≠ ncfg.v := by simpa [ncfg] using finite_slope_x_ne_of_point_ne_point hA0 hAB0 hdistAB have hrw : ncfg.r ≠ ncfg.w := by simpa [ncfg] using finite_slope_x_ne_of_point_ne_point hC0 hCD0 hdistCD have huniqX_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point ncfg.u (ncfg.m * ncfg.u)) (point ncfg.w (ncfg.n * ncfg.w)) (point ncfg.x 0) := by simpa [ncfg, hA_point, hD_point] using huniqX have huniqY_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point ncfg.v (ncfg.m * ncfg.v)) (point ncfg.r (ncfg.n * ncfg.r)) (point ncfg.y 0) := by simpa [ncfg, hB_point, hC_point] using huniqY have hx_den : ncfg.n * ncfg.w - ncfg.m * ncfg.u ≠ 0 := by simpa [ncfg] using unique_intersection_base_finite_finite_den_ne (a := cfg.a) (m := ncfg.m) (n := ncfg.n) (u := ncfg.u) (w := ncfg.w) (x := ncfg.x) ha huniqX_points have hy_den : ncfg.n * ncfg.r - ncfg.m * ncfg.v ≠ 0 := by simpa [ncfg] using unique_intersection_base_finite_finite_den_ne (a := cfg.a) (m := ncfg.m) (n := ncfg.n) (u := ncfg.v) (w := ncfg.r) (x := ncfg.y) ha huniqY_points refine ⟨ncfg, ?_, ?_⟩ · constructor · unfold NormalizedButterflyHyp exact ⟨by simpa [ncfg, hA_point] using hAon', by simpa [ncfg, hB_point] using hBon', by simpa [ncfg, hC_point] using hCon', by simpa [ncfg, hD_point] using hDon', huv, hrw, hx_den, hy_den, huniqX_points.2.1, huniqY_points.2.1⟩ · exact ha · simp [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, NormalizedButterflyConfiguration.toButterflyConfiguration, ncfg, hA_point, hB_point, hC_point, hD_point] theorem baseNormalized_hasStrictVerticalNormalizedModel_of_vertical_finite (cfg : BaseNormalizedButterflyConfiguration) (hcfg : BaseNormalizedButterflyHyp cfg) (hA0 : cfg.A 0 = 0) (hC0 : cfg.C 0 ≠ 0) : HasStrictVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := by have ha : cfg.a ≠ 0 := baseNormalized_a_ne cfg hcfg rcases hcfg.1 with ⟨_hradius, _hP, _hQ, hAon, hBon, hCon, hDon, _hmid, hAB, hCD, _hAD, _hBC, _hPX, _hPY⟩ have hdistAB : cfg.A ≠ cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.1 have hdistCD : cfg.C ≠ cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.2 have hAon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.A := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAon have hBon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hBon have hCon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.C := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCon have hDon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hDon have hAB0 : Collinear cfg.A (point 0 0) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAB have hCD0 : Collinear cfg.C (point 0 0) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCD have huniqX : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.A cfg.D (point cfg.x 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.1 have huniqY : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.B cfg.C (point cfg.y 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.2 let vcfg : VerticalNormalizedButterflyConfiguration := { a := cfg.a k := cfg.k n := cfg.C 1 / cfg.C 0 s := cfg.A 1 t := cfg.B 1 r := cfg.C 0 w := cfg.D 0 x := cfg.x y := cfg.y } have hA_point : point 0 vcfg.s = cfg.A := by ext i fin_cases i <;> simp [point, vcfg, hA0] have hA1 : cfg.A 1 ≠ 0 := by exact vertical_coord_ne_zero_of_on_normalized_circle ha (by simpa [vcfg, hA_point] using hAon') have hB0 : cfg.B 0 = 0 := collinear_origin_vertical_x_eq_zero_point hA0 hA1 hAB0 have hB_point : point 0 vcfg.t = cfg.B := by ext i fin_cases i <;> simp [point, vcfg, hB0] have hC_point : point (cfg.C 0) (vcfg.n * cfg.C 0) = cfg.C := by ext i fin_cases i · simp [point] · simp [point, vcfg] field_simp [hC0] have hD_y : cfg.D 1 = vcfg.n * cfg.D 0 := by simpa [vcfg] using collinear_origin_finite_slope_point hC0 hCD0 have hD_point : point (cfg.D 0) (vcfg.n * cfg.D 0) = cfg.D := by ext i fin_cases i · simp [point] · simp [point, hD_y] have hst : vcfg.s ≠ vcfg.t := by simpa [vcfg] using vertical_y_ne_of_point_ne_point hA0 hA1 hAB0 hdistAB have hrw : vcfg.r ≠ vcfg.w := by simpa [vcfg] using finite_slope_x_ne_of_point_ne_point hC0 hCD0 hdistCD have huniqX_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point 0 vcfg.s) (point vcfg.w (vcfg.n * vcfg.w)) (point vcfg.x 0) := by simpa [vcfg, hA_point, hD_point] using huniqX have huniqY_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point 0 vcfg.t) (point vcfg.r (vcfg.n * vcfg.r)) (point vcfg.y 0) := by simpa [vcfg, hB_point, hC_point] using huniqY have hx_den : vcfg.n * vcfg.w - vcfg.s ≠ 0 := by simpa [vcfg] using unique_intersection_base_vertical_finite_den_ne (a := cfg.a) (n := vcfg.n) (s := vcfg.s) (w := vcfg.w) (x := vcfg.x) ha huniqX_points have hy_den : vcfg.n * vcfg.r - vcfg.t ≠ 0 := by simpa [vcfg] using unique_intersection_base_vertical_finite_den_ne (a := cfg.a) (n := vcfg.n) (s := vcfg.t) (w := vcfg.r) (x := vcfg.y) ha huniqY_points refine ⟨vcfg, ?_, ?_⟩ · constructor · unfold VerticalNormalizedButterflyHyp exact ⟨by simpa [vcfg, hA_point] using hAon', by simpa [vcfg, hB_point] using hBon', by simpa [vcfg, hC_point] using hCon', by simpa [vcfg, hD_point] using hDon', hst, hrw, hx_den, hy_den, huniqX_points.2.1, huniqY_points.2.1⟩ · exact ha · simp [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, VerticalNormalizedButterflyConfiguration.toButterflyConfiguration, vcfg, hA_point, hB_point, hC_point, hD_point] theorem baseNormalized_hasStrictReverseVerticalNormalizedModel_of_finite_vertical (cfg : BaseNormalizedButterflyConfiguration) (hcfg : BaseNormalizedButterflyHyp cfg) (hA0 : cfg.A 0 ≠ 0) (hC0 : cfg.C 0 = 0) : HasStrictReverseVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := by have ha : cfg.a ≠ 0 := baseNormalized_a_ne cfg hcfg rcases hcfg.1 with ⟨_hradius, _hP, _hQ, hAon, hBon, hCon, hDon, _hmid, hAB, hCD, _hAD, _hBC, _hPX, _hPY⟩ have hdistAB : cfg.A ≠ cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.1 have hdistCD : cfg.C ≠ cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.2 have hAon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.A := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAon have hBon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hBon have hCon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.C := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCon have hDon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hDon have hAB0 : Collinear cfg.A (point 0 0) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAB have hCD0 : Collinear cfg.C (point 0 0) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCD have huniqX : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.A cfg.D (point cfg.x 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.1 have huniqY : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.B cfg.C (point cfg.y 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.2 let rvcfg : ReverseVerticalNormalizedButterflyConfiguration := { a := cfg.a k := cfg.k m := cfg.A 1 / cfg.A 0 u := cfg.A 0 v := cfg.B 0 s := cfg.C 1 t := cfg.D 1 x := cfg.x y := cfg.y } have hA_point : point (cfg.A 0) (rvcfg.m * cfg.A 0) = cfg.A := by ext i fin_cases i · simp [point] · simp [point, rvcfg] field_simp [hA0] have hB_y : cfg.B 1 = rvcfg.m * cfg.B 0 := by simpa [rvcfg] using collinear_origin_finite_slope_point hA0 hAB0 have hB_point : point (cfg.B 0) (rvcfg.m * cfg.B 0) = cfg.B := by ext i fin_cases i · simp [point] · simp [point, hB_y] have hC_point : point 0 rvcfg.s = cfg.C := by ext i fin_cases i <;> simp [point, rvcfg, hC0] have hC1 : cfg.C 1 ≠ 0 := by exact vertical_coord_ne_zero_of_on_normalized_circle ha (by simpa [rvcfg, hC_point] using hCon') have hD0 : cfg.D 0 = 0 := collinear_origin_vertical_x_eq_zero_point hC0 hC1 hCD0 have hD_point : point 0 rvcfg.t = cfg.D := by ext i fin_cases i <;> simp [point, rvcfg, hD0] have huv : rvcfg.u ≠ rvcfg.v := by simpa [rvcfg] using finite_slope_x_ne_of_point_ne_point hA0 hAB0 hdistAB have hst : rvcfg.s ≠ rvcfg.t := by simpa [rvcfg] using vertical_y_ne_of_point_ne_point hC0 hC1 hCD0 hdistCD have huniqX_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point rvcfg.u (rvcfg.m * rvcfg.u)) (point 0 rvcfg.t) (point rvcfg.x 0) := by simpa [rvcfg, hA_point, hD_point] using huniqX have huniqY_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point rvcfg.v (rvcfg.m * rvcfg.v)) (point 0 rvcfg.s) (point rvcfg.y 0) := by simpa [rvcfg, hB_point, hC_point] using huniqY have hx_den : rvcfg.m * rvcfg.u - rvcfg.t ≠ 0 := by simpa [rvcfg] using unique_intersection_base_finite_vertical_den_ne (a := cfg.a) (m := rvcfg.m) (u := rvcfg.u) (t := rvcfg.t) (x := rvcfg.x) ha huniqX_points have hy_den : rvcfg.m * rvcfg.v - rvcfg.s ≠ 0 := by simpa [rvcfg] using unique_intersection_base_finite_vertical_den_ne (a := cfg.a) (m := rvcfg.m) (u := rvcfg.v) (t := rvcfg.s) (x := rvcfg.y) ha huniqY_points refine ⟨rvcfg, ?_, ?_⟩ · constructor · unfold ReverseVerticalNormalizedButterflyHyp exact ⟨by simpa [rvcfg, hA_point] using hAon', by simpa [rvcfg, hB_point] using hBon', by simpa [rvcfg, hC_point] using hCon', by simpa [rvcfg, hD_point] using hDon', huv, hst, hx_den, hy_den, huniqX_points.2.1, huniqY_points.2.1⟩ · exact ha · simp [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, ReverseVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, rvcfg, hA_point, hB_point, hC_point, hD_point] theorem baseNormalized_hasStrictBothVerticalNormalizedModel_of_both_vertical (cfg : BaseNormalizedButterflyConfiguration) (hcfg : BaseNormalizedButterflyHyp cfg) (hA0 : cfg.A 0 = 0) (hC0 : cfg.C 0 = 0) : HasStrictBothVerticalNormalizedButterflyModel cfg.toButterflyConfiguration := by have ha : cfg.a ≠ 0 := baseNormalized_a_ne cfg hcfg rcases hcfg.1 with ⟨_hradius, _hP, _hQ, hAon, hBon, hCon, hDon, _hmid, hAB, hCD, _hAD, _hBC, _hPX, _hPY⟩ have hdistAB : cfg.A ≠ cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.1 have hdistCD : cfg.C ≠ cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, DistinctChordEndpoints] using hcfg.2.1.2.2 have hAon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.A := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAon have hBon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hBon have hCon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.C := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCon have hDon' : OnCircleSq (point 0 cfg.k) (cfg.a ^ 2 + cfg.k ^ 2) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hDon have hAB0 : Collinear cfg.A (point 0 0) cfg.B := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hAB have hCD0 : Collinear cfg.C (point 0 0) cfg.D := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCD have huniqX : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.A cfg.D (point cfg.x 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.1 have huniqY : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) cfg.B cfg.C (point cfg.y 0) := by simpa [BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hcfg.2.2.2 let bvcfg : BothVerticalNormalizedButterflyConfiguration := { a := cfg.a k := cfg.k s := cfg.A 1 t := cfg.B 1 r := cfg.C 1 w := cfg.D 1 x := cfg.x y := cfg.y } have hA_point : point 0 bvcfg.s = cfg.A := by ext i fin_cases i <;> simp [point, bvcfg, hA0] have hA1 : cfg.A 1 ≠ 0 := by exact vertical_coord_ne_zero_of_on_normalized_circle ha (by simpa [bvcfg, hA_point] using hAon') have hB0 : cfg.B 0 = 0 := collinear_origin_vertical_x_eq_zero_point hA0 hA1 hAB0 have hB_point : point 0 bvcfg.t = cfg.B := by ext i fin_cases i <;> simp [point, bvcfg, hB0] have hC_point : point 0 bvcfg.r = cfg.C := by ext i fin_cases i <;> simp [point, bvcfg, hC0] have hC1 : cfg.C 1 ≠ 0 := by exact vertical_coord_ne_zero_of_on_normalized_circle ha (by simpa [bvcfg, hC_point] using hCon') have hD0 : cfg.D 0 = 0 := collinear_origin_vertical_x_eq_zero_point hC0 hC1 hCD0 have hD_point : point 0 bvcfg.w = cfg.D := by ext i fin_cases i <;> simp [point, bvcfg, hD0] have hst : bvcfg.s ≠ bvcfg.t := by simpa [bvcfg] using vertical_y_ne_of_point_ne_point hA0 hA1 hAB0 hdistAB have hrw : bvcfg.r ≠ bvcfg.w := by simpa [bvcfg] using vertical_y_ne_of_point_ne_point hC0 hC1 hCD0 hdistCD have huniqX_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point 0 bvcfg.s) (point 0 bvcfg.w) (point bvcfg.x 0) := by simpa [bvcfg, hA_point, hD_point] using huniqX have huniqY_points : UniqueIntersection (point (-cfg.a) 0) (point cfg.a 0) (point 0 bvcfg.t) (point 0 bvcfg.r) (point bvcfg.y 0) := by simpa [bvcfg, hB_point, hC_point] using huniqY have hsw : bvcfg.s ≠ bvcfg.w := by simpa [bvcfg] using unique_intersection_base_vertical_vertical_y_ne (a := cfg.a) (s := bvcfg.s) (w := bvcfg.w) (x := bvcfg.x) ha huniqX_points have htr : bvcfg.t ≠ bvcfg.r := by simpa [bvcfg] using unique_intersection_base_vertical_vertical_y_ne (a := cfg.a) (s := bvcfg.t) (w := bvcfg.r) (x := bvcfg.y) ha huniqY_points refine ⟨bvcfg, ?_, ?_⟩ · constructor · unfold BothVerticalNormalizedButterflyHyp exact ⟨by simpa [bvcfg, hA_point] using hAon', by simpa [bvcfg, hB_point] using hBon', by simpa [bvcfg, hC_point] using hCon', by simpa [bvcfg, hD_point] using hDon', hst, hrw, hsw, htr, huniqX_points.2.1, huniqY_points.2.1⟩ · exact ha · simp [BaseNormalizedButterflyConfiguration.toButterflyConfiguration, BothVerticalNormalizedButterflyConfiguration.toButterflyConfiguration, bvcfg, hA_point, hB_point, hC_point, hD_point] theorem baseNormalizedCheckedChartCoverage : BaseNormalizedCheckedChartCoverageStatement := by intro cfg hcfg refine ⟨hcfg.1, ?_⟩ by_cases hA0 : cfg.A 0 = 0 · by_cases hC0 : cfg.C 0 = 0 · exact Or.inr (Or.inr (Or.inr (baseNormalized_hasStrictBothVerticalNormalizedModel_of_both_vertical cfg hcfg hA0 hC0))) · exact Or.inr (Or.inl (baseNormalized_hasStrictVerticalNormalizedModel_of_vertical_finite cfg hcfg hA0 hC0)) · by_cases hC0 : cfg.C 0 = 0 · exact Or.inr (Or.inr (Or.inl (baseNormalized_hasStrictReverseVerticalNormalizedModel_of_finite_vertical cfg hcfg hA0 hC0))) · exact Or.inl (baseNormalized_hasStrictNormalizedModel_of_finite_finite cfg hcfg hA0 hC0) theorem baseNormalizedButterflyTheorem : BaseNormalizedButterflyTheoremStatement := by intro cfg hcfg exact (strictCheckedChartModelButterflyTheorem cfg.toButterflyConfiguration (baseNormalizedCheckedChartCoverage cfg hcfg)).1 theorem baseNormalizedConfiguration_hyp (cfg : ButterflyConfiguration) (hcfg : NondegenerateButterflyHyp cfg) : BaseNormalizedButterflyHyp (baseNormalizedConfiguration cfg) := by rcases hcfg with ⟨hbutterfly, hdistinct, huniqX, huniqY⟩ rcases hbutterfly with ⟨_hradius, hP, hQ, hA, hB, hC, hD, hmid, hAB, hCD, hAD, hBC, hPX, hPY⟩ have hpq : cfg.P ≠ cfg.Q := hdistinct.1 have hqm : cfg.Q ≠ cfg.M := right_ne_midpoint_of_left_ne_right hmid hpq have hleft : baseNormalize cfg.M cfg.Q cfg.P = point (-1) 0 := baseNormalize_left_of_midpoint hmid hpq have hright : baseNormalize cfg.M cfg.Q cfg.Q = point 1 0 := baseNormalize_right hqm have horigin : baseNormalize cfg.M cfg.Q cfg.M = point 0 0 := baseNormalize_self cfg.M cfg.Q have hX_col : Collinear (baseNormalize cfg.M cfg.Q cfg.P) (baseNormalize cfg.M cfg.Q cfg.Q) (baseNormalize cfg.M cfg.Q cfg.X) := (collinear_baseNormalize_iff hqm).2 hPX have hY_col : Collinear (baseNormalize cfg.M cfg.Q cfg.P) (baseNormalize cfg.M cfg.Q cfg.Q) (baseNormalize cfg.M cfg.Q cfg.Y) := (collinear_baseNormalize_iff hqm).2 hPY have hX_y : (baseNormalize cfg.M cfg.Q cfg.X) 1 = 0 := by exact collinear_base_y_eq_zero (a := 1) (by norm_num) (by simpa [hleft, hright] using hX_col) have hY_y : (baseNormalize cfg.M cfg.Q cfg.Y) 1 = 0 := by exact collinear_base_y_eq_zero (a := 1) (by norm_num) (by simpa [hleft, hright] using hY_col) have hX_point : baseNormalize cfg.M cfg.Q cfg.X = point ((baseNormalize cfg.M cfg.Q cfg.X) 0) 0 := by ext i fin_cases i · simp [point] · simpa [point] using hX_y have hY_point : baseNormalize cfg.M cfg.Q cfg.Y = point ((baseNormalize cfg.M cfg.Q cfg.Y) 0) 0 := by ext i fin_cases i · simp [point] · simpa [point] using hY_y have hX_point_rev : point ((baseNormalize cfg.M cfg.Q cfg.X) 0) 0 = baseNormalize cfg.M cfg.Q cfg.X := hX_point.symm have hY_point_rev : point ((baseNormalize cfg.M cfg.Q cfg.Y) 0) 0 = baseNormalize cfg.M cfg.Q cfg.Y := hY_point.symm unfold BaseNormalizedButterflyHyp NondegenerateButterflyHyp constructor · unfold ButterflyHyp constructor · change 0 < (1 : ℝ) ^ 2 + ((baseNormalize cfg.M cfg.Q cfg.center) 1) ^ 2 positivity constructor · simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, hleft] using onCircleSq_baseNormalize_normalized hqm hmid hP hQ hP constructor · simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, hright] using onCircleSq_baseNormalize_normalized hqm hmid hP hQ hQ constructor · simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using onCircleSq_baseNormalize_normalized hqm hmid hP hQ hA constructor · simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using onCircleSq_baseNormalize_normalized hqm hmid hP hQ hB constructor · simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using onCircleSq_baseNormalize_normalized hqm hmid hP hQ hC constructor · simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using onCircleSq_baseNormalize_normalized hqm hmid hP hQ hD constructor · unfold IsMidpoint ext i fin_cases i <;> norm_num [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, midpoint, point] constructor · have hAB' := (collinear_baseNormalize_iff hqm).2 hAB simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, horigin] using hAB' constructor · have hCD' := (collinear_baseNormalize_iff hqm).2 hCD simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, horigin] using hCD' constructor · have hAD' := (collinear_baseNormalize_iff hqm).2 hAD simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, hX_point_rev] using hAD' constructor · have hBC' := (collinear_baseNormalize_iff hqm).2 hBC simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, hY_point_rev] using hBC' constructor · norm_num [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] · norm_num [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, Collinear, det2, vsub, point] constructor · unfold DistinctChordEndpoints constructor · intro hpq' have h0 := congrFun hpq' 0 norm_num [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, point] at h0 constructor · intro hABeq exact hdistinct.2.1 (baseNormalize_injective hqm (by simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hABeq)) · intro hCDeq exact hdistinct.2.2 (baseNormalize_injective hqm (by simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration] using hCDeq)) constructor · have huniqX' := uniqueIntersection_baseNormalize hqm huniqX simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, hleft, hright, hX_point_rev] using huniqX' · have huniqY' := uniqueIntersection_baseNormalize hqm huniqY simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, hleft, hright, hY_point_rev] using huniqY' theorem nondegenerateButterflyTheorem : NondegenerateButterflyTheoremStatement := by intro cfg hcfg have hbase := baseNormalizedConfiguration_hyp cfg hcfg have hnorm := baseNormalizedButterflyTheorem (baseNormalizedConfiguration cfg) hbase rcases hcfg with ⟨hbutterfly, hdistinct, _huniqX, _huniqY⟩ rcases hbutterfly with ⟨_hradius, _hP, _hQ, _hA, _hB, _hC, _hD, hmid, _hAB, _hCD, _hAD, _hBC, hPX, hPY⟩ have hpq : cfg.P ≠ cfg.Q := hdistinct.1 have hqm : cfg.Q ≠ cfg.M := right_ne_midpoint_of_left_ne_right hmid hpq have hleft : baseNormalize cfg.M cfg.Q cfg.P = point (-1) 0 := baseNormalize_left_of_midpoint hmid hpq have hright : baseNormalize cfg.M cfg.Q cfg.Q = point 1 0 := baseNormalize_right hqm have horigin : baseNormalize cfg.M cfg.Q cfg.M = point 0 0 := baseNormalize_self cfg.M cfg.Q have hX_col : Collinear (baseNormalize cfg.M cfg.Q cfg.P) (baseNormalize cfg.M cfg.Q cfg.Q) (baseNormalize cfg.M cfg.Q cfg.X) := (collinear_baseNormalize_iff hqm).2 hPX have hY_col : Collinear (baseNormalize cfg.M cfg.Q cfg.P) (baseNormalize cfg.M cfg.Q cfg.Q) (baseNormalize cfg.M cfg.Q cfg.Y) := (collinear_baseNormalize_iff hqm).2 hPY have hX_y : (baseNormalize cfg.M cfg.Q cfg.X) 1 = 0 := by exact collinear_base_y_eq_zero (a := 1) (by norm_num) (by simpa [hleft, hright] using hX_col) have hY_y : (baseNormalize cfg.M cfg.Q cfg.Y) 1 = 0 := by exact collinear_base_y_eq_zero (a := 1) (by norm_num) (by simpa [hleft, hright] using hY_col) have hX_point : point ((baseNormalize cfg.M cfg.Q cfg.X) 0) 0 = baseNormalize cfg.M cfg.Q cfg.X := by ext i fin_cases i · simp [point] · simpa [point] using hX_y.symm have hY_point : point ((baseNormalize cfg.M cfg.Q cfg.Y) 0) 0 = baseNormalize cfg.M cfg.Q cfg.Y := by ext i fin_cases i · simp [point] · simpa [point] using hY_y.symm have hnorm' : IsMidpoint (baseNormalize cfg.M cfg.Q cfg.M) (baseNormalize cfg.M cfg.Q cfg.X) (baseNormalize cfg.M cfg.Q cfg.Y) := by simpa [baseNormalizedConfiguration, BaseNormalizedButterflyConfiguration.toButterflyConfiguration, horigin, hX_point, hY_point] using hnorm exact isMidpoint_of_baseNormalize hqm hnorm' theorem strictNormalizedModelButterflyHyp_to_nondegenerateButterflyHyp {cfg : ButterflyConfiguration} (hcfg : StrictNormalizedModelButterflyHyp cfg) : NondegenerateButterflyHyp cfg := by have hconcl := strictNormalizedModelButterflyTheorem cfg hcfg exact ⟨hcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ theorem strictVerticalNormalizedModelButterflyHyp_to_nondegenerateButterflyHyp {cfg : ButterflyConfiguration} (hcfg : StrictVerticalNormalizedModelButterflyHyp cfg) : NondegenerateButterflyHyp cfg := by have hconcl := strictVerticalNormalizedModelButterflyTheorem cfg hcfg exact ⟨hcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ theorem strictReverseVerticalNormalizedModelButterflyHyp_to_nondegenerateButterflyHyp {cfg : ButterflyConfiguration} (hcfg : StrictReverseVerticalNormalizedModelButterflyHyp cfg) : NondegenerateButterflyHyp cfg := by have hconcl := strictReverseVerticalNormalizedModelButterflyTheorem cfg hcfg exact ⟨hcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ theorem strictBothVerticalNormalizedModelButterflyHyp_to_nondegenerateButterflyHyp {cfg : ButterflyConfiguration} (hcfg : StrictBothVerticalNormalizedModelButterflyHyp cfg) : NondegenerateButterflyHyp cfg := by have hconcl := strictBothVerticalNormalizedModelButterflyTheorem cfg hcfg exact ⟨hcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ theorem strictCheckedChartModelButterflyHyp_to_nondegenerateButterflyHyp {cfg : ButterflyConfiguration} (hcfg : StrictCheckedChartModelButterflyHyp cfg) : NondegenerateButterflyHyp cfg := by have hconcl := strictCheckedChartModelButterflyTheorem cfg hcfg exact ⟨hcfg.1, hconcl.2.1, hconcl.2.2.1, hconcl.2.2.2⟩ /-- A degenerate configuration allowed by the current v0 hypotheses. -/ def sameChordDegenerateConfiguration : ButterflyConfiguration where center := point 0 0 radiusSq := 1 M := point 0 0 P := point (-1) 0 Q := point 1 0 A := point (-1) 0 B := point 1 0 C := point (-1) 0 D := point 1 0 X := point (-1) 0 Y := point (-1) 0 theorem sameChordDegenerateConfiguration_hyp : ButterflyHyp sameChordDegenerateConfiguration := by unfold ButterflyHyp constructor · norm_num [sameChordDegenerateConfiguration] constructor · norm_num [sameChordDegenerateConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · unfold IsMidpoint ext i fin_cases i <;> norm_num [sameChordDegenerateConfiguration, midpoint, point] constructor · norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point] constructor · norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point] · norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point] theorem sameChordDegenerateConfiguration_not_conclusion : ¬ IsMidpoint sameChordDegenerateConfiguration.M sameChordDegenerateConfiguration.X sameChordDegenerateConfiguration.Y := by unfold sameChordDegenerateConfiguration IsMidpoint midpoint point intro h have h0 := congrFun h 0 norm_num at h0 theorem not_butterflyTheoremStatement_currentHyp : ¬ ButterflyTheoremStatement := by intro h exact sameChordDegenerateConfiguration_not_conclusion (h sameChordDegenerateConfiguration sameChordDegenerateConfiguration_hyp) theorem normalized_toButterflyConfiguration_ne_sameChordDegenerateConfiguration (cfg : NormalizedButterflyConfiguration) (hcfg : NormalizedButterflyHyp cfg) : cfg.toButterflyConfiguration ≠ sameChordDegenerateConfiguration := by intro hsame have hmid := normalized_toButterflyConfiguration_conclusion cfg hcfg rw [hsame] at hmid exact sameChordDegenerateConfiguration_not_conclusion hmid theorem sameChordDegenerateConfiguration_not_hasNormalizedButterflyModel : ¬ HasNormalizedButterflyModel sameChordDegenerateConfiguration := by intro hmodel exact sameChordDegenerateConfiguration_not_conclusion (hasNormalizedButterflyModel_conclusion hmodel) theorem sameChordDegenerateConfiguration_not_normalizedModelButterflyHyp : ¬ NormalizedModelButterflyHyp sameChordDegenerateConfiguration := by intro hcfg exact sameChordDegenerateConfiguration_not_hasNormalizedButterflyModel hcfg.2 theorem sameChordDegenerateConfiguration_not_hasStrictNormalizedButterflyModel : ¬ HasStrictNormalizedButterflyModel sameChordDegenerateConfiguration := by intro hmodel exact sameChordDegenerateConfiguration_not_conclusion (hasStrictNormalizedButterflyModel_conclusion hmodel).1 theorem sameChordDegenerateConfiguration_not_strictNormalizedModelButterflyHyp : ¬ StrictNormalizedModelButterflyHyp sameChordDegenerateConfiguration := by intro hcfg exact sameChordDegenerateConfiguration_not_hasStrictNormalizedButterflyModel hcfg.2 theorem sameChordDegenerateConfiguration_not_uniqueIntersectionX : ¬ UniqueIntersection sameChordDegenerateConfiguration.P sameChordDegenerateConfiguration.Q sameChordDegenerateConfiguration.A sameChordDegenerateConfiguration.D sameChordDegenerateConfiguration.X := by intro huniq have hq : sameChordDegenerateConfiguration.Q = sameChordDegenerateConfiguration.X := by exact huniq.2.2 sameChordDegenerateConfiguration.Q (by norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point]) (by norm_num [sameChordDegenerateConfiguration, Collinear, det2, vsub, point]) have h0 := congrFun hq 0 norm_num [sameChordDegenerateConfiguration, point] at h0 theorem sameChordDegenerateConfiguration_not_nondegenerateButterflyHyp : ¬ NondegenerateButterflyHyp sameChordDegenerateConfiguration := by intro hcfg exact sameChordDegenerateConfiguration_not_uniqueIntersectionX hcfg.2.2.1 noncomputable def normalizedExampleConfiguration : NormalizedButterflyConfiguration where a := 5 k := 0 m := 3 / 4 n := -(4 / 3) u := 4 v := -4 r := 3 w := -3 x := 25 y := -25 theorem normalizedExampleConfiguration_hyp : NormalizedButterflyHyp normalizedExampleConfiguration := by unfold NormalizedButterflyHyp constructor · norm_num [normalizedExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [normalizedExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [normalizedExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [normalizedExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [normalizedExampleConfiguration] constructor · norm_num [normalizedExampleConfiguration] constructor · norm_num [normalizedExampleConfiguration] constructor · norm_num [normalizedExampleConfiguration] constructor · norm_num [normalizedExampleConfiguration, Collinear, det2, vsub, point] · norm_num [normalizedExampleConfiguration, Collinear, det2, vsub, point] theorem normalizedExampleEmbeddedButterfly : ButterflyHyp normalizedExampleConfiguration.toButterflyConfiguration ∧ IsMidpoint normalizedExampleConfiguration.toButterflyConfiguration.M normalizedExampleConfiguration.toButterflyConfiguration.X normalizedExampleConfiguration.toButterflyConfiguration.Y := normalizedEmbeddedButterflyTheorem normalizedExampleConfiguration normalizedExampleConfiguration_hyp theorem normalizedExample_hasNormalizedButterflyModel : HasNormalizedButterflyModel normalizedExampleConfiguration.toButterflyConfiguration := normalized_toButterflyConfiguration_hasNormalizedButterflyModel normalizedExampleConfiguration normalizedExampleConfiguration_hyp theorem normalizedExample_normalizedModelButterflyHyp : NormalizedModelButterflyHyp normalizedExampleConfiguration.toButterflyConfiguration := hasNormalizedButterflyModel_to_normalizedModelButterflyHyp normalizedExample_hasNormalizedButterflyModel theorem normalizedExample_uniqueIntersections : UniqueIntersection normalizedExampleConfiguration.toButterflyConfiguration.P normalizedExampleConfiguration.toButterflyConfiguration.Q normalizedExampleConfiguration.toButterflyConfiguration.A normalizedExampleConfiguration.toButterflyConfiguration.D normalizedExampleConfiguration.toButterflyConfiguration.X ∧ UniqueIntersection normalizedExampleConfiguration.toButterflyConfiguration.P normalizedExampleConfiguration.toButterflyConfiguration.Q normalizedExampleConfiguration.toButterflyConfiguration.B normalizedExampleConfiguration.toButterflyConfiguration.C normalizedExampleConfiguration.toButterflyConfiguration.Y := normalized_toButterflyConfiguration_uniqueIntersections normalizedExampleConfiguration normalizedExampleConfiguration_hyp (by norm_num [normalizedExampleConfiguration]) theorem normalizedExample_strictNormalizedButterflyHyp : StrictNormalizedButterflyHyp normalizedExampleConfiguration := ⟨normalizedExampleConfiguration_hyp, by norm_num [normalizedExampleConfiguration]⟩ theorem normalizedExample_hasStrictNormalizedButterflyModel : HasStrictNormalizedButterflyModel normalizedExampleConfiguration.toButterflyConfiguration := normalized_toButterflyConfiguration_hasStrictNormalizedButterflyModel normalizedExampleConfiguration normalizedExample_strictNormalizedButterflyHyp theorem normalizedExample_strictNormalizedModelButterflyHyp : StrictNormalizedModelButterflyHyp normalizedExampleConfiguration.toButterflyConfiguration := ⟨normalizedExampleEmbeddedButterfly.1, normalizedExample_hasStrictNormalizedButterflyModel⟩ theorem normalizedExample_strictNormalizedModelButterflyConclusion : StrictNormalizedModelButterflyConclusion normalizedExampleConfiguration.toButterflyConfiguration := strictNormalizedModelButterflyTheorem normalizedExampleConfiguration.toButterflyConfiguration normalizedExample_strictNormalizedModelButterflyHyp noncomputable def verticalAuxiliaryExampleConfiguration : ButterflyConfiguration where center := point 0 0 radiusSq := 25 M := point 0 0 P := point (-5) 0 Q := point 5 0 A := point 0 5 B := point 0 (-5) C := point 4 3 D := point (-4) (-3) X := point (-(5 / 2)) 0 Y := point (5 / 2) 0 theorem verticalAuxiliaryExample_hyp : ButterflyHyp verticalAuxiliaryExampleConfiguration := by unfold ButterflyHyp constructor · norm_num [verticalAuxiliaryExampleConfiguration] constructor · norm_num [verticalAuxiliaryExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, OnCircleSq, sqDist, sqNorm, vsub, point] constructor · unfold IsMidpoint ext i fin_cases i <;> norm_num [verticalAuxiliaryExampleConfiguration, midpoint, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] theorem verticalAuxiliaryExample_distinctChordEndpoints : DistinctChordEndpoints verticalAuxiliaryExampleConfiguration := by unfold DistinctChordEndpoints constructor · intro h have h0 := congrFun h 0 norm_num [verticalAuxiliaryExampleConfiguration, point] at h0 constructor · intro h have h1 := congrFun h 1 norm_num [verticalAuxiliaryExampleConfiguration, point] at h1 · intro h have h0 := congrFun h 0 norm_num [verticalAuxiliaryExampleConfiguration, point] at h0 theorem verticalAuxiliaryExample_uniqueX : UniqueIntersection verticalAuxiliaryExampleConfiguration.P verticalAuxiliaryExampleConfiguration.Q verticalAuxiliaryExampleConfiguration.A verticalAuxiliaryExampleConfiguration.D verticalAuxiliaryExampleConfiguration.X := by unfold UniqueIntersection constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] · intro z hz_base hz_line have hz_y : z 1 = 0 := by exact collinear_base_y_eq_zero (a := 5) (by norm_num) (by simpa [verticalAuxiliaryExampleConfiguration] using hz_base) have hline : z 0 = -(5 / 2) := by norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] at hz_line rw [hz_y] at hz_line norm_num at hz_line nlinarith ext i fin_cases i · simp [verticalAuxiliaryExampleConfiguration, point] nlinarith · simpa [verticalAuxiliaryExampleConfiguration, point] using hz_y theorem verticalAuxiliaryExample_uniqueY : UniqueIntersection verticalAuxiliaryExampleConfiguration.P verticalAuxiliaryExampleConfiguration.Q verticalAuxiliaryExampleConfiguration.B verticalAuxiliaryExampleConfiguration.C verticalAuxiliaryExampleConfiguration.Y := by unfold UniqueIntersection constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] constructor · norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] · intro z hz_base hz_line have hz_y : z 1 = 0 := by exact collinear_base_y_eq_zero (a := 5) (by norm_num) (by simpa [verticalAuxiliaryExampleConfiguration] using hz_base) have hline : z 0 = 5 / 2 := by norm_num [verticalAuxiliaryExampleConfiguration, Collinear, det2, vsub, point] at hz_line rw [hz_y] at hz_line norm_num at hz_line nlinarith ext i fin_cases i · simp [verticalAuxiliaryExampleConfiguration, point] nlinarith · simpa [verticalAuxiliaryExampleConfiguration, point] using hz_y theorem verticalAuxiliaryExample_nondegenerateHyp : NondegenerateButterflyHyp verticalAuxiliaryExampleConfiguration := ⟨verticalAuxiliaryExample_hyp, verticalAuxiliaryExample_distinctChordEndpoints, verticalAuxiliaryExample_uniqueX, verticalAuxiliaryExample_uniqueY⟩ theorem verticalAuxiliaryExample_conclusion : IsMidpoint verticalAuxiliaryExampleConfiguration.M verticalAuxiliaryExampleConfiguration.X verticalAuxiliaryExampleConfiguration.Y := by unfold IsMidpoint ext i fin_cases i <;> norm_num [verticalAuxiliaryExampleConfiguration, midpoint, point] theorem verticalAuxiliaryExample_not_hasStrictNormalizedButterflyModel : ¬ HasStrictNormalizedButterflyModel verticalAuxiliaryExampleConfiguration := by intro hmodel rcases hmodel with ⟨ncfg, _hncfg, hEq⟩ have hA := congrArg ButterflyConfiguration.A hEq have hx := congrFun hA 0 have hy := congrFun hA 1 norm_num [verticalAuxiliaryExampleConfiguration, NormalizedButterflyConfiguration.toButterflyConfiguration, point] at hx hy rw [← hx] at hy norm_num at hy end AtlasKnownTheorems.ButterflyTheorem