import Definitions.Def_WeierstrassCurve_ReductionMap set_option autoImplicit false open IsLocalRing namespace ValuationSubring variable {L : Type*} [Field L] (A : ValuationSubring L) theorem add_notMem {x a : L} (hx : x ∉ A) (ha : a ∈ A) : x + a ∉ A := fun h => hx (by simpa using A.toSubring.sub_mem h ha) theorem mul_notMem {x y : L} (hx : x ∉ A) (hy : y ∉ A) : x * y ∉ A := fun h => by rcases A.mem_or_inv_mem x with hx' | hx' · exact hx hx' · have hx0 : x ≠ 0 := fun h0 => hx (h0 ▸ A.zero_mem) exact hy (by simpa [inv_mul_cancel_left₀ hx0] using A.toSubring.mul_mem hx' h) theorem div_notMem {a b : L} (ha' : a ∉ A.nonunits) (hb : b ∈ A.nonunits) (hb0 : b ≠ 0) : a / b ∉ A := fun h => by refine ha' ?_ rw [show a = a / b * b from (div_mul_cancel₀ a hb0).symm] exact A.mul_mem_nonunits h hb theorem coe_mem_nonunits_iff_residue_eq_zero (e : A) : (e : L) ∈ A.nonunits ↔ residue A e = 0 := by rw [A.coe_mem_nonunits_iff, residue_eq_zero_iff] end ValuationSubring namespace WeierstrassCurve namespace Affine theorem sub_mul_sub_negY {R : Type*} [CommRing R] {V : Affine R} {x₁ x₂ y₁ y₂ : R} (h₁ : V.Equation x₁ y₁) (h₂ : V.Equation x₂ y₂) : (y₁ - y₂) * (y₁ - V.negY x₂ y₂) = (x₁ - x₂) * (x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 + V.a₂ * (x₁ + x₂) + V.a₄ - V.a₁ * y₁) := by rw [equation_iff] at h₁ h₂ rw [negY] linear_combination h₁ - h₂ end Affine variable {L : Type*} [Field L] {A : ValuationSubring L} (W : WeierstrassCurve A) theorem Affine.notMem_nonunits_of_sub_negY_mem_nonunits (hΔ : (W.map (residue A)).Δ ≠ 0) {x y : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∈ A) (hY : y - (W.map A.subtype).toAffine.negY x y ∈ A.nonunits) : 3 * x ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y ∉ A.nonunits := by have hy : y ∈ A := Affine.Y_mem_of_X_mem W h hx set eX : A := 3 * ⟨x, hx⟩ ^ 2 + 2 * W.a₂ * ⟨x, hx⟩ + W.a₄ - W.a₁ * ⟨y, hy⟩ with heX set eY : A := ⟨y, hy⟩ - W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩ with heY have hcoeX : (eX : L) = 3 * x ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y := by push_cast [heX] rfl have hcoeY : (eY : L) = y - (W.map A.subtype).toAffine.negY x y := by have h1 : ((W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩ : A) : L) = (W.map A.subtype).toAffine.negY x y := (Affine.map_negY A.subtype (⟨x, hx⟩ : A) (⟨y, hy⟩ : A)).symm rw [heY] push_cast rw [h1] have hns := Affine.nonsingular_residue W hΔ (x := ⟨x, hx⟩) (y := ⟨y, hy⟩) h rw [Affine.nonsingular_iff] at hns have hY0 : residue A eY = 0 := by rw [← A.coe_mem_nonunits_iff_residue_eq_zero, hcoeY] exact hY have hX0 : residue A eX ≠ 0 := by rcases hns.2 with hX | hY' · intro h0 apply hX rw [heX] at h0 simp only [map_sub, map_add, map_mul, map_pow, map_ofNat] at h0 show residue A W.a₁ * residue A ⟨y, hy⟩ = 3 * residue A ⟨x, hx⟩ ^ 2 + 2 * residue A W.a₂ * residue A ⟨x, hx⟩ + residue A W.a₄ linear_combination -h0 · exact absurd (by show residue A ⟨y, hy⟩ = -residue A ⟨y, hy⟩ - residue A W.a₁ * residue A ⟨x, hx⟩ - residue A W.a₃ rw [heY] at hY0 simp only [Affine.negY, map_sub, map_neg, map_mul] at hY0 linear_combination hY0) hY' rw [← hcoeX, A.coe_mem_nonunits_iff_residue_eq_zero] exact hX0 section Slope variable [DecidableEq L] theorem Affine.slope_notMem_of_sub_mem_nonunits (hΔ : (W.map (residue A)).Δ ≠ 0) {x₁ x₂ y₁ y₂ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∈ A) (hPQ : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) (hxx : x₁ - x₂ ∈ A.nonunits) (hyy : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits) : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∉ A := by have hy₁ : y₁ ∈ A := Affine.Y_mem_of_X_mem W h₁ hx₁ have hy₂ : y₂ ∈ A := Affine.Y_mem_of_X_mem W h₂ hx₂ have ha₁ : (W.map A.subtype).toAffine.a₁ ∈ A := SetLike.coe_mem W.a₁ have ha₂ : (W.map A.subtype).toAffine.a₂ ∈ A := SetLike.coe_mem W.a₂ have ha₃ : (W.map A.subtype).toAffine.a₃ ∈ A := SetLike.coe_mem W.a₃ have ha₄ : (W.map A.subtype).toAffine.a₄ ∈ A := SetLike.coe_mem W.a₄ have hnegY : (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A := by rw [Affine.negY] exact A.toSubring.sub_mem (A.toSubring.sub_mem (A.toSubring.neg_mem hy₂) (A.toSubring.mul_mem ha₁ hx₂)) ha₃ by_cases hx : x₁ = x₂ · have hy : y₁ ≠ (W.map A.subtype).toAffine.negY x₂ y₂ := fun h => hPQ ⟨hx, h⟩ have hy12 : y₁ = y₂ := (Affine.Y_eq_of_X_eq h₁ h₂ hx).resolve_right hy rw [Affine.slope_of_Y_ne hx hy] have hden : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ ∈ A.nonunits := by rwa [← hx, ← hy12] at hyy have hden0 : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ ≠ 0 := by rw [sub_ne_zero] intro hcon exact hy (by rw [← hx, ← hy12]; exact hcon) have hnum := Affine.notMem_nonunits_of_sub_negY_mem_nonunits W hΔ h₁ hx₁ hden exact A.div_notMem hnum hden hden0 · by_cases hyy' : y₁ - y₂ ∈ A.nonunits · rw [Affine.slope_of_X_ne hx] have hden : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ ∈ A.nonunits := by have key : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ = (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) + (y₁ - y₂) + (W.map A.subtype).toAffine.a₁ * (x₁ - x₂) := by simp only [Affine.negY] ring rw [key] exact add_mem (add_mem hyy hyy') (A.mul_mem_nonunits ha₁ hxx) have hnum := Affine.notMem_nonunits_of_sub_negY_mem_nonunits W hΔ h₁ hx₁ hden set N : L := x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 + (W.map A.subtype).toAffine.a₂ * (x₁ + x₂) + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ with hN have hNunit : N ∉ A.nonunits := by intro hmem apply hnum have key : 3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ = N - (x₁ + x₁ + x₂ + (W.map A.subtype).toAffine.a₂) * -(x₁ - x₂) := by rw [hN]; ring rw [key] exact sub_mem hmem (A.mul_mem_nonunits (add_mem (add_mem (add_mem hx₁ hx₁) hx₂) ha₂) (neg_mem hxx)) have hd0 : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ≠ 0 := by intro hd apply hNunit rw [hN] have hid := Affine.sub_mul_sub_negY h₁ h₂ rw [hd, mul_zero] at hid rcases mul_eq_zero.mp hid.symm with h | h · exact absurd (sub_eq_zero.mp h) hx · rw [h] exact zero_mem _ have hslope : (y₁ - y₂) / (x₁ - x₂) = N / (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) := by rw [div_eq_div_iff (sub_ne_zero.mpr hx) hd0, hN] linear_combination Affine.sub_mul_sub_negY h₁ h₂ rw [hslope] exact A.div_notMem hNunit hyy hd0 · rw [Affine.slope_of_X_ne hx] exact A.div_notMem hyy' hxx (sub_ne_zero.mpr hx) theorem Affine.addX_notMem_of_sub_mem_nonunits (hΔ : (W.map (residue A)).Δ ≠ 0) {x₁ x₂ y₁ y₂ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∈ A) (hPQ : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) (hxx : x₁ - x₂ ∈ A.nonunits) (hyy : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits) : (W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∉ A := by have hℓ := Affine.slope_notMem_of_sub_mem_nonunits W hΔ h₁ h₂ hx₁ hx₂ hPQ hxx hyy set ℓ : L := (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ have ha₁ : (W.map A.subtype).toAffine.a₁ ∈ A := SetLike.coe_mem W.a₁ have ha₂ : (W.map A.subtype).toAffine.a₂ ∈ A := SetLike.coe_mem W.a₂ rw [show (W.map A.subtype).toAffine.addX x₁ x₂ ℓ = ℓ * (ℓ + (W.map A.subtype).toAffine.a₁) + (-(W.map A.subtype).toAffine.a₂ - x₁ - x₂) from by rw [Affine.addX]; ring] exact A.add_notMem (A.mul_notMem hℓ (by simpa [add_comm] using A.add_notMem hℓ ha₁)) (A.toSubring.sub_mem (A.toSubring.sub_mem (A.toSubring.neg_mem ha₂) hx₁) hx₂) end Slope end WeierstrassCurve namespace ValuationSubring variable {L : Type*} [Field L] (A : ValuationSubring L) theorem ne_zero_of_notMem_nonunits {a : L} (ha : a ∉ A.nonunits) : a ≠ 0 := fun h => ha (h ▸ A.nonunits.zero_mem) theorem inv_mem_of_notMem_nonunits {a : L} (ha : a ∉ A.nonunits) : a⁻¹ ∈ A := by rw [mem_nonunits_iff_or] at ha push_neg at ha exact ha.2 theorem inv_mem_nonunits_of_notMem {a : L} (ha : a ∉ A) : a⁻¹ ∈ A.nonunits := A.inv_mem_nonunits_iff.mpr (Or.inr ha) theorem inv_mem_of_notMem {a : L} (ha : a ∉ A) : a⁻¹ ∈ A := A.nonunits_subset (A.inv_mem_nonunits_of_notMem ha) theorem add_notMem_nonunits {a b : L} (ha : a ∉ A.nonunits) (hb : b ∈ A.nonunits) : a + b ∉ A.nonunits := fun h => ha (by simpa using A.nonunits.sub_mem h hb) theorem mul_notMem_nonunits {a b : L} (ha : a ∉ A.nonunits) (hb : b ∉ A.nonunits) : a * b ∉ A.nonunits := by intro h have ha0 := A.ne_zero_of_notMem_nonunits ha have hb0 := A.ne_zero_of_notMem_nonunits hb rw [mem_nonunits_iff_or] at h rcases h with h | h · exact (mul_ne_zero ha0 hb0) h · exact h (mul_inv_rev a b ▸ A.toSubring.mul_mem (A.inv_mem_of_notMem_nonunits hb) (A.inv_mem_of_notMem_nonunits ha)) theorem inv_notMem_nonunits_of_notMem_nonunits {a : L} (ha : a ∈ A) (ha' : a ∉ A.nonunits) : a⁻¹ ∉ A.nonunits := by rw [mem_nonunits_iff_or] push_neg exact ⟨inv_ne_zero (A.ne_zero_of_notMem_nonunits ha'), by rwa [inv_inv]⟩ theorem one_add_notMem_nonunits {a : L} (ha : a ∈ A.nonunits) : 1 + a ∉ A.nonunits := A.add_notMem_nonunits A.one_notMem_nonunits ha theorem natCast_mem_nonunits_iff_residue_eq_zero (n : ℕ) : (n : L) ∈ A.nonunits ↔ (n : ResidueField A) = 0 := by have h1 : ((n : A) : L) = (n : L) := by push_cast; rfl have h2 : residue A (n : A) = (n : ResidueField A) := map_natCast (residue A) n rw [← h1, A.coe_mem_nonunits_iff_residue_eq_zero, h2] end ValuationSubring namespace WeierstrassCurve open ValuationSubring variable {L : Type*} [Field L] {A : ValuationSubring L} variable (W : WeierstrassCurve A) namespace Affine theorem cubic_inv_notMem_nonunits {x : L} (hx : x ∉ A) : 1 + (W.map A.subtype).toAffine.a₂ * x⁻¹ + (W.map A.subtype).toAffine.a₄ * (x⁻¹ * x⁻¹) + (W.map A.subtype).toAffine.a₆ * (x⁻¹ * x⁻¹ * x⁻¹) ∉ A.nonunits := by have hxinv : x⁻¹ ∈ A.nonunits := A.inv_mem_nonunits_of_notMem hx have ha₂ : (W.map A.subtype).toAffine.a₂ ∈ A := SetLike.coe_mem W.a₂ have ha₄ : (W.map A.subtype).toAffine.a₄ ∈ A := SetLike.coe_mem W.a₄ have ha₆ : (W.map A.subtype).toAffine.a₆ ∈ A := SetLike.coe_mem W.a₆ rw [add_assoc, add_assoc] refine A.one_add_notMem_nonunits (add_mem (A.mul_mem_nonunits ha₂ hxinv) (add_mem ?_ ?_)) · exact A.mul_mem_nonunits ha₄ (A.nonunits.mul_mem hxinv hxinv) · exact A.mul_mem_nonunits ha₆ (A.nonunits.mul_mem (A.nonunits.mul_mem hxinv hxinv) hxinv) theorem rhs_eq_cubic_mul {x : L} (hx : x ∉ A) : x ^ 3 + (W.map A.subtype).toAffine.a₂ * x ^ 2 + (W.map A.subtype).toAffine.a₄ * x + (W.map A.subtype).toAffine.a₆ = x ^ 3 * (1 + (W.map A.subtype).toAffine.a₂ * x⁻¹ + (W.map A.subtype).toAffine.a₄ * (x⁻¹ * x⁻¹) + (W.map A.subtype).toAffine.a₆ * (x⁻¹ * x⁻¹ * x⁻¹)) := by have hx0 : x ≠ 0 := fun h => hx (h ▸ A.zero_mem) field_simp theorem Y_ne_zero_of_X_notMem {x y : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∉ A) : y ≠ 0 := by rintro rfl rw [equation_iff] at h have h0 : x ^ 3 + (W.map A.subtype).toAffine.a₂ * x ^ 2 + (W.map A.subtype).toAffine.a₄ * x + (W.map A.subtype).toAffine.a₆ = 0 := by linear_combination -h rw [rhs_eq_cubic_mul W hx] at h0 rcases mul_eq_zero.mp h0 with h0 | h0 · exact hx (pow_eq_zero_iff (n := 3) (by norm_num) |>.mp h0 ▸ A.zero_mem) · exact A.ne_zero_of_notMem_nonunits (cubic_inv_notMem_nonunits W hx) h0 theorem X_div_Y_mem_nonunits {x y : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∉ A) : x / y ∈ A.nonunits := by have hy0 : y ≠ 0 := Y_ne_zero_of_X_notMem W h hx have hx0 : x ≠ 0 := fun h0 => hx (h0 ▸ A.zero_mem) by_contra hxy have hyx : y / x ∈ A := by have := A.inv_mem_of_notMem_nonunits hxy rwa [inv_div] at this have hxinv : x⁻¹ ∈ A := A.inv_mem_of_notMem hx rw [equation_iff] at h have key : x * (1 + (W.map A.subtype).toAffine.a₂ * x⁻¹ + (W.map A.subtype).toAffine.a₄ * (x⁻¹ * x⁻¹) + (W.map A.subtype).toAffine.a₆ * (x⁻¹ * x⁻¹ * x⁻¹)) = (y / x) * (y / x) + (W.map A.subtype).toAffine.a₁ * (y / x) + (W.map A.subtype).toAffine.a₃ * (y / x) * x⁻¹ := by field_simp linear_combination -h refine hx ?_ have hmem : x * (1 + (W.map A.subtype).toAffine.a₂ * x⁻¹ + (W.map A.subtype).toAffine.a₄ * (x⁻¹ * x⁻¹) + (W.map A.subtype).toAffine.a₆ * (x⁻¹ * x⁻¹ * x⁻¹)) ∈ A := by rw [key] exact add_mem (add_mem (mul_mem hyx hyx) (mul_mem (SetLike.coe_mem W.a₁) hyx)) (mul_mem (mul_mem (SetLike.coe_mem W.a₃) hyx) hxinv) have hcu := cubic_inv_notMem_nonunits W hx have := mul_mem hmem (A.inv_mem_of_notMem_nonunits hcu) rwa [mul_assoc, mul_inv_cancel₀ (A.ne_zero_of_notMem_nonunits hcu), mul_one] at this theorem Y_notMem_of_X_notMem {x y : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∉ A) : y ∉ A := by intro hy refine hx ?_ have hmem : y * (x / y) ∈ A.nonunits := A.mul_mem_nonunits hy (X_div_Y_mem_nonunits W h hx) rw [mul_div_cancel₀ _ (Y_ne_zero_of_X_notMem W h hx)] at hmem exact A.nonunits_subset hmem theorem X_cubed_div_Y_sq_notMem_nonunits {x y : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∉ A) : x ^ 3 / y ^ 2 ∈ A ∧ x ^ 3 / y ^ 2 ∉ A.nonunits := by have hy0 : y ≠ 0 := Y_ne_zero_of_X_notMem W h hx have hx0 : x ≠ 0 := fun h0 => hx (h0 ▸ A.zero_mem) have hxy : x / y ∈ A.nonunits := X_div_Y_mem_nonunits W h hx have hyinv : y⁻¹ ∈ A.nonunits := A.inv_mem_nonunits_of_notMem (Y_notMem_of_X_notMem W h hx) have ha₁ : (W.map A.subtype).toAffine.a₁ ∈ A := SetLike.coe_mem W.a₁ have ha₃ : (W.map A.subtype).toAffine.a₃ ∈ A := SetLike.coe_mem W.a₃ rw [equation_iff] at h have hu : (1 + (W.map A.subtype).toAffine.a₁ * (x / y) + (W.map A.subtype).toAffine.a₃ * y⁻¹) ∉ A.nonunits := by rw [add_assoc] exact A.one_add_notMem_nonunits (add_mem (A.mul_mem_nonunits ha₁ hxy) (A.mul_mem_nonunits ha₃ hyinv)) have hu' : (1 + (W.map A.subtype).toAffine.a₁ * (x / y) + (W.map A.subtype).toAffine.a₃ * y⁻¹) ∈ A := by refine add_mem (add_mem A.one_mem ?_) ?_ · exact mul_mem ha₁ (A.nonunits_subset hxy) · exact mul_mem ha₃ (A.nonunits_subset hyinv) have hc := cubic_inv_notMem_nonunits W hx have hc' : (1 + (W.map A.subtype).toAffine.a₂ * x⁻¹ + (W.map A.subtype).toAffine.a₄ * (x⁻¹ * x⁻¹) + (W.map A.subtype).toAffine.a₆ * (x⁻¹ * x⁻¹ * x⁻¹)) ∈ A := by have hxinv : x⁻¹ ∈ A := A.inv_mem_of_notMem hx refine add_mem (add_mem (add_mem A.one_mem ?_) ?_) ?_ · exact mul_mem (SetLike.coe_mem W.a₂) hxinv · exact mul_mem (SetLike.coe_mem W.a₄) (mul_mem hxinv hxinv) · exact mul_mem (SetLike.coe_mem W.a₆) (mul_mem (mul_mem hxinv hxinv) hxinv) have key' : x ^ 3 / y ^ 2 = (1 + (W.map A.subtype).toAffine.a₁ * (x / y) + (W.map A.subtype).toAffine.a₃ * y⁻¹) * (1 + (W.map A.subtype).toAffine.a₂ * x⁻¹ + (W.map A.subtype).toAffine.a₄ * (x⁻¹ * x⁻¹) + (W.map A.subtype).toAffine.a₆ * (x⁻¹ * x⁻¹ * x⁻¹))⁻¹ := by rw [eq_comm, mul_inv_eq_iff_eq_mul₀ (A.ne_zero_of_notMem_nonunits hc), div_mul_eq_mul_div, eq_div_iff (pow_ne_zero 2 hy0)] field_simp linear_combination h constructor · rw [key'] exact mul_mem hu' (A.inv_mem_of_notMem_nonunits hc) · rw [key'] exact A.mul_notMem_nonunits hu (A.inv_notMem_nonunits_of_notMem_nonunits hc' hc) variable {W} theorem inv_Y_div_mem_nonunits {x y τ : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∉ A) (ht : (x / y) / τ ∈ A) : (1 / y) / τ ∈ A.nonunits := by have hx0 : x ≠ 0 := fun h0 => hx (h0 ▸ A.zero_mem) have hy0 : y ≠ 0 := Y_ne_zero_of_X_notMem W h hx have key : (1 / y) / τ = ((x / y) / τ) * x⁻¹ := by field_simp rw [key] exact A.mul_mem_nonunits ht (A.inv_mem_nonunits_of_notMem hx) theorem inv_X_mul_div_mem_nonunits {x y τ : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∉ A) (hτ0 : τ ≠ 0) (ht : (x / y) / τ ∈ A) : x⁻¹ / τ ∈ A.nonunits := by have hx0 : x ≠ 0 := fun h0 => hx (h0 ▸ A.zero_mem) have hy0 : y ≠ 0 := Y_ne_zero_of_X_notMem W h hx have key : x⁻¹ / τ = (y ^ 2 / x ^ 3) * ((x / y) / τ) * (x / y) := by first | (field_simp; ring1) | field_simp rw [key] refine A.mul_mem_nonunits (mul_mem ?_ ht) (X_div_Y_mem_nonunits W h hx) rw [show y ^ 2 / x ^ 3 = (x ^ 3 / y ^ 2)⁻¹ by rw [inv_div]] exact A.inv_mem_of_notMem_nonunits (X_cubed_div_Y_sq_notMem_nonunits W h hx).2 theorem neg_formal_param_add {x y : L} (hy0 : y ≠ 0) (hy'0 : (W.map A.subtype).toAffine.negY x y ≠ 0) : (-(x / y)) + (-(x / (W.map A.subtype).toAffine.negY x y)) = (W.map A.subtype).toAffine.a₁ * (x / y) * (x / (W.map A.subtype).toAffine.negY x y) + (W.map A.subtype).toAffine.a₃ * (x / y) * (1 / (W.map A.subtype).toAffine.negY x y) := by have hsum : (W.map A.subtype).toAffine.negY x y = -y - (W.map A.subtype).toAffine.a₁ * x - (W.map A.subtype).toAffine.a₃ := rfl generalize hgen : (W.map A.subtype).toAffine.negY x y = y' at * rw [← sub_eq_zero] have key : (-(x / y)) + (-(x / y')) - ((W.map A.subtype).toAffine.a₁ * (x / y) * (x / y') + (W.map A.subtype).toAffine.a₃ * (x / y) * (1 / y')) = (-(x * y') - x * y - (W.map A.subtype).toAffine.a₁ * x * x - (W.map A.subtype).toAffine.a₃ * x) / (y * y') := by first | (field_simp; ring1) | field_simp rw [key, div_eq_zero_iff] left linear_combination (-x) * hsum theorem neg_formal_param_estimate {x y τ : L} (h : (W.map A.subtype).toAffine.Equation x y) (hx : x ∉ A) (hτ0 : τ ≠ 0) (ht : (x / y) / τ ∈ A) : ((-(x / y)) + (-(x / (W.map A.subtype).toAffine.negY x y))) / τ ∈ A.nonunits := by have h' : (W.map A.subtype).toAffine.Equation x ((W.map A.subtype).toAffine.negY x y) := (Affine.equation_neg x y).mpr h have hy0 : y ≠ 0 := Y_ne_zero_of_X_notMem W h hx have hy'0 : (W.map A.subtype).toAffine.negY x y ≠ 0 := Y_ne_zero_of_X_notMem W h' hx rw [neg_formal_param_add hy0 hy'0, add_div] refine add_mem ?_ ?_ · rw [show (W.map A.subtype).toAffine.a₁ * (x / y) * (x / (W.map A.subtype).toAffine.negY x y) / τ = (W.map A.subtype).toAffine.a₁ * ((x / y) / τ) * (x / (W.map A.subtype).toAffine.negY x y) by ring] exact A.mul_mem_nonunits (mul_mem (SetLike.coe_mem W.a₁) ht) (X_div_Y_mem_nonunits W h' hx) · rw [show (W.map A.subtype).toAffine.a₃ * (x / y) * (1 / (W.map A.subtype).toAffine.negY x y) / τ = (W.map A.subtype).toAffine.a₃ * (x / y) * ((1 / (W.map A.subtype).toAffine.negY x y) / τ) by ring] rw [show (W.map A.subtype).toAffine.a₃ * (x / y) * ((1 / (W.map A.subtype).toAffine.negY x y) / τ) = (W.map A.subtype).toAffine.a₃ * ((x / y) / τ) * (1 / (W.map A.subtype).toAffine.negY x y) by ring] rw [one_div] exact A.mul_mem_nonunits (mul_mem (SetLike.coe_mem W.a₃) ht) (A.inv_mem_nonunits_of_notMem (Y_notMem_of_X_notMem W h' hx)) section AdditionEstimate variable [DecidableEq L] theorem sub_eq_slope_mul_sub {x₁ y₁ x₂ y₂ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) : y₁ - y₂ = (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * (x₁ - x₂) := by by_cases hx : x₁ = x₂ · have hy : y₁ = y₂ := Y_eq_of_Y_ne h₁ h₂ hx (fun h => hxy ⟨hx, h⟩) rw [hx, hy, sub_self, sub_self, mul_zero] · rw [slope_of_X_ne hx, div_mul_cancel₀ _ (sub_ne_zero.mpr hx)] theorem vieta_addX {x₁ y₁ x₂ y₂ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) : x₁ * x₂ + x₁ * ((W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) + x₂ * ((W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) = 2 * x₁ * ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ^ 2 + ((W.map A.subtype).toAffine.a₁ * x₁ - 2 * y₁ - (W.map A.subtype).toAffine.a₃) * ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) + (-(W.map A.subtype).toAffine.a₁ * y₁ + (W.map A.subtype).toAffine.a₄) ∧ x₁ * x₂ * ((W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) = x₁ ^ 2 * ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ^ 2 - (2 * x₁ * y₁ + (W.map A.subtype).toAffine.a₃ * x₁) * ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) + (y₁ ^ 2 + (W.map A.subtype).toAffine.a₃ * y₁ - (W.map A.subtype).toAffine.a₆) := by have key := (Affine.addPolynomial_eq (W' := (W.map A.subtype).toAffine) x₁ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)).symm.trans (Affine.addPolynomial_slope h₁ h₂ hxy) rw [Cubic.prod_X_sub_C_eq, neg_inj, Cubic.toPoly_injective] at key have hc := congrArg Cubic.c key have hd := congrArg Cubic.d key simp only at hc hd exact ⟨by linear_combination -hc, by linear_combination hd⟩ theorem secant_slope_identity {x₁ y₁ x₂ y₂ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) : (y₁ - y₂) * (y₁^2*y₂^2 + (W.map A.subtype).toAffine.a₁*x₁*y₁*y₂^2 - (W.map A.subtype).toAffine.a₂*x₁^2*y₂^2 + (W.map A.subtype).toAffine.a₃*(y₁*y₂^2 + y₁^2*y₂) - (W.map A.subtype).toAffine.a₄*x₁*(y₂^2 + y₁*y₂) - (W.map A.subtype).toAffine.a₆*(y₂^2 + y₁*y₂ + y₁^2)) = (x₂*y₁ - x₁*y₂) * (-(W.map A.subtype).toAffine.a₁*y₁^2*y₂ + (W.map A.subtype).toAffine.a₂*x₁*y₁*y₂ + (W.map A.subtype).toAffine.a₂*x₂*y₁^2 + (W.map A.subtype).toAffine.a₄*y₁^2 + x₁^2*y₂^2 + x₁*x₂*y₁*y₂ + x₂^2*y₁^2) := by rw [Affine.equation_iff] at h₁ h₂ set a1 := (W.map A.subtype).toAffine.a₁ set a2 := (W.map A.subtype).toAffine.a₂ set a3 := (W.map A.subtype).toAffine.a₃ set a4 := (W.map A.subtype).toAffine.a₄ set a6 := (W.map A.subtype).toAffine.a₆ linear_combination (-a1^2*x₁*x₂*y₂ + a1*a2*x₁*x₂^2 - a1*a3*x₁*y₂ - a1*a3*x₂*y₂ + a1*a4*x₁*x₂ + a1*a6*x₁ + a1*x₁*x₂^3 - a1*x₁*y₂^2 + a1*x₂*y₁*y₂ + a2*a3*x₂^2 - a2*x₂^2*y₁ - a3^2*y₂ + a3*a4*x₂ + a3*a6 + a3*x₂^3 + a3*y₁*y₂ - a3*y₂^2 - a4*x₂*y₁ - a6*y₁ - x₂^3*y₁ + y₁*y₂^2 - y₂^3) * h₁ + (a1^2*x₁^2*y₁ - a1*a2*x₁^3 + 2*a1*a3*x₁*y₁ - a1*a4*x₁^2 - a1*a6*x₁ - a1*x₁^4 - a2*a3*x₁^2 + a2*x₁^2*y₁ + a3^2*y₁ - a3*a4*x₁ - a3*a6 - a3*x₁^3 + a4*x₁*y₁ + a6*y₁ + x₁^3*y₁) * h₂ theorem tangent_slope_identity {x₁ y₁ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) : -(3*x₁^2 + 2*(W.map A.subtype).toAffine.a₂*x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁*y₁) * ((W.map A.subtype).toAffine.a₁*x₁*y₁ - (W.map A.subtype).toAffine.a₂*x₁^2 + 2*(W.map A.subtype).toAffine.a₃*y₁ - 2*(W.map A.subtype).toAffine.a₄*x₁ - 3*(W.map A.subtype).toAffine.a₆ + y₁^2) = (y₁*(2*y₁ + (W.map A.subtype).toAffine.a₁*x₁ + (W.map A.subtype).toAffine.a₃) - x₁*(3*x₁^2 + 2*(W.map A.subtype).toAffine.a₂*x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁*y₁)) * (3*x₁^2 + 2*(W.map A.subtype).toAffine.a₂*x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁*y₁) := by rw [Affine.equation_iff] at h₁ linear_combination (3*(W.map A.subtype).toAffine.a₁*y₁ - 6*(W.map A.subtype).toAffine.a₂*x₁ - 3*(W.map A.subtype).toAffine.a₄ - 9*x₁^2) * h₁ theorem tangent_intercept_identity {x₁ y₁ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) : y₁*(2*y₁ + (W.map A.subtype).toAffine.a₁*x₁ + (W.map A.subtype).toAffine.a₃) - x₁*(3*x₁^2 + 2*(W.map A.subtype).toAffine.a₂*x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁*y₁) = -(x₁^3 - (W.map A.subtype).toAffine.a₄*x₁ - 2*(W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃*y₁) := by rw [Affine.equation_iff] at h₁ linear_combination 2 * h₁ theorem slope_div_intercept_estimate {x₁ y₁ x₂ y₂ τ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hx₁ : x₁ ∉ A) (hx₂ : x₂ ∉ A) (hxy : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) (hτ : τ ∈ A.nonunits) (hτ0 : τ ≠ 0) (ht₁ : (x₁ / y₁) / τ ∈ A) (ht₂ : (x₂ / y₂) / τ ∈ A) : y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁ ≠ 0 ∧ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁)) / τ ∈ A.nonunits ∧ ((1 : L) / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁)) / τ ∈ A.nonunits := by have ha1A : (W.map A.subtype).toAffine.a₁ ∈ A := SetLike.coe_mem W.a₁ have ha2A : (W.map A.subtype).toAffine.a₂ ∈ A := SetLike.coe_mem W.a₂ have ha3A : (W.map A.subtype).toAffine.a₃ ∈ A := SetLike.coe_mem W.a₃ have ha4A : (W.map A.subtype).toAffine.a₄ ∈ A := SetLike.coe_mem W.a₄ have ha6A : (W.map A.subtype).toAffine.a₆ ∈ A := SetLike.coe_mem W.a₆ have hy₁0 : y₁ ≠ 0 := Y_ne_zero_of_X_notMem W h₁ hx₁ have hy₂0 : y₂ ≠ 0 := Y_ne_zero_of_X_notMem W h₂ hx₂ have hx₁0 : x₁ ≠ 0 := fun h0 => hx₁ (h0 ▸ A.zero_mem) have hT₁ : x₁ / y₁ ∈ A.nonunits := X_div_Y_mem_nonunits W h₁ hx₁ have hT₂ : x₂ / y₂ ∈ A.nonunits := X_div_Y_mem_nonunits W h₂ hx₂ have hT₁A : x₁ / y₁ ∈ A := A.nonunits_subset hT₁ have hT₂A : x₂ / y₂ ∈ A := A.nonunits_subset hT₂ have hs₁ : (1 / y₁) / τ ∈ A.nonunits := inv_Y_div_mem_nonunits h₁ hx₁ ht₁ have hs₂ : (1 / y₂) / τ ∈ A.nonunits := inv_Y_div_mem_nonunits h₂ hx₂ ht₂ have hs₁' : (1 : L) / y₁ ∈ A.nonunits := by rw [one_div] exact A.inv_mem_nonunits_of_notMem (Y_notMem_of_X_notMem W h₁ hx₁) have hs₂' : (1 : L) / y₂ ∈ A.nonunits := by rw [one_div] exact A.inv_mem_nonunits_of_notMem (Y_notMem_of_X_notMem W h₂ hx₂) have hs₁A : (1 : L) / y₁ ∈ A := A.nonunits_subset hs₁' have hs₂A : (1 : L) / y₂ ∈ A := A.nonunits_subset hs₂' have main : y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁ ≠ 0 ∧ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁)) / τ ∈ A.nonunits := by by_cases hx : x₁ = x₂ · have hy : y₁ ≠ (W.map A.subtype).toAffine.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩ have hyy : y₁ = y₂ := Y_eq_of_Y_ne h₁ h₂ hx hy subst hx subst hyy have hψ0 : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ ≠ 0 := sub_ne_zero_of_ne hy have hxinv : x₁⁻¹ ∈ A.nonunits := A.inv_mem_nonunits_of_notMem hx₁ have hxinvA : x₁⁻¹ ∈ A := A.nonunits_subset hxinv have hxτ : x₁⁻¹ / τ ∈ A.nonunits := inv_X_mul_div_mem_nonunits h₁ hx₁ hτ0 ht₁ have hcube := X_cubed_div_Y_sq_notMem_nonunits W h₁ hx₁ have hcubeinvA : (x₁ ^ 3 / y₁ ^ 2)⁻¹ ∈ A := A.inv_mem_of_notMem_nonunits hcube.2 have hI_eq : (x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁) / x₁ ^ 3 = 1 + ((-((W.map A.subtype).toAffine.a₄ * x₁⁻¹) - ((W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₆) * (x₁⁻¹ * x₁⁻¹)) * x₁⁻¹ + ((W.map A.subtype).toAffine.a₃ * (x₁ ^ 3 / y₁ ^ 2)⁻¹) * (1 / y₁)) := by field_simp ring have hIm : ((-((W.map A.subtype).toAffine.a₄ * x₁⁻¹) - ((W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₆) * (x₁⁻¹ * x₁⁻¹)) * x₁⁻¹ + ((W.map A.subtype).toAffine.a₃ * (x₁ ^ 3 / y₁ ^ 2)⁻¹) * (1 / y₁)) ∈ A.nonunits := add_mem (A.mul_mem_nonunits (sub_mem (neg_mem (mul_mem ha4A hxinvA)) (mul_mem (add_mem ha6A ha6A) (mul_mem hxinvA hxinvA))) hxinv) (A.mul_mem_nonunits (mul_mem ha3A hcubeinvA) hs₁') have hInot : (x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁) / x₁ ^ 3 ∉ A.nonunits := by rw [hI_eq] exact A.one_add_notMem_nonunits hIm have hI0 : x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁ ≠ 0 := by intro h0 exact hInot (by rw [h0, zero_div]; exact A.nonunits.zero_mem) have hIinvA : ((x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁) / x₁ ^ 3)⁻¹ ∈ A := A.inv_mem_of_notMem_nonunits hInot have hψ_eq : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ = y₁ + y₁ + (W.map A.subtype).toAffine.a₁ * x₁ + (W.map A.subtype).toAffine.a₃ := by simp only [negY] ring have h₁' := h₁ rw [Affine.equation_iff] at h₁' have hkey : (y₁ - (W.map A.subtype).toAffine.slope x₁ x₁ y₁ y₁ * x₁) * (y₁ - (W.map A.subtype).toAffine.negY x₁ y₁) = -(x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁) := by rw [Affine.slope_of_Y_ne rfl hy, sub_mul, div_mul_eq_mul_div, div_mul_cancel₀ _ hψ0, hψ_eq] linear_combination (2 : L) * h₁' have hν0 : y₁ - (W.map A.subtype).toAffine.slope x₁ x₁ y₁ y₁ * x₁ ≠ 0 := by intro h0 rw [h0, zero_mul] at hkey exact hI0 (by linear_combination hkey) refine ⟨hν0, ?_⟩ have hslope_mul : (W.map A.subtype).toAffine.slope x₁ x₁ y₁ y₁ * (y₁ - (W.map A.subtype).toAffine.negY x₁ y₁) = 3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ := by rw [Affine.slope_of_Y_ne rfl hy, div_mul_cancel₀ _ hψ0] have hℓν : (W.map A.subtype).toAffine.slope x₁ x₁ y₁ y₁ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₁ y₁ y₁ * x₁) = -(3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) / (x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁) := by rw [div_eq_div_iff hν0 hI0] linear_combination (-(y₁ - (W.map A.subtype).toAffine.slope x₁ x₁ y₁ y₁ * x₁)) * hslope_mul + (W.map A.subtype).toAffine.slope x₁ x₁ y₁ y₁ * hkey rw [hℓν] have hsplit : (-(3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ + (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) / (x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁)) / τ = ((x₁ ^ 3 - (W.map A.subtype).toAffine.a₄ * x₁ - 2 * (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₃ * y₁) / x₁ ^ 3)⁻¹ * (-(((1 + 1 + 1) + ((W.map A.subtype).toAffine.a₂ + (W.map A.subtype).toAffine.a₂) * x₁⁻¹ + (W.map A.subtype).toAffine.a₄ * (x₁⁻¹ * x₁⁻¹)) * (x₁⁻¹ / τ) - ((W.map A.subtype).toAffine.a₁ * (x₁ ^ 3 / y₁ ^ 2)⁻¹) * ((1 / y₁) / τ))) := by field_simp ring rw [hsplit] refine A.mul_mem_nonunits hIinvA (A.nonunits.neg_mem (sub_mem ?_ ?_)) · exact A.mul_mem_nonunits (add_mem (add_mem (add_mem (add_mem A.one_mem A.one_mem) A.one_mem) (mul_mem (add_mem ha2A ha2A) hxinvA)) (mul_mem ha4A (mul_mem hxinvA hxinvA))) hxτ · exact A.mul_mem_nonunits (mul_mem ha1A hcubeinvA) hs₁ · have hxx0 : x₁ - x₂ ≠ 0 := sub_ne_zero_of_ne hx have hsec := secant_slope_identity (W := W) h₁ h₂ have hU_eq : (y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2)) / (y₁ ^ 2 * y₂ ^ 2) = 1 + (((W.map A.subtype).toAffine.a₁ - (W.map A.subtype).toAffine.a₂ * (x₁ / y₁) - (W.map A.subtype).toAffine.a₄ * (1 / y₁) - (W.map A.subtype).toAffine.a₄ * (1 / y₂)) * (x₁ / y₁) + ((W.map A.subtype).toAffine.a₃ - (W.map A.subtype).toAffine.a₆ * (1 / y₁) - (W.map A.subtype).toAffine.a₆ * (1 / y₂)) * (1 / y₁) + ((W.map A.subtype).toAffine.a₃ - (W.map A.subtype).toAffine.a₆ * (1 / y₂)) * (1 / y₂)) := by field_simp ring have hUm : (((W.map A.subtype).toAffine.a₁ - (W.map A.subtype).toAffine.a₂ * (x₁ / y₁) - (W.map A.subtype).toAffine.a₄ * (1 / y₁) - (W.map A.subtype).toAffine.a₄ * (1 / y₂)) * (x₁ / y₁) + ((W.map A.subtype).toAffine.a₃ - (W.map A.subtype).toAffine.a₆ * (1 / y₁) - (W.map A.subtype).toAffine.a₆ * (1 / y₂)) * (1 / y₁) + ((W.map A.subtype).toAffine.a₃ - (W.map A.subtype).toAffine.a₆ * (1 / y₂)) * (1 / y₂)) ∈ A.nonunits := by refine add_mem (add_mem (A.mul_mem_nonunits ?_ hT₁) (A.mul_mem_nonunits ?_ hs₁')) (A.mul_mem_nonunits ?_ hs₂') · exact sub_mem (sub_mem (sub_mem ha1A (mul_mem ha2A hT₁A)) (mul_mem ha4A hs₁A)) (mul_mem ha4A hs₂A) · exact sub_mem (sub_mem ha3A (mul_mem ha6A hs₁A)) (mul_mem ha6A hs₂A) · exact sub_mem ha3A (mul_mem ha6A hs₂A) have hUnot : (y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2)) / (y₁ ^ 2 * y₂ ^ 2) ∉ A.nonunits := by rw [hU_eq] exact A.one_add_notMem_nonunits hUm have hUA : (y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2)) / (y₁ ^ 2 * y₂ ^ 2) ∈ A := by rw [hU_eq] exact add_mem A.one_mem (A.nonunits_subset hUm) have hUinvA : ((y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2)) / (y₁ ^ 2 * y₂ ^ 2))⁻¹ ∈ A := A.inv_mem_of_notMem_nonunits hUnot have hU0 : y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2) ≠ 0 := by intro h0 exact hUnot (by rw [h0, zero_div]; exact A.nonunits.zero_mem) have hxy21 : x₁ * y₂ - x₂ * y₁ ≠ 0 := by intro h0 have hUV : (y₁ - y₂) * (y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2)) = 0 := by rw [hsec] linear_combination (-(-((W.map A.subtype).toAffine.a₁ * y₁ ^ 2 * y₂) + (W.map A.subtype).toAffine.a₂ * x₁ * y₁ * y₂ + (W.map A.subtype).toAffine.a₂ * x₂ * y₁ ^ 2 + (W.map A.subtype).toAffine.a₄ * y₁ ^ 2 + x₁ ^ 2 * y₂ ^ 2 + x₁ * x₂ * y₁ * y₂ + x₂ ^ 2 * y₁ ^ 2)) * h0 rcases mul_eq_zero.mp hUV with h | h · refine hx ?_ have hy12 : y₁ = y₂ := by linear_combination h have hxx : (x₁ - x₂) * y₁ = 0 := by linear_combination h0 + x₁ * hy12 rcases mul_eq_zero.mp hxx with h' | h' · exact sub_eq_zero.mp h' · exact absurd h' hy₁0 · exact hU0 h have hkey : (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁) * (x₁ - x₂) = x₁ * y₂ - x₂ * y₁ := by rw [Affine.slope_of_X_ne hx] field_simp ring have hν0 : y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁ ≠ 0 := by intro h0 exact hxy21 (by rw [← hkey, h0, zero_mul]) refine ⟨hν0, ?_⟩ have hℓν : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁) = (y₁ - y₂) / (x₁ * y₂ - x₂ * y₁) := by rw [div_eq_div_iff hν0 hxy21, Affine.slope_of_X_ne hx] field_simp ring have hVU : (y₁ - y₂) / (x₁ * y₂ - x₂ * y₁) = -((-((W.map A.subtype).toAffine.a₁ * y₁ ^ 2 * y₂) + (W.map A.subtype).toAffine.a₂ * x₁ * y₁ * y₂ + (W.map A.subtype).toAffine.a₂ * x₂ * y₁ ^ 2 + (W.map A.subtype).toAffine.a₄ * y₁ ^ 2 + x₁ ^ 2 * y₂ ^ 2 + x₁ * x₂ * y₁ * y₂ + x₂ ^ 2 * y₁ ^ 2) / (y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2))) := by rw [← neg_div, div_eq_div_iff hxy21 hU0] linear_combination hsec have hVsplit : ((y₁ - y₂) / (x₁ * y₂ - x₂ * y₁)) / τ = ((y₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₁ * x₁ * y₁ * y₂ ^ 2 - (W.map A.subtype).toAffine.a₂ * x₁ ^ 2 * y₂ ^ 2 + (W.map A.subtype).toAffine.a₃ * (y₁ * y₂ ^ 2 + y₁ ^ 2 * y₂) - (W.map A.subtype).toAffine.a₄ * x₁ * (y₂ ^ 2 + y₁ * y₂) - (W.map A.subtype).toAffine.a₆ * (y₂ ^ 2 + y₁ * y₂ + y₁ ^ 2)) / (y₁ ^ 2 * y₂ ^ 2))⁻¹ * (-((-(W.map A.subtype).toAffine.a₁ + (W.map A.subtype).toAffine.a₂ * (x₁ / y₁) + (W.map A.subtype).toAffine.a₂ * (x₂ / y₂) + (W.map A.subtype).toAffine.a₄ * (1 / y₂)) * ((1 / y₂) / τ) + ((x₁ / y₁) / τ) * (x₁ / y₁) + ((x₂ / y₂) / τ) * (x₁ / y₁ + x₂ / y₂))) := by rw [hVU] first | (field_simp; ring1) | field_simp rw [hℓν, hVsplit] refine A.mul_mem_nonunits hUinvA (A.nonunits.neg_mem (add_mem (add_mem (A.mul_mem_nonunits ?_ hs₂) (A.mul_mem_nonunits ht₁ hT₁)) (A.mul_mem_nonunits ht₂ (add_mem hT₁ hT₂)))) exact add_mem (add_mem (add_mem (neg_mem ha1A) (mul_mem ha2A hT₁A)) (mul_mem ha2A hT₂A)) (mul_mem ha4A hs₂A) obtain ⟨hν0, hℓν⟩ := main refine ⟨hν0, hℓν, ?_⟩ have hℓν' : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁) ∈ A.nonunits := by rw [show (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁) = ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁)) / τ * τ from (div_mul_cancel₀ _ hτ0).symm] exact A.mul_mem_nonunits (A.nonunits_subset hℓν) hτ have hy₁0 : y₁ ≠ 0 := Y_ne_zero_of_X_notMem W h₁ hx₁ have hline : ((1 : L) / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁)) / τ = (1 / y₁) / τ + ((x₁ / y₁) / τ) * ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ / (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁)) := by first | (field_simp; ring1) | field_simp rw [hline] exact add_mem (inv_Y_div_mem_nonunits h₁ hx₁ ht₁) (A.mul_mem_nonunits ht₁ hℓν') theorem collinear_prod_sum {x₁ y₁ x₂ y₂ x₃ y₃ ℓ ν : L} (he₁ : x₁ + x₂ + x₃ = ℓ ^ 2 + (W.map A.subtype).toAffine.a₁ * ℓ - (W.map A.subtype).toAffine.a₂) (he₂ : x₁ * x₂ + x₁ * x₃ + x₂ * x₃ = 2 * x₁ * ℓ ^ 2 + ((W.map A.subtype).toAffine.a₁ * x₁ - 2 * y₁ - (W.map A.subtype).toAffine.a₃) * ℓ + (-(W.map A.subtype).toAffine.a₁ * y₁ + (W.map A.subtype).toAffine.a₄)) (he₃ : x₁ * x₂ * x₃ = x₁ ^ 2 * ℓ ^ 2 - (2 * x₁ * y₁ + (W.map A.subtype).toAffine.a₃ * x₁) * ℓ + (y₁ ^ 2 + (W.map A.subtype).toAffine.a₃ * y₁ - (W.map A.subtype).toAffine.a₆)) (hν : ν = y₁ - ℓ * x₁) (hy₂ : y₂ = ℓ * x₂ + ν) (hy₃ : y₃ = ℓ * x₃ + ν) : y₁ * y₂ * y₃ = ν ^ 3 - (W.map A.subtype).toAffine.a₂ * ℓ * ν ^ 2 + (W.map A.subtype).toAffine.a₄ * ℓ ^ 2 * ν - (W.map A.subtype).toAffine.a₆ * ℓ ^ 3 ∧ x₁ * y₂ * y₃ + x₂ * y₁ * y₃ + x₃ * y₁ * y₂ = -((W.map A.subtype).toAffine.a₁ * ℓ * ν ^ 2) - (W.map A.subtype).toAffine.a₂ * ν ^ 2 + (W.map A.subtype).toAffine.a₃ * ℓ ^ 2 * ν + ((W.map A.subtype).toAffine.a₄ + (W.map A.subtype).toAffine.a₄) * ℓ * ν - ((W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₆) * ℓ ^ 2 := by subst hy₂ hy₃ hν constructor · linear_combination (ℓ * (y₁ - ℓ * x₁) ^ 2) * he₁ + (ℓ ^ 2 * (y₁ - ℓ * x₁)) * he₂ + ℓ ^ 3 * he₃ · linear_combination ((y₁ - ℓ * x₁) ^ 2) * he₁ + (2 * ℓ * (y₁ - ℓ * x₁)) * he₂ + (3 * ℓ ^ 2) * he₃ theorem add_formal_param_estimate {x₁ y₁ x₂ y₂ τ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁) (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hx₁ : x₁ ∉ A) (hx₂ : x₂ ∉ A) (hxy : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂)) (hτ : τ ∈ A.nonunits) (hτ0 : τ ≠ 0) (ht₁ : (x₁ / y₁) / τ ∈ A) (ht₂ : (x₂ / y₂) / τ ∈ A) : (W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∉ A ∧ ((-((W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) / (W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂))) - (-(x₁ / y₁)) - (-(x₂ / y₂))) / τ ∈ A.nonunits := by have ha1A : (W.map A.subtype).toAffine.a₁ ∈ A := SetLike.coe_mem W.a₁ have ha2A : (W.map A.subtype).toAffine.a₂ ∈ A := SetLike.coe_mem W.a₂ have ha3A : (W.map A.subtype).toAffine.a₃ ∈ A := SetLike.coe_mem W.a₃ have ha4A : (W.map A.subtype).toAffine.a₄ ∈ A := SetLike.coe_mem W.a₄ have ha6A : (W.map A.subtype).toAffine.a₆ ∈ A := SetLike.coe_mem W.a₆ have hy₁0 : y₁ ≠ 0 := Y_ne_zero_of_X_notMem W h₁ hx₁ have hy₂0 : y₂ ≠ 0 := Y_ne_zero_of_X_notMem W h₂ hx₂ obtain ⟨hν0, hℓντ, hsντ⟩ := slope_div_intercept_estimate h₁ h₂ hx₁ hx₂ hxy hτ hτ0 ht₁ ht₂ obtain ⟨hv₂, hv₃⟩ := vieta_addX (W := W) h₁ h₂ hxy have hS := sub_eq_slope_mul_sub (W := W) h₁ h₂ hxy have hR : (W.map A.subtype).toAffine.Equation ((W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) ((W.map A.subtype).toAffine.negAddY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) := equation_negAdd h₁ h₂ hxy have he₁ : x₁ + x₂ + (W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) = ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ^ 2 + (W.map A.subtype).toAffine.a₁ * ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) - (W.map A.subtype).toAffine.a₂ := by simp only [Affine.addX] ring have hy₃_line : (W.map A.subtype).toAffine.negAddY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) = ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) * ((W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) + (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁) := by simp only [Affine.negAddY] ring have hy₂_line : y₂ = ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) * x₂ + (y₁ - (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ * x₁) := by linear_combination -hS obtain ⟨hD, hN⟩ := collinear_prod_sum he₁ hv₂ hv₃ rfl hy₂_line hy₃_line rw [show (W.map A.subtype).toAffine.addY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) = (W.map A.subtype).toAffine.negY ((W.map A.subtype).toAffine.addX x₁ x₂ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) ((W.map A.subtype).toAffine.negAddY x₁ x₂ y₁ ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂)) from rfl] set ℓ := (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ with hℓ_def set x₃ := (W.map A.subtype).toAffine.addX x₁ x₂ ℓ with hx₃_def set y₃ := (W.map A.subtype).toAffine.negAddY x₁ x₂ y₁ ℓ with hy₃_def set ν := y₁ - ℓ * x₁ with hν_def have hℓν_m : ℓ / ν ∈ A.nonunits := by rw [show ℓ / ν = ℓ / ν / τ * τ from (div_mul_cancel₀ _ hτ0).symm] exact A.mul_mem_nonunits (A.nonunits_subset hℓντ) hτ have hℓν_A : ℓ / ν ∈ A := A.nonunits_subset hℓν_m have hsν_m : (1 : L) / ν ∈ A.nonunits := by rw [show (1 : L) / ν = (1 : L) / ν / τ * τ from (div_mul_cancel₀ _ hτ0).symm] exact A.mul_mem_nonunits (A.nonunits_subset hsντ) hτ have hu_eq : (ν ^ 3 - (W.map A.subtype).toAffine.a₂ * ℓ * ν ^ 2 + (W.map A.subtype).toAffine.a₄ * ℓ ^ 2 * ν - (W.map A.subtype).toAffine.a₆ * ℓ ^ 3) / ν ^ 3 = 1 + (-((W.map A.subtype).toAffine.a₂ * (ℓ / ν)) + ((W.map A.subtype).toAffine.a₄ * (ℓ / ν)) * (ℓ / ν) - (((W.map A.subtype).toAffine.a₆ * (ℓ / ν)) * (ℓ / ν)) * (ℓ / ν)) := by field_simp ring have hum : (-((W.map A.subtype).toAffine.a₂ * (ℓ / ν)) + ((W.map A.subtype).toAffine.a₄ * (ℓ / ν)) * (ℓ / ν) - (((W.map A.subtype).toAffine.a₆ * (ℓ / ν)) * (ℓ / ν)) * (ℓ / ν)) ∈ A.nonunits := sub_mem (add_mem (A.nonunits.neg_mem (A.mul_mem_nonunits ha2A hℓν_m)) (A.mul_mem_nonunits (mul_mem ha4A hℓν_A) hℓν_m)) (A.mul_mem_nonunits (mul_mem (mul_mem ha6A hℓν_A) hℓν_A) hℓν_m) have hu_not : (ν ^ 3 - (W.map A.subtype).toAffine.a₂ * ℓ * ν ^ 2 + (W.map A.subtype).toAffine.a₄ * ℓ ^ 2 * ν - (W.map A.subtype).toAffine.a₆ * ℓ ^ 3) / ν ^ 3 ∉ A.nonunits := by rw [hu_eq] exact A.one_add_notMem_nonunits hum have hu_invA : ((ν ^ 3 - (W.map A.subtype).toAffine.a₂ * ℓ * ν ^ 2 + (W.map A.subtype).toAffine.a₄ * ℓ ^ 2 * ν - (W.map A.subtype).toAffine.a₆ * ℓ ^ 3) / ν ^ 3)⁻¹ ∈ A := A.inv_mem_of_notMem_nonunits hu_not have hD0 : ν ^ 3 - (W.map A.subtype).toAffine.a₂ * ℓ * ν ^ 2 + (W.map A.subtype).toAffine.a₄ * ℓ ^ 2 * ν - (W.map A.subtype).toAffine.a₆ * ℓ ^ 3 ≠ 0 := by intro h0 exact hu_not (by rw [h0, zero_div]; exact A.nonunits.zero_mem) have hy₃0 : y₃ ≠ 0 := by intro h0 rw [h0, mul_zero] at hD exact hD0 hD.symm have hsum_frac : -(x₃ / y₃) + -(x₁ / y₁) + -(x₂ / y₂) = -((x₁ * y₂ * y₃ + x₂ * y₁ * y₃ + x₃ * y₁ * y₂) / (y₁ * y₂ * y₃)) := by field_simp ring have hsum_split : (-(x₃ / y₃) + -(x₁ / y₁) + -(x₂ / y₂)) / τ = ((ν ^ 3 - (W.map A.subtype).toAffine.a₂ * ℓ * ν ^ 2 + (W.map A.subtype).toAffine.a₄ * ℓ ^ 2 * ν - (W.map A.subtype).toAffine.a₆ * ℓ ^ 3) / ν ^ 3)⁻¹ * (((W.map A.subtype).toAffine.a₁ - (W.map A.subtype).toAffine.a₃ * (ℓ / ν)) * (ℓ / ν / τ) + ((W.map A.subtype).toAffine.a₂ - ((W.map A.subtype).toAffine.a₄ + (W.map A.subtype).toAffine.a₄) * (ℓ / ν) + (((W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₆ + (W.map A.subtype).toAffine.a₆) * (ℓ / ν)) * (ℓ / ν)) * ((1 : L) / ν / τ)) := by rw [hsum_frac, hN, hD] field_simp ring have hsum_mem : (-(x₃ / y₃) + -(x₁ / y₁) + -(x₂ / y₂)) / τ ∈ A.nonunits := by rw [hsum_split] refine A.mul_mem_nonunits hu_invA (add_mem (A.mul_mem_nonunits ?_ hℓντ) (A.mul_mem_nonunits ?_ hsντ)) · exact sub_mem ha1A (mul_mem ha3A hℓν_A) · exact add_mem (sub_mem ha2A (mul_mem (add_mem ha4A ha4A) hℓν_A)) (mul_mem (mul_mem (add_mem (add_mem ha6A ha6A) ha6A) hℓν_A) hℓν_A) have hT₃τ : (x₃ / y₃) / τ ∈ A := by have key : (x₃ / y₃) / τ = -((-(x₃ / y₃) + -(x₁ / y₁) + -(x₂ / y₂)) / τ) + (-((x₁ / y₁) / τ)) + (-((x₂ / y₂) / τ)) := by ring rw [key] exact add_mem (add_mem (neg_mem (A.nonunits_subset hsum_mem)) (neg_mem ht₁)) (neg_mem ht₂) have hT₃ : x₃ / y₃ ∈ A.nonunits := by rw [show x₃ / y₃ = x₃ / y₃ / τ * τ from (div_mul_cancel₀ _ hτ0).symm] exact A.mul_mem_nonunits hT₃τ hτ have hy₃inv : y₃⁻¹ ∈ A.nonunits := by have hν_alt : ν = y₃ - ℓ * x₃ := by linear_combination -hy₃_line have expand : (1 : L) / ν - ℓ / ν * (x₃ / y₃) = (y₃ - ℓ * x₃) / (ν * y₃) := by first | (field_simp; ring1) | field_simp have key : y₃⁻¹ = (1 : L) / ν - ℓ / ν * (x₃ / y₃) := by rw [expand, ← hν_alt, eq_div_iff (mul_ne_zero hν0 hy₃0), mul_comm ν y₃, ← mul_assoc, inv_mul_cancel₀ hy₃0, one_mul] rw [key] exact sub_mem hsν_m (A.mul_mem_nonunits hℓν_A hT₃) have hy₃notA : y₃ ∉ A := (A.inv_mem_nonunits_iff.mp hy₃inv).resolve_left hy₃0 have hx₃notA : x₃ ∉ A := fun hmem => hy₃notA (Y_mem_of_X_mem W hR hmem) refine ⟨hx₃notA, ?_⟩ have hneg := neg_formal_param_estimate (W := W) hR hx₃notA hτ0 hT₃τ have key : (-(x₃ / (W.map A.subtype).toAffine.negY x₃ y₃) - -(x₁ / y₁) - -(x₂ / y₂)) / τ = (-(x₃ / y₃) + -(x₃ / (W.map A.subtype).toAffine.negY x₃ y₃)) / τ - (-(x₃ / y₃) + -(x₁ / y₁) + -(x₂ / y₂)) / τ := by ring rw [key] exact sub_mem hneg hsum_mem end AdditionEstimate section Assembly variable [DecidableEq L] open Affine.Point in theorem formal_param_nsmul {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hx : x ∉ A) (j : ℕ) : (j • (some x y h : (W.map A.subtype).toAffine.Point) = 0 → (j : L) ∈ A.nonunits) ∧ (∀ x' y' (h' : (W.map A.subtype).toAffine.Nonsingular x' y'), j • (some x y h : (W.map A.subtype).toAffine.Point) = some x' y' h' → x' ∉ A ∧ (-(x' / y')) / (-(x / y)) - (j : L) ∈ A.nonunits) := by have hy0 : y ≠ 0 := Affine.Y_ne_zero_of_X_notMem W h.1 hx have hx0 : x ≠ 0 := fun h0 => hx (h0 ▸ A.zero_mem) have hτ : -(x / y) ∈ A.nonunits := A.nonunits.neg_mem (Affine.X_div_Y_mem_nonunits W h.1 hx) have hτ0 : -(x / y) ≠ 0 := neg_ne_zero.mpr (div_ne_zero hx0 hy0) have hself : (x / y) / -(x / y) ∈ A := by rw [div_neg, div_self (div_ne_zero hx0 hy0)] exact A.toSubring.neg_mem A.one_mem induction j with | zero => refine ⟨fun _ => by simpa using A.nonunits.zero_mem, fun x' y' h' heq => ?_⟩ rw [zero_smul] at heq exact absurd heq.symm (some_ne_zero h') | succ j ih => rw [succ_nsmul] rcases hP : (j • (some x y h : (W.map A.subtype).toAffine.Point)) with _ | @⟨xj, yj, hj⟩ · have hj0 : (j : L) ∈ A.nonunits := (ih.1) hP rw [← Affine.Point.zero_def, zero_add] refine ⟨fun h0 => absurd h0 (some_ne_zero h), fun x' y' h' heq => ?_⟩ obtain ⟨rfl, rfl⟩ : x = x' ∧ y = y' := by rwa [Affine.Point.some.injEq] at heq refine ⟨hx, ?_⟩ rw [div_self hτ0, Nat.cast_succ] have : (1 : L) - (j + 1) = -j := by ring rw [this] exact A.nonunits.neg_mem hj0 · have hIH := (ih.2) xj yj hj hP obtain ⟨hxj, hcong⟩ := hIH have htj : (xj / yj) / -(x / y) ∈ A := by have h1 : -(xj / yj) / -(x / y) ∈ A := by have := add_mem (A.nonunits_subset hcong) (show ((j : L)) ∈ A from by simpa using SetLike.coe_mem ((j : ℕ) : A)) simpa using this simpa [neg_div] using A.toSubring.neg_mem h1 by_cases hcond : xj = x ∧ yj = (W.map A.subtype).toAffine.negY x y · rw [add_of_Y_eq hcond.1 hcond.2] refine ⟨fun _ => ?_, fun x' y' h' heq => absurd heq.symm (some_ne_zero h')⟩ have hneg := Affine.neg_formal_param_estimate (W := W) h.1 hx hτ0 hself rw [hcond.1, hcond.2] at hcong have key : ((j : L) + 1) = ((-(x / y)) + (-(x / (W.map A.subtype).toAffine.negY x y))) / -(x / y) - (-(x / (W.map A.subtype).toAffine.negY x y)) / -(x / y) + (j : L) + (1 - (-(x / y)) / -(x / y)) := by first | (field_simp; ring1) | field_simp rw [Nat.cast_succ, key] have h1 : (1 : L) - (-(x / y)) / -(x / y) = 0 := by rw [div_self hτ0]; ring rw [h1, add_zero] have h2 : -(x / (W.map A.subtype).toAffine.negY x y) / -(x / y) - (j : L) ∈ A.nonunits := hcong have h3 := A.nonunits.sub_mem hneg h2 have heq : ((-(x / y)) + (-(x / (W.map A.subtype).toAffine.negY x y))) / -(x / y) - (-(x / (W.map A.subtype).toAffine.negY x y)) / -(x / y) + (j : L) = ((-(x / y)) + (-(x / (W.map A.subtype).toAffine.negY x y))) / -(x / y) - ((-(x / (W.map A.subtype).toAffine.negY x y)) / -(x / y) - (j : L)) := by ring rw [heq] exact h3 · rw [add_some hcond] refine ⟨fun h0 => absurd h0 (some_ne_zero _), fun x' y' h' heq => ?_⟩ obtain ⟨hx', hy'⟩ : (W.map A.subtype).toAffine.addX xj x ((W.map A.subtype).toAffine.slope xj x yj y) = x' ∧ (W.map A.subtype).toAffine.addY xj x yj ((W.map A.subtype).toAffine.slope xj x yj y) = y' := by rwa [Affine.Point.some.injEq] at heq subst hx' subst hy' obtain ⟨hadd1, hadd2⟩ := add_formal_param_estimate (W := W) hj.1 h.1 hxj hx hcond hτ hτ0 htj hself refine ⟨hadd1, ?_⟩ have key : (-((W.map A.subtype).toAffine.addX xj x ((W.map A.subtype).toAffine.slope xj x yj y) / (W.map A.subtype).toAffine.addY xj x yj ((W.map A.subtype).toAffine.slope xj x yj y))) / -(x / y) - ((j : ℕ) + 1 : L) = ((-((W.map A.subtype).toAffine.addX xj x ((W.map A.subtype).toAffine.slope xj x yj y) / (W.map A.subtype).toAffine.addY xj x yj ((W.map A.subtype).toAffine.slope xj x yj y))) - (-(xj / yj)) - (-(x / y))) / -(x / y) + ((-(xj / yj)) / -(x / y) - (j : L)) + ((-(x / y)) / -(x / y) - 1) := by first | (field_simp; ring1) | field_simp rw [Nat.cast_succ, key] refine add_mem (add_mem hadd2 ?_) ?_ · exact hcong · rw [div_self hτ0, sub_self] exact A.nonunits.zero_mem end Assembly end Affine open Affine Affine.Point in theorem X_mem_of_nsmul_eq_zero' [DecidableEq L] {n : ℕ} (hn : (n : ResidueField A) ≠ 0) {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hP : n • (some x y h : (W.map A.subtype).toAffine.Point) = 0) : x ∈ A := by by_contra hx refine hn ?_ rw [← A.natCast_mem_nonunits_iff_residue_eq_zero] exact (formal_param_nsmul (W := W) h hx n).1 hP theorem X_mem_of_nsmul_eq_zero'' [DecidableEq L] (hΔ : (W.map (residue A)).Δ ≠ 0) {n : ℕ} (hn : (n : ResidueField A) ≠ 0) {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (hP : n • (Affine.Point.some x y h : (W.map A.subtype).toAffine.Point) = 0) : x ∈ A := X_mem_of_nsmul_eq_zero' W hn h hP open Affine.Point in theorem some_eq_of_mem_inertia_of_nsmul_eq_zero' [DecidableEq L] (hΔ : (W.map (residue A)).Δ ≠ 0) {K : Type*} [Field K] [Algebra K L] {σ : L ≃ₐ[K] L} (hσ : σ ∈ A.decompositionSubgroup K) (hσI : (⟨σ, hσ⟩ : A.decompositionSubgroup K) ∈ A.inertiaSubgroup K) {n : ℕ} (hn : (n : ResidueField A) ≠ 0) {x y : L} (h : (W.map A.subtype).toAffine.Nonsingular x y) (h' : (W.map A.subtype).toAffine.Nonsingular (σ x) (σ y)) (hP : n • (some x y h : (W.map A.subtype).toAffine.Point) = 0) (hP' : n • (some (σ x) (σ y) h' : (W.map A.subtype).toAffine.Point) = 0) : (some (σ x) (σ y) h' : (W.map A.subtype).toAffine.Point) = some x y h := by have hx : x ∈ A := X_mem_of_nsmul_eq_zero' W hn h hP have hy : y ∈ A := Affine.Y_mem_of_X_mem W h.1 hx have hσx : σ x ∈ A := A.smul_mem_of_mem_decompositionSubgroup K hσ hx have hσy : σ y ∈ A := A.smul_mem_of_mem_decompositionSubgroup K hσ hy have hresx : σ x - x ∈ A.nonunits := by rw [show σ x - x = (((⟨σ x, hσx⟩ : A) - ⟨x, hx⟩ : A) : L) from rfl, A.coe_mem_nonunits_iff_residue_eq_zero, map_sub, sub_eq_zero] exact A.residue_smul_eq_of_mem_inertiaSubgroup hσ hσI ⟨x, hx⟩ have hresy : σ y - y ∈ A.nonunits := by rw [show σ y - y = (((⟨σ y, hσy⟩ : A) - ⟨y, hy⟩ : A) : L) from rfl, A.coe_mem_nonunits_iff_residue_eq_zero, map_sub, sub_eq_zero] exact A.residue_smul_eq_of_mem_inertiaSubgroup hσ hσI ⟨y, hy⟩ by_contra hne have hnegns : (W.map A.subtype).toAffine.Nonsingular x ((W.map A.subtype).toAffine.negY x y) := (Affine.nonsingular_neg ..).mpr h have hPQ : ¬(σ x = x ∧ σ y = (W.map A.subtype).toAffine.negY x ((W.map A.subtype).toAffine.negY x y)) := by rw [Affine.negY_negY] exact fun ⟨hx', hy'⟩ => hne (by simp only [Affine.Point.some.injEq]; exact ⟨hx', hy'⟩) have hQdef : (some (σ x) (σ y) h' : (W.map A.subtype).toAffine.Point) - some x y h = some _ _ (Affine.nonsingular_add h' hnegns hPQ) := by rw [sub_eq_add_neg, neg_some, add_some hPQ] have hQtor : n • ((some (σ x) (σ y) h' : (W.map A.subtype).toAffine.Point) - some x y h) = 0 := by rw [smul_sub, hP, hP', sub_zero] have hQX : (W.map A.subtype).toAffine.addX (σ x) x ((W.map A.subtype).toAffine.slope (σ x) x (σ y) ((W.map A.subtype).toAffine.negY x y)) ∈ A := by refine X_mem_of_nsmul_eq_zero' W hn (Affine.nonsingular_add h' hnegns hPQ) ?_ rw [← hQdef] exact hQtor refine Affine.addX_notMem_of_sub_mem_nonunits W hΔ h'.1 hnegns.1 hσx hx hPQ hresx ?_ hQX rw [Affine.negY_negY] exact hresy open Affine.Point in theorem fixed_of_mem_inertia_of_nsmul_eq_zero [DecidableEq L] {V : WeierstrassCurve L} (W : WeierstrassCurve A) (hVW : W.map A.subtype = V) (hΔ : (W.map (residue A)).Δ ≠ 0) {K : Type*} [Field K] [Algebra K L] {σ : L ≃ₐ[K] L} (hσ : σ ∈ A.decompositionSubgroup K) (hσI : (⟨σ, hσ⟩ : A.decompositionSubgroup K) ∈ A.inertiaSubgroup K) {n : ℕ} (hn : (n : ResidueField A) ≠ 0) {x y : L} (h : V.toAffine.Nonsingular x y) (h' : V.toAffine.Nonsingular (σ x) (σ y)) (hP : n • (some x y h : V.toAffine.Point) = 0) (hP' : n • (some (σ x) (σ y) h' : V.toAffine.Point) = 0) : σ x = x ∧ σ y = y := by subst hVW have key := some_eq_of_mem_inertia_of_nsmul_eq_zero' W hΔ hσ hσI hn h h' hP hP' rwa [Affine.Point.some.injEq] at key end WeierstrassCurve