Definitions/Def_WeierstrassCurve_TorsionIntegral.lean

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