import Mathlib
import Definitions.Def_TateCurve_XMultDistinctRouteB
import Definitions.Def_TateCurve_TateFiltrationPrep
import Definitions.Def_TateCurve_KeystoneVocab
import Theorems.Thm_TateCurve_symAddHyps_unconditional
import Theorems.Thm_TateCurve_diffHyp_unconditional
import Theorems.Thm_TateCurve_eq_zero_or_eq_tateParam_unconditional

set_option linter.unusedSectionVars false
set_option autoImplicit false

universe u

namespace WeierstrassCurve
variable {F : Type u} [Field F] [DecidableEq F] (W : WeierstrassCurve F)

abbrev n_torsionGen (n : ℕ) : Type u := Submodule.torsionBy ℤ W.toAffine.Point n
end WeierstrassCurve

namespace WeierstrassCurve.Affine
variable {F : Type*} [Field F] [DecidableEq F] {W : WeierstrassCurve F}

lemma addX_sub_addX_negY_mul_sq {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
    (W.toAffine.addX x₁ x₂ (W.toAffine.slope x₁ x₂ y₁ y₂) -
        W.toAffine.addX x₁ x₂ (W.toAffine.slope x₁ x₂ y₁ (W.toAffine.negY x₂ y₂))) *
        (x₁ - x₂) ^ 2 =
      -((y₁ - W.toAffine.negY x₁ y₁) * (y₂ - W.toAffine.negY x₂ y₂)) := by
  have e₁ := addX_mul_sq_of_X_ne (W := W.toAffine) y₁ y₂ hx
  have e₂ := addX_mul_sq_of_X_ne (W := W.toAffine) y₁ (W.toAffine.negY x₂ y₂) hx
  rw [sub_mul, e₁, e₂]
  simp only [negY]
  ring

end WeierstrassCurve.Affine

open WeierstrassCurve.Affine

namespace TateCurve

variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] [DecidableEq K]
variable {q u v w ζ t : K} {p : ℕ}

lemma sub_negY_curve (q x y : K) : y - (curve q).toAffine.negY x y = 2 * y + x := by
  rw [negY]
  show y - (-y - (curve q).a₁ * x - (curve q).a₃) = 2 * y + x
  rw [curve_a₁, curve_a₃]
  ring

private lemma point_some_congr {W : WeierstrassCurve K} {x x' y y' : K}
    (hx : x = x') (hy : y = y')
    (h : W.toAffine.Nonsingular x y) (h' : W.toAffine.Nonsingular x' y') :
    (Point.some x y h : W.toAffine.Point) = Point.some x' y' h' := by
  subst hx; subst hy; rfl

section LatticeHelpers

private lemma zpow_ne_one_of_norm_lt_one (hq : ‖q‖₊ < 1) {m : ℤ} (hm : m ≠ 0) :
    q ^ m ≠ 1 := by

  have hpos : ∀ n : ℕ, n ≠ 0 → q ^ n ≠ 1 := by
    intro n hn hcontra
    have h1 : ‖q ^ n‖₊ = 1 := by rw [hcontra, nnnorm_one]
    have h2 : ‖q ^ n‖₊ < 1 := by
      rw [nnnorm_pow]
      exact pow_lt_one₀ zero_le hq hn
    exact absurd h1 (ne_of_lt h2)
  intro hcontra
  rcases lt_trichotomy m 0 with hneg | hzero | hpos'
  ·
    have h1 : q ^ (-m) = 1 := by
      have h2 : (q ^ m)⁻¹ = (1 : K)⁻¹ := by rw [hcontra]
      rwa [← zpow_neg, inv_one] at h2
    have h2 : q ^ ((-m).toNat) = 1 := by
      rw [← zpow_natCast, Int.toNat_of_nonneg (by omega)]
      exact h1
    exact hpos (-m).toNat (by omega) h2
  · exact hm hzero
  · have h2 : q ^ (m.toNat) = 1 := by
      rw [← zpow_natCast, Int.toNat_of_nonneg (by omega)]
      exact hcontra
    exact hpos m.toNat (by omega) h2

private lemma zpow_left_injective_of_norm_lt_one (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {m n : ℤ}
    (h : q ^ m = q ^ n) : m = n := by
  by_contra hmn
  apply zpow_ne_one_of_norm_lt_one hq (sub_ne_zero.mpr hmn)
  rw [sub_eq_add_neg, zpow_add₀ hq0, h, ← zpow_add₀ hq0, add_neg_cancel, zpow_zero]

end LatticeHelpers

section TateParameters

variable {p : ℕ}

lemma tateParam_ne_zero (hζ0 : ζ ≠ 0) (ht0 : t ≠ 0) {i j : ℕ} : ζ ^ i * t ^ j ≠ 0 :=
  mul_ne_zero (pow_ne_zero i hζ0) (pow_ne_zero j ht0)

lemma tateParam_pow (hζp : ζ ^ p = 1) (ht : t ^ p = q) (i j : ℕ) :
    (ζ ^ i * t ^ j) ^ p = q ^ (j : ℤ) := by
  have h1 : (ζ ^ i) ^ p = 1 := by rw [← pow_mul, mul_comm, pow_mul, hζp, one_pow]
  have h2 : (t ^ j) ^ p = q ^ j := by rw [← pow_mul, mul_comm, pow_mul, ht]
  rw [mul_pow, h1, h2, one_mul, zpow_natCast]

lemma tateParam_offLattice (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j : ℕ} (hi : i < p) (hj : j < p) (hij : ¬(i = 0 ∧ j = 0)) :
    OffLattice q (ζ ^ i * t ^ j) := by
  have hζp : ζ ^ p = 1 := hζ.pow_eq_one
  intro n hn

  have h1 : q ^ (n * (p : ℤ) + (j : ℤ)) = 1 := by
    have h2 : (q ^ n * (ζ ^ i * t ^ j)) ^ p = 1 := by rw [hn, one_pow]
    rwa [mul_pow, tateParam_pow hζp ht, ← zpow_natCast (q ^ n) p, ← zpow_mul,
      ← zpow_add₀ hq0] at h2

  have h3 : n * (p : ℤ) + (j : ℤ) = 0 := by
    by_contra h
    exact zpow_ne_one_of_norm_lt_one hq h h1

  have hn0 : n = 0 := by
    rcases lt_trichotomy n 0 with hneg | h0 | hpos
    · exfalso
      have hle : n * (p : ℤ) ≤ (-1) * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
    · exact h0
    · exfalso
      have hle : 1 * (p : ℤ) ≤ n * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
  have hj0 : j = 0 := by
    have h4 : (j : ℤ) = 0 := by
      rw [hn0] at h3
      simpa using h3
    exact_mod_cast h4

  have hi0 : i ≠ 0 := fun h => hij ⟨h, hj0⟩
  have h5 : ζ ^ i = 1 := by
    have h6 := hn
    rw [hn0, zpow_zero, one_mul, hj0, pow_zero, mul_one] at h6
    exact h6
  exact hi0 (hζ.pow_inj hi (by omega) (by rw [h5, pow_zero]))

lemma tateParam_class_eq (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (ht0 : t ≠ 0)
    {i j i' j' : ℕ} (hi : i < p) (hj : j < p) (hi' : i' < p) (hj' : j' < p)
    {k : ℤ} (hk : ζ ^ i' * t ^ j' = q ^ k * (ζ ^ i * t ^ j)) : i = i' ∧ j = j' := by
  have hζp : ζ ^ p = 1 := hζ.pow_eq_one

  have hpow : (q : K) ^ (j' : ℤ) = q ^ (k * (p : ℤ) + (j : ℤ)) := by
    have h1 : (ζ ^ i' * t ^ j') ^ p = (q ^ k * (ζ ^ i * t ^ j)) ^ p := by rw [hk]
    rwa [tateParam_pow hζp ht, mul_pow, tateParam_pow hζp ht, ← zpow_natCast (q ^ k) p,
      ← zpow_mul, ← zpow_add₀ hq0] at h1
  have hjj : (j' : ℤ) = k * (p : ℤ) + (j : ℤ) :=
    zpow_left_injective_of_norm_lt_one hq0 hq hpow

  have hk0 : k = 0 := by
    rcases lt_trichotomy k 0 with hneg | h0 | hpos
    · exfalso
      have hle : k * (p : ℤ) ≤ (-1) * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
    · exact h0
    · exfalso
      have hle : 1 * (p : ℤ) ≤ k * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
  have hjeq : j = j' := by
    have h4 : (j' : ℤ) = (j : ℤ) := by rw [hjj, hk0]; ring
    exact_mod_cast h4.symm

  have hieq : i = i' := by
    have h2 : ζ ^ i' * t ^ j = ζ ^ i * t ^ j := by
      have h3 := hk
      rw [hk0, zpow_zero, one_mul, ← hjeq] at h3
      exact h3
    have h4 : ζ ^ i' = ζ ^ i := mul_right_cancel₀ (pow_ne_zero j ht0) h2
    exact hζ.pow_inj hi hi' h4.symm
  exact ⟨hieq, hjeq⟩

end TateParameters

lemma point_inv_eq_neg (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q u⁻¹) (pointY q u⁻¹))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q u⁻¹) (pointY q u⁻¹) h₁ : (curve q).toAffine.Point)
      = -Point.some (pointX q u) (pointY q u) h₂ := by
  rw [Point.neg_some]
  refine point_some_congr (pointX_inv hq0 hu0 hu) ?_ h₁ _
  rw [pointY_inv hq0 hq hu0 hu, negY]
  show -pointY q u - pointX q u = -pointY q u - (curve q).a₁ * pointX q u - (curve q).a₃
  rw [curve_a₁, curve_a₃]
  ring

theorem point_mul_eq_add_or_sub_of_symAddHyps (hyps : SymAddHyps q)
    (hp : AddParams q v w) (hxne : pointX q v ≠ pointX q w)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (v * w)) (pointY q (v * w)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q v) (pointY q v))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q w) (pointY q w)) :
    (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃ ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = -(Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃) ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = Point.some (pointX q v) (pointY q v) h₂ - Point.some (pointX q w) (pointY q w) h₃ ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = -(Point.some (pointX q v) (pointY q v) h₂ - Point.some (pointX q w) (pointY q w) h₃) := by
  have hd2 : (pointX q v - pointX q w) ^ 2 ≠ 0 := pow_ne_zero 2 (sub_ne_zero.mpr hxne)

  have hS1 := hyps.sum v w hp
  have hS2 := hyps.prod v w hp
  rw [symSumNum_eq_b] at hS1
  rw [symProdNum_eq_b] at hS2

  have hsum := WeierstrassCurve.Affine.addX_add_addX_negY_mul_sq' (W := curve q)
    h₂.left h₃.left hxne
  have hprod := WeierstrassCurve.Affine.addX_mul_addX_negY_mul_sq (W := (curve q).toAffine)
    h₂.left h₃.left hxne

  have hsumEq : pointX q (v * w) + pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) +
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hS1.trans hsum.symm)
  have hprodEq : pointX q (v * w) * pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) *
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hS2.trans hprod.symm)

  have hroot : (pointX q (v * w) -
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w))) *
      (pointX q (v * w) -
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w)))) = 0 := by
    linear_combination pointX q (v * w) * hsumEq - hprodEq
  have hcond : ¬(pointX q v = pointX q w ∧
      pointY q v = (curve q).toAffine.negY (pointX q w) (pointY q w)) :=
    fun hxy => hxne hxy.left
  have hcond' : ¬(pointX q v = pointX q w ∧
      pointY q v = (curve q).toAffine.negY (pointX q w)
        ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    fun hxy => hxne hxy.left
  rcases mul_eq_zero.mp hroot with hcase | hcase
  ·
    have hxeq := sub_eq_zero.mp hcase
    have hns : (curve q).toAffine.Nonsingular
        ((curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)))
        ((curve q).toAffine.addY (pointX q v) (pointX q w) (pointY q v)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w))) :=
      WeierstrassCurve.Affine.nonsingular_add h₂ h₃ hcond
    rcases WeierstrassCurve.Affine.Y_eq_of_X_eq h₁.left hns.left hxeq with hyeq | hyeq
    · left
      rw [Point.add_of_X_ne hxne]
      exact point_some_congr hxeq hyeq h₁ _
    · right; left
      rw [Point.add_of_X_ne hxne, Point.neg_some]
      exact point_some_congr hxeq hyeq h₁ _
  ·
    have hxeq := sub_eq_zero.mp hcase
    have hns : (curve q).toAffine.Nonsingular
        ((curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))))
        ((curve q).toAffine.addY (pointX q v) (pointX q w) (pointY q v)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w)))) :=
      WeierstrassCurve.Affine.nonsingular_add h₂ ((nonsingular_neg _ _).mpr h₃) hcond'
    rcases WeierstrassCurve.Affine.Y_eq_of_X_eq h₁.left hns.left hxeq with hyeq | hyeq
    · right; right; left
      rw [sub_eq_add_neg, Point.neg_some, Point.add_of_X_ne hxne]
      exact point_some_congr hxeq hyeq h₁ _
    · right; right; right
      rw [sub_eq_add_neg, Point.neg_some, Point.add_of_X_ne hxne, Point.neg_some]
      exact point_some_congr hxeq hyeq h₁ _

private lemma muT_norm_eq_one_of_isPrimitiveRoot (hζ : IsPrimitiveRoot ζ p) (hp0 : p ≠ 0) :
    ‖ζ‖ = 1 := by
  have h1 : ‖ζ‖ ^ p = 1 := by rw [← norm_pow, hζ.pow_eq_one, norm_one]
  rcases (pow_eq_one_iff_of_ne_zero hp0).mp h1 with h | ⟨h, _⟩
  · exact h
  · exfalso
    have h2 := norm_nonneg ζ
    rw [h] at h2
    linarith

private lemma offLattice_zeta_pow' (hq0 : q ≠ 0) (hq1 : ‖q‖ < 1) (hζ : IsPrimitiveRoot ζ p)
    (hp0 : p ≠ 0) {k : ℕ} (hk : ¬ p ∣ k) : OffLattice q (ζ ^ k) :=
  offLattice_of_norm_eq_one hq0 hq1
    (by rw [norm_pow, muT_norm_eq_one_of_isPrimitiveRoot hζ hp0, one_pow])
    (fun h1 => hk ((hζ.pow_eq_one_iff_dvd k).mp h1))

theorem point_mul_eq_add_or_neg_of_symAddHyps_of_diff (hyps : SymAddHyps q)
    (hd1 : (pointX q (v * w) - pointX q (v * w⁻¹)) * (pointX q v - pointX q w) ^ 2 =
      -((2 * pointY q v + pointX q v) * (2 * pointY q w + pointX q w)))
    (hp : AddParams q v w) (hxne : pointX q v ≠ pointX q w)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (v * w)) (pointY q (v * w)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q v) (pointY q v))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q w) (pointY q w)) :
    (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃ ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = -(Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃) := by
  have hd2 : (pointX q v - pointX q w) ^ 2 ≠ 0 := pow_ne_zero 2 (sub_ne_zero.mpr hxne)

  have hS1 := hyps.sum v w hp
  rw [symSumNum_eq_b] at hS1
  have hsum := WeierstrassCurve.Affine.addX_add_addX_negY_mul_sq' (W := curve q)
    h₂.left h₃.left hxne
  have hsumEq : pointX q (v * w) + pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) +
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hS1.trans hsum.symm)

  have hdiffC := WeierstrassCurve.Affine.addX_sub_addX_negY_mul_sq (W := curve q)
    (pointY q v) (pointY q w) hxne
  rw [sub_negY_curve, sub_negY_curve] at hdiffC
  have hdiffEq : pointX q (v * w) - pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) -
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hd1.trans hdiffC.symm)

  have hxeq : pointX q (v * w) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
        ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) := by
    have h2 : (2 : K) ≠ 0 := by norm_num
    apply mul_left_cancel₀ h2
    linear_combination hsumEq + hdiffEq

  have hcond : ¬(pointX q v = pointX q w ∧
      pointY q v = (curve q).toAffine.negY (pointX q w) (pointY q w)) :=
    fun hxy => hxne hxy.left
  have hns : (curve q).toAffine.Nonsingular
      ((curve q).toAffine.addX (pointX q v) (pointX q w)
        ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)))
      ((curve q).toAffine.addY (pointX q v) (pointX q w) (pointY q v)
        ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w))) :=
    WeierstrassCurve.Affine.nonsingular_add h₂ h₃ hcond
  rcases WeierstrassCurve.Affine.Y_eq_of_X_eq h₁.left hns.left hxeq with hyeq | hyeq
  · left
    rw [Point.add_of_X_ne hxne]
    exact point_some_congr hxeq hyeq h₁ _
  · right
    rw [Point.add_of_X_ne hxne, Point.neg_some]
    exact point_some_congr hxeq hyeq h₁ _

theorem point_mul_eq_add_of_symAddHyps_of_diffHyp (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hp : AddParams q v w) (hxne : pointX q v ≠ pointX q w)
    (hp' : AddParams q (v * w) v⁻¹) (hxne' : pointX q (v * w) ≠ pointX q v)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (v * w)) (pointY q (v * w)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q v) (pointY q v))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q w) (pointY q w))
    (hP2 : (Point.some (pointX q v) (pointY q v) h₂ : (curve q).toAffine.Point)
        + Point.some (pointX q v) (pointY q v) h₂ ≠ 0) :
    (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
      = Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃ := by

  have hvw0 : v * w ≠ 0 := mul_ne_zero hp.u_ne_zero hp.v_ne_zero
  have hprod0 : (v * w) * v⁻¹ ≠ 0 := mul_ne_zero hvw0 (inv_ne_zero hp.u_ne_zero)
  have h₄ : (curve q).toAffine.Nonsingular (pointX q ((v * w) * v⁻¹)) (pointY q ((v * w) * v⁻¹)) :=
    nonsingular_point hq0 hq hprod0 hp'.offLattice_mul
  have hinv0 : v⁻¹ ≠ 0 := inv_ne_zero hp.u_ne_zero
  have hinvOff : OffLattice q v⁻¹ := OffLattice.inv hq0 hp.offLattice_u
  have h₅ : (curve q).toAffine.Nonsingular (pointX q v⁻¹) (pointY q v⁻¹) :=
    nonsingular_point hq0 hq hinv0 hinvOff

  set R := (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
    with hR_def
  set P := (Point.some (pointX q v) (pointY q v) h₂ : (curve q).toAffine.Point) with hP_def
  set Q := (Point.some (pointX q w) (pointY q w) h₃ : (curve q).toAffine.Point) with hQ_def

  have hxneDer : pointX q (v * w) ≠ pointX q v⁻¹ := by
    rw [pointX_inv hq0 hp.u_ne_zero hp.offLattice_u]
    exact hxne'
  have hder := point_mul_eq_add_or_neg_of_symAddHyps_of_diff hyps
    (hdiff (v * w) v⁻¹ hp') hp' hxneDer h₄ h₁ h₅

  have helem : (v * w) * v⁻¹ = w := by
    rw [mul_comm v w, mul_assoc, mul_inv_cancel₀ hp.u_ne_zero, mul_one]
  have e₄ : (Point.some (pointX q ((v * w) * v⁻¹)) (pointY q ((v * w) * v⁻¹)) h₄ :
      (curve q).toAffine.Point) = Q :=
    point_some_congr (congrArg (pointX q) helem) (congrArg (pointY q) helem) h₄ h₃
  have e₅ : (Point.some (pointX q v⁻¹) (pointY q v⁻¹) h₅ : (curve q).toAffine.Point) = -P :=
    point_inv_eq_neg hq0 hq hp.u_ne_zero hp.offLattice_u h₅ h₂
  rw [e₄, e₅] at hder

  rcases hder with hder | hder
  ·
    calc R = P + (R + -P) := by abel
      _ = P + Q := by rw [← hder]
  ·
    rcases point_mul_eq_add_or_neg_of_symAddHyps_of_diff hyps (hdiff v w hp) hp hxne h₁ h₂ h₃
      with hmain | hmain
    · exact hmain
    ·
      exfalso
      apply hP2
      have k1 : R + (P + Q) = 0 := by rw [hR_def, hmain]; abel
      have k2 : Q + (R + -P) = 0 := by rw [hder]; abel
      calc P + P = (R + (P + Q)) - (Q + (R + -P)) := by abel
        _ = 0 - 0 := by rw [k1, k2]
        _ = 0 := by abel

theorem zeta_pow_mul_self_point_eq_add (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p) (hpp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a))) :
    (Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) h₁ :
        (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂
          + Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ := by

  have hp0 : p ≠ 0 := by omega
  have hζ0 : ζ ≠ 0 := hζ.ne_zero hp0
  have hζa0 : ζ ^ a ≠ 0 := pow_ne_zero _ hζ0
  have hq1 : ‖q‖ < 1 := by exact_mod_cast hq
  have hnζ : ‖ζ‖ = 1 := muT_norm_eq_one_of_isPrimitiveRoot hζ hp0
  have hnζa : ‖ζ ^ a‖ = 1 := by rw [norm_pow, hnζ, one_pow]
  have hndvd_a : ¬ p ∣ a := fun hdvd =>
    absurd (Nat.le_of_dvd (by omega) hdvd) (by omega)
  have hndvd_2a : ¬ p ∣ a + a := by
    intro hdvd
    rw [← two_mul a] at hdvd
    rcases (Nat.Prime.dvd_mul hpp).mp hdvd with h2 | ha
    · exact absurd (Nat.le_of_dvd (by norm_num) h2) (by omega)
    · exact hndvd_a ha
  have hndvd_3a : ¬ p ∣ a + a + a := by
    intro hdvd
    have h3a : a + a + a = 3 * a := by ring
    rw [h3a] at hdvd
    rcases (Nat.Prime.dvd_mul hpp).mp hdvd with h3 | ha
    · exact absurd (Nat.le_of_dvd (by norm_num) h3) (by omega)
    · exact hndvd_a ha
  have hndvd_pa : ¬ p ∣ p - a := fun hdvd =>
    absurd (Nat.le_of_dvd (by omega) hdvd) (by omega)

  have hζaOff : OffLattice q (ζ ^ a) := offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_a
  have hζ2aOff : OffLattice q (ζ ^ a * ζ ^ a) := by
    rw [← pow_add]
    exact offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_2a
  have hζpaOff : OffLattice q (ζ ^ (p - a)) := offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_pa

  have hpa_inv : ζ ^ (p - a) = (ζ ^ a)⁻¹ := by
    have hcancel : ζ ^ a * ζ ^ (p - a) = ζ ^ a * (ζ ^ a)⁻¹ := by
      rw [mul_inv_cancel₀ hζa0, ← pow_add, show a + (p - a) = p by omega, hζ.pow_eq_one]
    exact mul_left_cancel₀ hζa0 hcancel

  have helem1 : (ζ ^ a * ζ ^ a) * ζ ^ (p - a) = ζ ^ a := by
    rw [mul_assoc, ← pow_add, show a + (p - a) = p by omega, hζ.pow_eq_one, mul_one]

  have hpDouble : AddParams q (ζ ^ a * ζ ^ a) (ζ ^ (p - a)) := by
    refine ⟨hq0, mul_ne_zero hζa0 hζa0, pow_ne_zero _ hζ0, hζ2aOff, hζpaOff, ?_, ?_⟩
    · rw [helem1]; exact hζaOff
    · have helem2 : (ζ ^ a * ζ ^ a) * (ζ ^ (p - a))⁻¹ = ζ ^ (a + a + a) := by
        rw [hpa_inv, inv_inv, ← pow_add, ← pow_add]
      rw [helem2]
      exact offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_3a

  have hxneDouble : pointX q (ζ ^ a * ζ ^ a) ≠ pointX q (ζ ^ (p - a)) := by
    intro hX
    rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq (mul_ne_zero hζa0 hζa0) (pow_ne_zero _ hζ0)
      hζ2aOff hζpaOff
      (le_of_eq (by rw [norm_mul, hnζa, one_mul]))
      (le_of_eq (by rw [norm_pow, hnζ, one_pow]))
      (by rw [helem1, hnζa]; exact hq1) hX with heq | hone
    ·
      apply hndvd_3a
      have h1 : ζ ^ (a + a + a) = 1 := by
        rw [pow_add, pow_add, heq, ← pow_add, show p - a + a = p by omega, hζ.pow_eq_one]
      exact (hζ.pow_eq_one_iff_dvd _).mp h1
    ·
      rw [helem1] at hone
      exact hndvd_a ((hζ.pow_eq_one_iff_dvd a).mp hone)

  have hprodNs : (curve q).toAffine.Nonsingular (pointX q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a)))
      (pointY q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a))) :=
    nonsingular_point hq0 hq (mul_ne_zero (mul_ne_zero hζa0 hζa0) (pow_ne_zero _ hζ0))
      hpDouble.offLattice_mul
  have hwNs : (curve q).toAffine.Nonsingular (pointX q (ζ ^ (p - a))) (pointY q (ζ ^ (p - a))) :=
    nonsingular_point hq0 hq (pow_ne_zero _ hζ0) hζpaOff

  have hcase := point_mul_eq_add_or_neg_of_symAddHyps_of_diff hyps
    (hdiff (ζ ^ a * ζ ^ a) (ζ ^ (p - a)) hpDouble) hpDouble hxneDouble hprodNs h₁ hwNs

  have e1 : (Point.some (pointX q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a)))
      (pointY q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a))) hprodNs : (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :=
    point_some_congr (congrArg (pointX q) helem1) (congrArg (pointY q) helem1) hprodNs h₂
  have hwNs' : (curve q).toAffine.Nonsingular (pointX q ((ζ ^ a)⁻¹)) (pointY q ((ζ ^ a)⁻¹)) := by
    rw [← hpa_inv]
    exact hwNs
  have e2 : (Point.some (pointX q (ζ ^ (p - a))) (pointY q (ζ ^ (p - a))) hwNs :
      (curve q).toAffine.Point)
      = -(Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂) := by
    have e2' : (Point.some (pointX q (ζ ^ (p - a))) (pointY q (ζ ^ (p - a))) hwNs :
        (curve q).toAffine.Point)
        = Point.some (pointX q ((ζ ^ a)⁻¹)) (pointY q ((ζ ^ a)⁻¹)) hwNs' :=
      point_some_congr (congrArg (pointX q) hpa_inv) (congrArg (pointY q) hpa_inv) hwNs hwNs'
    rw [e2']
    exact point_inv_eq_neg hq0 hq hζa0 hζaOff hwNs' h₂
  rw [e1, e2] at hcase

  set P2 := (Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) h₁ :
    (curve q).toAffine.Point) with hP2_def
  set P1 := (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
    (curve q).toAffine.Point) with hP1_def
  rcases hcase with hc | hc
  ·
    calc P2 = (P2 + -P1) + P1 := by abel
      _ = P1 + P1 := by rw [← hc]
  ·
    exfalso
    have k : P1 + (P2 + -P1) = 0 := by
      nth_rewrite 1 [hc]
      abel
    have h0 : P2 = 0 := by
      calc P2 = P1 + (P2 + -P1) := by abel
        _ = 0 := k
    exact Point.some_ne_zero h₁ h0

private lemma muTranslation_aux (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p) (hpp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u) (hau : OffLattice q (ζ ^ a * u))
    (hule : ‖u‖ ≤ 1) (hqlt : ‖q‖ < ‖u‖)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a)))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ : (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂
          + Point.some (pointX q u) (pointY q u) h₃ := by

  have hp0 : p ≠ 0 := by omega
  have hζ0 : ζ ≠ 0 := hζ.ne_zero hp0
  have hζa0 : ζ ^ a ≠ 0 := pow_ne_zero _ hζ0
  have hq1 : ‖q‖ < 1 := by exact_mod_cast hq
  have hnζ : ‖ζ‖ = 1 := muT_norm_eq_one_of_isPrimitiveRoot hζ hp0
  have hnζa : ‖ζ ^ a‖ = 1 := by rw [norm_pow, hnζ, one_pow]
  have hndvd_a : ¬ p ∣ a := fun hdvd =>
    absurd (Nat.le_of_dvd (by omega) hdvd) (by omega)
  have hndvd_2a : ¬ p ∣ a + a := by
    intro hdvd
    rw [← two_mul a] at hdvd
    rcases (Nat.Prime.dvd_mul hpp).mp hdvd with h2 | ha
    · exact absurd (Nat.le_of_dvd (by norm_num) h2) (by omega)
    · exact hndvd_a ha
  have hζaOff : OffLattice q (ζ ^ a) := offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_a
  have hζ2aOff : OffLattice q (ζ ^ a * ζ ^ a) := by
    rw [← pow_add]
    exact offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_2a

  have hDns : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * ζ ^ a))
      (pointY q (ζ ^ a * ζ ^ a)) :=
    nonsingular_point hq0 hq (mul_ne_zero hζa0 hζa0) hζ2aOff

  by_cases hC2 : OffLattice q (ζ ^ a * u⁻¹)
  · by_cases hC4 : OffLattice q (ζ ^ a * ζ ^ a * u)
    ·
      have hpMain : AddParams q (ζ ^ a) u := ⟨hq0, hζa0, hu0, hζaOff, hu, hau, hC2⟩
      have hxneMain : pointX q (ζ ^ a) ≠ pointX q u := by
        intro hX
        rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq hζa0 hu0 hζaOff hu (le_of_eq hnζa) hule
          (by rw [norm_mul, hnζa, one_mul]; exact hqlt) hX with heq | hone
        ·
          apply hC2 0
          rw [zpow_zero, one_mul, heq, mul_inv_cancel₀ hu0]
        ·
          exact hau 0 (by rw [zpow_zero, one_mul]; exact hone)
      have hpDer : AddParams q (ζ ^ a * u) (ζ ^ a)⁻¹ := by
        refine ⟨hq0, mul_ne_zero hζa0 hu0, inv_ne_zero hζa0, hau,
          OffLattice.inv hq0 hζaOff, ?_, ?_⟩
        · have helem : (ζ ^ a * u) * (ζ ^ a)⁻¹ = u := by
            rw [mul_comm (ζ ^ a) u, mul_assoc, mul_inv_cancel₀ hζa0, mul_one]
          rw [helem]; exact hu
        · have helem : (ζ ^ a * u) * ((ζ ^ a)⁻¹)⁻¹ = ζ ^ a * ζ ^ a * u := by
            rw [inv_inv]; ring
          rw [helem]; exact hC4
      have hxneDer : pointX q (ζ ^ a * u) ≠ pointX q (ζ ^ a) := by
        intro hX
        rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq (mul_ne_zero hζa0 hu0) hζa0 hau hζaOff
          (by rw [norm_mul, hnζa, one_mul]; exact hule) (le_of_eq hnζa)
          (by rw [norm_mul, norm_mul, hnζa, one_mul, mul_one]; exact hqlt) hX with heq | hone
        ·
          have hu1 : u = 1 := by
            have h := heq.trans (mul_one (ζ ^ a)).symm
            exact mul_left_cancel₀ hζa0 h
          exact hu 0 (by rw [zpow_zero, one_mul, hu1])
        ·
          apply hC4 0
          rw [zpow_zero, one_mul]
          calc ζ ^ a * ζ ^ a * u = (ζ ^ a * u) * ζ ^ a := by ring
            _ = 1 := hone

      have hP2 : (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
          (curve q).toAffine.Point)
          + Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ ≠ 0 := by
        intro h2tor
        have hodd : Odd p := hpp.odd_of_ne_two (by omega)
        have hpow : (ζ ^ a) ^ p = q ^ (0 : ℤ) := by
          rw [← pow_mul, mul_comm a p, pow_mul, hζ.pow_eq_one, one_pow, zpow_zero]
        have hptor : p • (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
            (curve q).toAffine.Point) = 0 :=
          nsmul_prime_eq_zero hyps hq0 hq hζa0 hζaOff hpow hpp hodd h₂
        set PT := (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
          (curve q).toAffine.Point) with hPT_def
        obtain ⟨k, hk⟩ := hodd
        have hk' : p = k + k + 1 := by omega
        have hpP : p • PT = PT := by
          calc p • PT = (k + k + 1) • PT := by rw [← hk']
            _ = k • PT + k • PT + PT := by rw [add_nsmul, add_nsmul, one_nsmul]
            _ = k • (PT + PT) + PT := by rw [← nsmul_add]
            _ = PT := by rw [h2tor, smul_zero, zero_add]
        have h0 : PT = 0 := by rw [← hpP, hptor]
        exact Point.some_ne_zero h₂ h0
      exact point_mul_eq_add_of_symAddHyps_of_diffHyp hyps hdiff hq0 hq hpMain hxneMain hpDer
        hxneDer h₁ h₂ h₃ hP2
    ·
      have hdouble := zeta_pow_mul_self_point_eq_add hyps hdiff hq0 hq hp5 hpp hζ ha1 hap hDns h₂
      have hC4' : ∃ n : ℤ, q ^ n * (ζ ^ a * ζ ^ a * u) = 1 := by
        by_contra hcon
        exact hC4 (fun n hn => hcon ⟨n, hn⟩)
      obtain ⟨n, hn⟩ := hC4'

      have hqn0 : (q : K) ^ n ≠ 0 := zpow_ne_zero _ hq0
      have hzu_eq : ζ ^ a * u = q ^ (-n) * (ζ ^ a)⁻¹ := by
        have hcancel : (q ^ n * ζ ^ a) * (ζ ^ a * u) =
            (q ^ n * ζ ^ a) * (q ^ (-n) * (ζ ^ a)⁻¹) := by
          rw [show (q ^ n * ζ ^ a) * (ζ ^ a * u) = q ^ n * (ζ ^ a * ζ ^ a * u) by ring, hn,
            show (q ^ n * ζ ^ a) * (q ^ (-n) * (ζ ^ a)⁻¹) =
              (q ^ n * q ^ (-n)) * (ζ ^ a * (ζ ^ a)⁻¹) by ring,
            ← zpow_add₀ hq0, show n + -n = 0 by omega, zpow_zero,
            mul_inv_cancel₀ hζa0, mul_one]
        exact mul_left_cancel₀ (mul_ne_zero hqn0 hζa0) hcancel
      have hu_eq : u = q ^ (-n) * (ζ ^ a * ζ ^ a)⁻¹ := by
        have hcancel : (q ^ n * (ζ ^ a * ζ ^ a)) * u =
            (q ^ n * (ζ ^ a * ζ ^ a)) * (q ^ (-n) * (ζ ^ a * ζ ^ a)⁻¹) := by
          rw [show (q ^ n * (ζ ^ a * ζ ^ a)) * u = q ^ n * (ζ ^ a * ζ ^ a * u) by ring, hn,
            show (q ^ n * (ζ ^ a * ζ ^ a)) * (q ^ (-n) * (ζ ^ a * ζ ^ a)⁻¹) =
              (q ^ n * q ^ (-n)) * ((ζ ^ a * ζ ^ a) * (ζ ^ a * ζ ^ a)⁻¹) by ring,
            ← zpow_add₀ hq0, show n + -n = 0 by omega, zpow_zero,
            mul_inv_cancel₀ (mul_ne_zero hζa0 hζa0), mul_one]
        exact mul_left_cancel₀ (mul_ne_zero hqn0 (mul_ne_zero hζa0 hζa0)) hcancel

      have hXzu : pointX q (ζ ^ a * u) = pointX q (ζ ^ a) := by
        rw [hzu_eq, pointX_zpow_mul hq0, pointX_inv hq0 hζa0 hζaOff]
      have hYzu : pointY q (ζ ^ a * u) = -pointY q (ζ ^ a) - pointX q (ζ ^ a) := by
        rw [hzu_eq, pointY_zpow_mul hq0, pointY_inv hq0 hq hζa0 hζaOff]
      have hXu : pointX q u = pointX q (ζ ^ a * ζ ^ a) := by
        rw [hu_eq, pointX_zpow_mul hq0, pointX_inv hq0 (mul_ne_zero hζa0 hζa0) hζ2aOff]
      have hYu : pointY q u = -pointY q (ζ ^ a * ζ ^ a) - pointX q (ζ ^ a * ζ ^ a) := by
        rw [hu_eq, pointY_zpow_mul hq0, pointY_inv hq0 hq (mul_ne_zero hζa0 hζa0) hζ2aOff]

      have hL : (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
          (curve q).toAffine.Point)
          = -(Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂) := by
        rw [Point.neg_some]
        refine point_some_congr hXzu ?_ h₁ _
        rw [hYzu, negY]
        show -pointY q (ζ ^ a) - pointX q (ζ ^ a) =
          -pointY q (ζ ^ a) - (curve q).a₁ * pointX q (ζ ^ a) - (curve q).a₃
        rw [curve_a₁, curve_a₃]
        ring
      have hU : (Point.some (pointX q u) (pointY q u) h₃ : (curve q).toAffine.Point)
          = -(Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) hDns) := by
        rw [Point.neg_some]
        refine point_some_congr hXu ?_ h₃ _
        rw [hYu, negY]
        show -pointY q (ζ ^ a * ζ ^ a) - pointX q (ζ ^ a * ζ ^ a) =
          -pointY q (ζ ^ a * ζ ^ a) - (curve q).a₁ * pointX q (ζ ^ a * ζ ^ a) - (curve q).a₃
        rw [curve_a₁, curve_a₃]
        ring
      rw [hL, hU, hdouble]
      abel
  ·

    have hdouble := zeta_pow_mul_self_point_eq_add hyps hdiff hq0 hq hp5 hpp hζ ha1 hap hDns h₂
    have hC2' : ∃ n : ℤ, q ^ n * (ζ ^ a * u⁻¹) = 1 := by
      by_contra hcon
      exact hC2 (fun n hn => hcon ⟨n, hn⟩)
    obtain ⟨n, hn⟩ := hC2'

    have hu_eq : u = q ^ n * ζ ^ a := by
      have h1 : (q ^ n * (ζ ^ a * u⁻¹)) * u = u := by rw [hn, one_mul]
      have h2 : (q ^ n * ζ ^ a) * (u⁻¹ * u) = u := by
        calc (q ^ n * ζ ^ a) * (u⁻¹ * u) = (q ^ n * (ζ ^ a * u⁻¹)) * u := by ring
          _ = u := h1
      rw [inv_mul_cancel₀ hu0, mul_one] at h2
      exact h2.symm

    have hXu : pointX q u = pointX q (ζ ^ a) := by rw [hu_eq, pointX_zpow_mul hq0]
    have hYu : pointY q u = pointY q (ζ ^ a) := by rw [hu_eq, pointY_zpow_mul hq0]
    have hzu_eq : ζ ^ a * u = q ^ n * (ζ ^ a * ζ ^ a) := by rw [hu_eq]; ring
    have hXzu : pointX q (ζ ^ a * u) = pointX q (ζ ^ a * ζ ^ a) := by
      rw [hzu_eq, pointX_zpow_mul hq0]
    have hYzu : pointY q (ζ ^ a * u) = pointY q (ζ ^ a * ζ ^ a) := by
      rw [hzu_eq, pointY_zpow_mul hq0]
    have hL : (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
        (curve q).toAffine.Point)
        = Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) hDns :=
      point_some_congr hXzu hYzu h₁ hDns
    have hU : (Point.some (pointX q u) (pointY q u) h₃ : (curve q).toAffine.Point)
        = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :=
      point_some_congr hXu hYu h₃ h₂
    rw [hL, hU]
    exact hdouble

theorem muTranslation_of_symAddHyps_of_diffHyp (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p) (hpp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) :
    MuTranslation q ζ p := by
  intro a ha1 hap u hu0 hu hau h₁ h₂ h₃

  have hq1 : ‖q‖ < 1 := by exact_mod_cast hq
  have hqpos : (0 : ℝ) < ‖q‖ := norm_pos_iff.mpr hq0
  have hupos : (0 : ℝ) < ‖u‖ := norm_pos_iff.mpr hu0
  obtain ⟨m, hm⟩ := exists_mem_Ioc_zpow (x := ‖u‖) (y := ‖q‖⁻¹) hupos
    ((one_lt_inv₀ hqpos).mpr hq1)
  have hinv_zpow : ∀ k : ℤ, (‖q‖⁻¹) ^ k = ‖q‖ ^ (-k) := by
    intro k
    rw [inv_zpow, ← zpow_neg]

  set u' := q ^ (m + 1) * u with hu'_def
  have hu'0 : u' ≠ 0 := mul_ne_zero (zpow_ne_zero _ hq0) hu0
  have hu' : OffLattice q u' := OffLattice.zpow_mul hq0 (m + 1) hu
  have hau' : OffLattice q (ζ ^ a * u') := by
    have helem : ζ ^ a * u' = q ^ (m + 1) * (ζ ^ a * u) := by rw [hu'_def]; ring
    rw [helem]
    exact OffLattice.zpow_mul hq0 (m + 1) hau

  have hnorm_u' : ‖u'‖ = ‖q‖ ^ (m + 1) * ‖u‖ := by
    rw [hu'_def, norm_mul, norm_zpow]
  have hu'le : ‖u'‖ ≤ 1 := by
    rw [hnorm_u']
    have h1 : ‖u‖ ≤ ‖q‖ ^ (-(m + 1)) := by
      have h2 := hm.2
      rwa [hinv_zpow (m + 1)] at h2
    calc ‖q‖ ^ (m + 1) * ‖u‖ ≤ ‖q‖ ^ (m + 1) * ‖q‖ ^ (-(m + 1)) :=
          mul_le_mul_of_nonneg_left h1 (le_of_lt (zpow_pos hqpos _))
      _ = 1 := by
          rw [← zpow_add₀ (ne_of_gt hqpos), show m + 1 + -(m + 1) = 0 by omega, zpow_zero]
  have hu'gt : ‖q‖ < ‖u'‖ := by
    rw [hnorm_u']
    have h1 : ‖q‖ ^ (-m) < ‖u‖ := by
      have h2 := hm.1
      rwa [hinv_zpow m] at h2
    calc ‖q‖ = ‖q‖ ^ (m + 1) * ‖q‖ ^ (-m) := by
          rw [← zpow_add₀ (ne_of_gt hqpos), show m + 1 + -m = 1 by omega, zpow_one]
      _ < ‖q‖ ^ (m + 1) * ‖u‖ := mul_lt_mul_of_pos_left h1 (zpow_pos hqpos _)

  have hXu' : pointX q u' = pointX q u := by rw [hu'_def, pointX_zpow_mul hq0]
  have hYu' : pointY q u' = pointY q u := by rw [hu'_def, pointY_zpow_mul hq0]
  have hzuelem : ζ ^ a * u' = q ^ (m + 1) * (ζ ^ a * u) := by rw [hu'_def]; ring
  have hXzu' : pointX q (ζ ^ a * u') = pointX q (ζ ^ a * u) := by
    rw [hzuelem, pointX_zpow_mul hq0]
  have hYzu' : pointY q (ζ ^ a * u') = pointY q (ζ ^ a * u) := by
    rw [hzuelem, pointY_zpow_mul hq0]

  have h₁' : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * u')) (pointY q (ζ ^ a * u')) := by
    rw [hXzu', hYzu']; exact h₁
  have h₃' : (curve q).toAffine.Nonsingular (pointX q u') (pointY q u') := by
    rw [hXu', hYu']; exact h₃

  have haux := muTranslation_aux hyps hdiff hq0 hq hp5 hpp hζ ha1 hap hu'0 hu' hau'
    hu'le hu'gt h₁' h₂ h₃'
  have e₁ : (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
      (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a * u')) (pointY q (ζ ^ a * u')) h₁' :=
    point_some_congr hXzu'.symm hYzu'.symm h₁ h₁'
  have e₃ : (Point.some (pointX q u) (pointY q u) h₃ : (curve q).toAffine.Point)
      = Point.some (pointX q u') (pointY q u') h₃' :=
    point_some_congr hXu'.symm hYu'.symm h₃ h₃'
  rw [e₁, e₃]
  exact haux

lemma zeta_pow_mod (hζp : ζ ^ p = 1) (n : ℕ) : ζ ^ n = ζ ^ (n % p) := by
  conv_lhs => rw [← Nat.mod_add_div n p]
  rw [pow_add, pow_mul, hζp, one_pow, mul_one]

lemma offLattice_zeta_pow (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hζ : IsPrimitiveRoot ζ p)
    (ht : t ^ p = q) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p) : OffLattice q (ζ ^ a) := by
  have hp0 : 0 < p := lt_of_le_of_lt (Nat.zero_le a) hap
  have h := tateParam_offLattice (t := t) hq0 hq hζ ht hap hp0 (fun h => by omega)
  rwa [pow_zero, mul_one] at h

lemma zeta_pow_point_eq_nsmul (hμ : MuTranslation q ζ p) (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hp : p.Prime) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (hζpt : (curve q).toAffine.Nonsingular (pointX q ζ) (pointY q ζ)) :
    ∀ a : ℕ, 1 ≤ a → a < p →
      ∀ h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a)),
        (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₁ : (curve q).toAffine.Point)
          = a • Point.some (pointX q ζ) (pointY q ζ) hζpt := by
  have hζ0 : ζ ≠ 0 := fun h0 => by
    have hζp := hζ.pow_eq_one
    rw [h0, zero_pow hp.ne_zero] at hζp
    exact zero_ne_one hζp
  intro a
  induction a with
  | zero => intro h; omega
  | succ n ih =>
    intro _ hlt h₁
    rcases Nat.lt_or_ge n 1 with h2 | h2
    ·
      have hn0 : n = 0 := by omega
      subst hn0
      have hx : ζ ^ 1 = ζ := pow_one ζ
      rw [one_nsmul]
      exact point_some_congr (congrArg (pointX q) hx) (congrArg (pointY q) hx) h₁ hζpt
    ·
      have hnp : n < p := by omega
      have hparam : ζ ^ 1 * ζ ^ n = ζ ^ (n + 1) := by
        rw [pow_one, mul_comm, ← pow_succ]
      have hu0 : (ζ : K) ^ n ≠ 0 := pow_ne_zero _ hζ0
      have huoff : OffLattice q (ζ ^ n) := offLattice_zeta_pow hq0 hq hζ ht h2 hnp
      have hprodoff : OffLattice q (ζ ^ 1 * ζ ^ n) := by
        have h := offLattice_zeta_pow hq0 hq hζ ht (a := n + 1) (by omega) hlt
        rwa [← hparam] at h
      have h₁' : (curve q).toAffine.Nonsingular (pointX q (ζ ^ 1 * ζ ^ n))
          (pointY q (ζ ^ 1 * ζ ^ n)) := by rw [hparam]; exact h₁
      have h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ 1)) (pointY q (ζ ^ 1)) := by
        rw [pow_one]; exact hζpt
      have hns_n : (curve q).toAffine.Nonsingular (pointX q (ζ ^ n)) (pointY q (ζ ^ n)) :=
        nonsingular_point hq0 hq hu0 huoff
      have htrans := hμ 1 le_rfl (by omega) (ζ ^ n) hu0 huoff hprodoff h₁' h₂ hns_n
      calc (Point.some (pointX q (ζ ^ (n + 1))) (pointY q (ζ ^ (n + 1))) h₁ :
              (curve q).toAffine.Point)
          = Point.some (pointX q (ζ ^ 1 * ζ ^ n)) (pointY q (ζ ^ 1 * ζ ^ n)) h₁' :=
            point_some_congr (congrArg (pointX q) hparam.symm)
              (congrArg (pointY q) hparam.symm) h₁ h₁'
        _ = Point.some (pointX q (ζ ^ 1)) (pointY q (ζ ^ 1)) h₂
              + Point.some (pointX q (ζ ^ n)) (pointY q (ζ ^ n)) hns_n := htrans
        _ = Point.some (pointX q ζ) (pointY q ζ) hζpt
              + Point.some (pointX q (ζ ^ n)) (pointY q (ζ ^ n)) hns_n := by
            congr 1
            exact point_some_congr (congrArg (pointX q) (pow_one ζ))
              (congrArg (pointY q) (pow_one ζ)) h₂ hζpt
        _ = Point.some (pointX q ζ) (pointY q ζ) hζpt
              + n • Point.some (pointX q ζ) (pointY q ζ) hζpt := by
            rw [ih h2 hnp hns_n]
        _ = (n + 1) • Point.some (pointX q ζ) (pointY q ζ) hζpt := by
            rw [add_comm, ← succ_nsmul]

end TateCurve

namespace TateCurve

variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] [DecidableEq K] [IsAlgClosed K]
variable {q ζ t : K} {p : ℕ}

section UnconditionalCascade

theorem muTranslation_unconditional (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p)
    (hpp : p.Prime) (hζ : IsPrimitiveRoot ζ p) : MuTranslation q ζ p :=
  muTranslation_of_symAddHyps_of_diffHyp (symAddHyps_unconditional hq0 hq)
    (diffHyp_unconditional hq0 (by exact_mod_cast hq)) hq0 hq hp5 hpp hζ

theorem nsmul_prime_eq_zero_unconditional (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u) {s : ℤ}
    (hpow : u ^ p = q ^ s) (hp : p.Prime) (hodd : Odd p)
    (hns : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    p • (Point.some (pointX q u) (pointY q u) hns : (curve q).toAffine.Point) = 0 :=
  nsmul_prime_eq_zero (symAddHyps_unconditional hq0 hq) hq0 hq hu0 hu hpow hp hodd hns

theorem eq_zpow_mul_of_pointXY_eq_unconditional (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    {u v : K} (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu : OffLattice q u) (hv : OffLattice q v)
    {su sv : ℤ} (hpu : u ^ p = q ^ su) (hpv : v ^ p = q ^ sv)
    (hp : p.Prime) (hodd : Odd p)
    (hX : pointX q u = pointX q v) (hY : pointY q u = pointY q v) :
    ∃ k : ℤ, v = q ^ k * u :=
  eq_zpow_mul_of_pointXY_eq (symAddHyps_unconditional hq0 hq) hq0 hq hu0 hv0 hu hv
    hpu hpv hp hodd hX hY

end UnconditionalCascade

section Parametrization

private lemma zeta_ne_zero (hp : p.Prime) (hζ : IsPrimitiveRoot ζ p) : ζ ≠ 0 := by
  intro h0
  have hζp : ζ ^ p = 1 := hζ.pow_eq_one
  rw [h0, zero_pow hp.ne_zero] at hζp
  exact zero_ne_one hζp

private lemma troot_ne_zero (hq0 : q ≠ 0) (hp : p.Prime) (ht : t ^ p = q) : t ≠ 0 := by
  intro h0
  exact hq0 (by rw [← ht, h0, zero_pow hp.ne_zero])

variable (q ζ t) in

noncomputable def tateTorsionPoint (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (i j : ℕ) : (curve q).toAffine.Point :=
  if hij : i < p ∧ j < p ∧ ¬(i = 0 ∧ j = 0) then
    Point.some (pointX q (ζ ^ i * t ^ j)) (pointY q (ζ ^ i * t ^ j))
      (nonsingular_point hq0 hq
        (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht))
        (tateParam_offLattice hq0 hq hζ ht hij.1 hij.2.1 hij.2.2))
  else 0

lemma tateTorsionPoint_spec (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j : ℕ} (hi : i < p) (hj : j < p) (hij : ¬(i = 0 ∧ j = 0)) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht i j
      = Point.some (pointX q (ζ ^ i * t ^ j)) (pointY q (ζ ^ i * t ^ j))
          (nonsingular_point hq0 hq
            (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht))
            (tateParam_offLattice hq0 hq hζ ht hi hj hij)) := by
  rw [tateTorsionPoint, dif_pos ⟨hi, hj, hij⟩]

@[simp] lemma tateTorsionPoint_zero_zero (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht 0 0 = 0 := by
  rw [tateTorsionPoint, dif_neg (fun h => h.2.2 ⟨rfl, rfl⟩)]

lemma tateTorsionPoint_ne_zero (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j : ℕ} (hi : i < p) (hj : j < p) (hij : ¬(i = 0 ∧ j = 0)) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht i j ≠ 0 := by
  rw [tateTorsionPoint_spec hq0 hq hp hζ ht hi hj hij]
  exact Point.some_ne_zero _

lemma nsmul_tateTorsionPoint (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (i j : ℕ) :
    p • tateTorsionPoint q ζ t hq0 hq hp hζ ht i j = 0 := by
  by_cases hij : i < p ∧ j < p ∧ ¬(i = 0 ∧ j = 0)
  · rw [tateTorsionPoint_spec hq0 hq hp hζ ht hij.1 hij.2.1 hij.2.2]
    exact nsmul_prime_eq_zero_unconditional hq0 hq
      (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht))
      (tateParam_offLattice hq0 hq hζ ht hij.1 hij.2.1 hij.2.2)
      (tateParam_pow hζ.pow_eq_one ht i j) hp (hp.odd_of_ne_two (by omega)) _
  · rw [tateTorsionPoint, dif_neg hij, smul_zero]

lemma tateTorsionPoint_mem (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (i j : ℕ) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht i j
      ∈ Submodule.torsionBy ℤ (curve q).toAffine.Point p := by
  rw [Submodule.mem_torsionBy_iff, natCast_zsmul]
  exact nsmul_tateTorsionPoint hq0 hq hp hp5 hζ ht i j

lemma tateTorsionPoint_injOn (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j i' j' : ℕ} (hi : i < p) (hj : j < p) (hi' : i' < p)
    (hj' : j' < p)
    (hpp : tateTorsionPoint q ζ t hq0 hq hp hζ ht i j
      = tateTorsionPoint q ζ t hq0 hq hp hζ ht i' j') : i = i' ∧ j = j' := by
  have hζ0 : ζ ≠ 0 := zeta_ne_zero hp hζ
  have ht0 : t ≠ 0 := troot_ne_zero hq0 hp ht
  by_cases hij : i = 0 ∧ j = 0
  · by_cases hij' : i' = 0 ∧ j' = 0
    · exact ⟨hij.1.trans hij'.1.symm, hij.2.trans hij'.2.symm⟩
    · exfalso
      rw [hij.1, hij.2, tateTorsionPoint_zero_zero] at hpp
      exact tateTorsionPoint_ne_zero hq0 hq hp hζ ht hi' hj' hij' hpp.symm
  · by_cases hij' : i' = 0 ∧ j' = 0
    · exfalso
      rw [hij'.1, hij'.2, tateTorsionPoint_zero_zero] at hpp
      exact tateTorsionPoint_ne_zero hq0 hq hp hζ ht hi hj hij hpp
    · rw [tateTorsionPoint_spec hq0 hq hp hζ ht hi hj hij,
        tateTorsionPoint_spec hq0 hq hp hζ ht hi' hj' hij', Point.some.injEq] at hpp
      obtain ⟨k, hk⟩ := eq_zpow_mul_of_pointXY_eq_unconditional hq0 hq
        (tateParam_ne_zero hζ0 ht0) (tateParam_ne_zero hζ0 ht0)
        (tateParam_offLattice hq0 hq hζ ht hi hj hij)
        (tateParam_offLattice hq0 hq hζ ht hi' hj' hij')
        (tateParam_pow hζ.pow_eq_one ht i j) (tateParam_pow hζ.pow_eq_one ht i' j')
        hp (hp.odd_of_ne_two (by omega)) hpp.1 hpp.2
      exact tateParam_class_eq hq0 hq hζ ht ht0 hi hj hi' hj' hk

variable (q ζ t) in

noncomputable def tateTorsionEquiv (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) :
    (Fin p × Fin p) ≃ ((curve q).n_torsionGen p) := by
  refine Equiv.ofBijective
    (fun ij => ⟨tateTorsionPoint q ζ t hq0 hq hp hζ ht (ij.1 : ℕ) (ij.2 : ℕ),
      tateTorsionPoint_mem hq0 hq hp hp5 hζ ht (ij.1 : ℕ) (ij.2 : ℕ)⟩) ⟨?_, ?_⟩
  · rintro ⟨i, j⟩ ⟨i', j'⟩ hff
    obtain ⟨h1, h2⟩ := tateTorsionPoint_injOn hq0 hq hp hp5 hζ ht i.isLt j.isLt i'.isLt j'.isLt
      (congrArg Subtype.val hff)
    rw [Prod.mk.injEq]
    exact ⟨Fin.ext h1, Fin.ext h2⟩
  · rintro ⟨R, hR⟩
    have hRkill : p • R = 0 := by
      have h := (Submodule.mem_torsionBy_iff _ _).mp hR
      rwa [natCast_zsmul] at h
    rcases eq_zero_or_eq_tateParam_unconditional hq0 hq hp hp5 hζ ht R hRkill with
      h0 | ⟨i, j, hi, hj, hij, hns, hRe⟩
    · refine ⟨(⟨0, hp.pos⟩, ⟨0, hp.pos⟩), ?_⟩
      apply Subtype.ext
      show tateTorsionPoint q ζ t hq0 hq hp hζ ht 0 0 = R
      rw [tateTorsionPoint_zero_zero, h0]
    · refine ⟨(⟨i, hi⟩, ⟨j, hj⟩), ?_⟩
      apply Subtype.ext
      show tateTorsionPoint q ζ t hq0 hq hp hζ ht i j = R
      rw [tateTorsionPoint_spec hq0 hq hp hζ ht hi hj hij, hRe]

theorem natCard_n_torsionGen_curve (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) :
    Nat.card ((curve q).n_torsionGen p) = p ^ 2 := by
  rw [← Nat.card_congr (tateTorsionEquiv q ζ t hq0 hq hp hp5 hζ ht),
    Nat.card_eq_fintype_card, Fintype.card_prod, Fintype.card_fin, sq]

end Parametrization

section GroupStructure

theorem tateTorsionPoint_zeta_mul (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u) (hau : OffLattice q (ζ ^ a * u))
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a)))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
        (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂
          + Point.some (pointX q u) (pointY q u) h₃ :=
  muTranslation_unconditional hq0 hq hp5 hp hζ a ha1 hap u hu0 hu hau h₁ h₂ h₃

theorem tateTorsionPoint_fst_eq_nsmul (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (hζns : (curve q).toAffine.Nonsingular (pointX q ζ) (pointY q ζ))
    {i : ℕ} (hi1 : 1 ≤ i) (hip : i < p)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ i)) (pointY q (ζ ^ i))) :
    (Point.some (pointX q (ζ ^ i)) (pointY q (ζ ^ i)) h₁ : (curve q).toAffine.Point)
      = i • Point.some (pointX q ζ) (pointY q ζ) hζns :=
  zeta_pow_point_eq_nsmul (muTranslation_unconditional hq0 hq hp5 hp hζ) hq0 hq hp hζ ht
    hζns i hi1 hip h₁

theorem tateTorsionPoint_inv (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q u⁻¹) (pointY q u⁻¹))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q u⁻¹) (pointY q u⁻¹) h₁ : (curve q).toAffine.Point)
      = -Point.some (pointX q u) (pointY q u) h₂ :=
  point_inv_eq_neg hq0 hq hu0 hu h₁ h₂

end GroupStructure

section GaloisAction

private lemma map_tateParam (σ : K →+* K) {e c : ℕ} (hσζ : σ ζ = ζ ^ e)
    (hσt : σ t = ζ ^ c * t) (i j : ℕ) :
    σ (ζ ^ i * t ^ j) = ζ ^ (e * i + c * j) * t ^ j := by
  rw [map_mul, map_pow, map_pow, hσζ, hσt, mul_pow, ← pow_mul, ← pow_mul, pow_add]
  ring

theorem map_pointX_tateParam (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (σ : K →+* K) (hσ : Isometry ⇑σ) (hσq : σ q = q) {e c : ℕ}
    (hσζ : σ ζ = ζ ^ e) (hσt : σ t = ζ ^ c * t) (i j : ℕ) :
    σ (pointX q (ζ ^ i * t ^ j)) = pointX q (ζ ^ (e * i + c * j) * t ^ j) := by
  rw [map_pointX σ hσ hσq hq0 hq
    (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht)),
    map_tateParam σ hσζ hσt]

theorem map_pointY_tateParam (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (σ : K →+* K) (hσ : Isometry ⇑σ) (hσq : σ q = q) {e c : ℕ}
    (hσζ : σ ζ = ζ ^ e) (hσt : σ t = ζ ^ c * t) (i j : ℕ) :
    σ (pointY q (ζ ^ i * t ^ j)) = pointY q (ζ ^ (e * i + c * j) * t ^ j) := by
  rw [map_pointY σ hσ hσq hq0 hq
    (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht)),
    map_tateParam σ hσζ hσt]

theorem map_pointX_tateParam_toric (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (σ : K →+* K) (hσ : Isometry ⇑σ) (hσq : σ q = q) {e c : ℕ}
    (hσζ : σ ζ = ζ ^ e) (hσt : σ t = ζ ^ c * t) (i : ℕ) :
    σ (pointX q (ζ ^ i * t ^ 0)) = pointX q (ζ ^ (e * i) * t ^ 0) := by
  have h := map_pointX_tateParam hq0 hq hp hζ ht σ hσ hσq hσζ hσt i 0
  simpa using h

end GaloisAction

end TateCurve