Definitions/Def_TateCurve_TateParameter.lean

import Mathlib
import Definitions.Def_TateCurve_QSeries

set_option autoImplicit false

open scoped NNReal
open IsUltrametricDist Filter

namespace TateCurve

section QSeriesExtras

variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K]
variable {q : K} [CompleteSpace K]

theorem nnnorm_Δ_sub_le (hq : ‖q‖₊ < 1) : ‖(curve q).Δ - q‖₊ ≤ ‖q‖₊ ^ 2 := by
  have ha₄ := nnnorm_a₄_le hq
  have ha₆ := nnnorm_a₆_le hq
  have ha₆q := nnnorm_a₆_add_le hq

  have hsplit : (curve q).Δ - q =
      -(a₆ q + q) + a₄ q ^ 2 + -(64 * a₄ q ^ 3) + -(432 * a₆ q ^ 2) + 72 * a₄ q * a₆ q := by
    rw [curve_Δ]; ring
  rw [hsplit]

  have hq_sq : ‖q‖₊ ^ 3 ≤ ‖q‖₊ ^ 2 := pow_le_pow_of_le_one zero_le hq.le (by norm_num)
  have h64 : ‖(64 : K)‖₊ ≤ 1 := by exact_mod_cast nnnorm_natCast_le_one K 64
  have h432 : ‖(432 : K)‖₊ ≤ 1 := by exact_mod_cast nnnorm_natCast_le_one K 432
  have h72 : ‖(72 : K)‖₊ ≤ 1 := by exact_mod_cast nnnorm_natCast_le_one K 72
  refine nnnorm_add_le_of_le (nnnorm_add_le_of_le (nnnorm_add_le_of_le (nnnorm_add_le_of_le
    ?_ ?_) ?_) ?_) ?_
  ·
    rw [nnnorm_neg]; exact ha₆q
  ·
    rw [nnnorm_pow]
    exact pow_le_pow_left' ha₄ 2
  ·
    rw [nnnorm_neg, nnnorm_mul, nnnorm_pow]
    calc ‖(64 : K)‖₊ * ‖a₄ q‖₊ ^ 3 ≤ 1 * ‖q‖₊ ^ 3 :=
          mul_le_mul' h64 (pow_le_pow_left' ha₄ 3)
      _ = ‖q‖₊ ^ 3 := one_mul _
      _ ≤ ‖q‖₊ ^ 2 := hq_sq
  ·
    rw [nnnorm_neg, nnnorm_mul, nnnorm_pow]
    calc ‖(432 : K)‖₊ * ‖a₆ q‖₊ ^ 2 ≤ 1 * ‖q‖₊ ^ 2 :=
          mul_le_mul' h432 (pow_le_pow_left' ha₆ 2)
      _ = ‖q‖₊ ^ 2 := one_mul _
  ·
    rw [nnnorm_mul, nnnorm_mul]
    calc ‖(72 : K)‖₊ * ‖a₄ q‖₊ * ‖a₆ q‖₊ ≤ 1 * ‖q‖₊ * ‖q‖₊ :=
          mul_le_mul' (mul_le_mul' h72 ha₄) ha₆
      _ = ‖q‖₊ ^ 2 := by ring

theorem nnnorm_Δ (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) : ‖(curve q).Δ‖₊ = ‖q‖₊ := by
  refine nnnorm_eq_of_nnnorm_sub_lt ((nnnorm_Δ_sub_le hq).trans_lt ?_)
  have hq0' : 0 < ‖q‖₊ := by simpa [pos_iff_ne_zero] using hq0
  calc ‖q‖₊ ^ 2 = ‖q‖₊ * ‖q‖₊ := pow_two ‖q‖₊
    _ < 1 * ‖q‖₊ := mul_lt_mul_of_pos_right hq hq0'
    _ = ‖q‖₊ := one_mul _

theorem Δ_ne_zero (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) : (curve q).Δ ≠ 0 := by
  intro h
  apply hq0
  have := nnnorm_Δ hq0 hq
  rw [h, nnnorm_zero] at this
  rw [← nnnorm_eq_zero, ← this]

theorem isElliptic (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) : (curve q).IsElliptic :=
  ⟨isUnit_iff_ne_zero.mpr (Δ_ne_zero hq0 hq)⟩

theorem nnnorm_c₄ (hq : ‖q‖₊ < 1) : ‖(curve q).c₄‖₊ = 1 := by
  have h : ‖(curve q).c₄ - 1‖₊ < 1 := by
    rw [curve_c₄]
    have : (1 : K) - 48 * a₄ q - 1 = -(48 * a₄ q) := by ring
    rw [this, nnnorm_neg, nnnorm_mul]
    calc ‖(48 : K)‖₊ * ‖a₄ q‖₊ ≤ 1 * ‖q‖₊ := by
          gcongr
          · exact_mod_cast nnnorm_natCast_le_one K 48
          · exact nnnorm_a₄_le hq
      _ = ‖q‖₊ := one_mul _
      _ < 1 := hq
  have := nnnorm_eq_of_nnnorm_sub_lt (a := (curve q).c₄) (b := (1 : K))
    (by rw [nnnorm_one]; exact h)
  rwa [nnnorm_one] at this

theorem nnnorm_j (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) :
    haveI := isElliptic hq0 hq
    ‖(curve q).j‖₊ = ‖q‖₊⁻¹ := by
  letI := isElliptic hq0 hq
  rw [WeierstrassCurve.j, nnnorm_mul, nnnorm_pow, nnnorm_c₄ hq, one_pow, mul_one]
  rw [Units.val_inv_eq_inv_val, nnnorm_inv, WeierstrassCurve.coe_Δ', nnnorm_Δ hq0 hq]

theorem one_lt_nnnorm_j (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) :
    haveI := isElliptic hq0 hq
    1 < ‖(curve q).j‖₊ := by
  rw [nnnorm_j hq0 hq]
  have hq0' : 0 < ‖q‖₊ := by simpa [pos_iff_ne_zero] using hq0
  exact (one_lt_inv₀ hq0').mpr hq

end QSeriesExtras

end TateCurve

open scoped NNReal

open IsUltrametricDist Filter

namespace TateCurve

variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K]

section PowSub

theorem nnnorm_pow_succ_sub_pow_succ_le (x y : K) (n : ℕ) :
    ‖x ^ (n + 1) - y ^ (n + 1)‖₊ ≤ (max ‖x‖₊ ‖y‖₊) ^ n * ‖x - y‖₊ := by
  induction n with
  | zero => simp
  | succ k ih =>
      have hsplit : x ^ (k + 2) - y ^ (k + 2)
          = x * (x ^ (k + 1) - y ^ (k + 1)) + (x - y) * y ^ (k + 1) := by ring
      have h₁ : ‖x * (x ^ (k + 1) - y ^ (k + 1))‖₊
          ≤ (max ‖x‖₊ ‖y‖₊) ^ (k + 1) * ‖x - y‖₊ := by
        rw [nnnorm_mul]
        calc ‖x‖₊ * ‖x ^ (k + 1) - y ^ (k + 1)‖₊
            ≤ max ‖x‖₊ ‖y‖₊ * ((max ‖x‖₊ ‖y‖₊) ^ k * ‖x - y‖₊) :=
              mul_le_mul' (le_max_left _ _) ih
          _ = (max ‖x‖₊ ‖y‖₊) ^ (k + 1) * ‖x - y‖₊ := by ring
      have h₂ : ‖(x - y) * y ^ (k + 1)‖₊
          ≤ (max ‖x‖₊ ‖y‖₊) ^ (k + 1) * ‖x - y‖₊ := by
        rw [nnnorm_mul, nnnorm_pow]
        calc ‖x - y‖₊ * ‖y‖₊ ^ (k + 1)
            ≤ ‖x - y‖₊ * (max ‖x‖₊ ‖y‖₊) ^ (k + 1) :=
              mul_le_mul' le_rfl (pow_le_pow_left' (le_max_right _ _) _)
          _ = (max ‖x‖₊ ‖y‖₊) ^ (k + 1) * ‖x - y‖₊ := mul_comm _ _
      calc ‖x ^ (k + 1 + 1) - y ^ (k + 1 + 1)‖₊
          = ‖x * (x ^ (k + 1) - y ^ (k + 1)) + (x - y) * y ^ (k + 1)‖₊ := by rw [← hsplit]
        _ ≤ (max ‖x‖₊ ‖y‖₊) ^ (k + 1) * ‖x - y‖₊ := nnnorm_add_le_of_le h₁ h₂

end PowSub

section CoeffSumDiff

variable (c : ℕ → ℕ) {q₁ q₂ : K}

theorem term_sub_term (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) {n : ℕ} (hn : n ≠ 0) :
    term c q₁ n - term c q₂ n
      = (c n : K) * ((q₁ ^ n - q₂ ^ n) / ((1 - q₁ ^ n) * (1 - q₂ ^ n))) := by
  have hq₁n : ‖q₁ ^ n‖₊ < 1 := by
    rw [nnnorm_pow]; exact pow_lt_one₀ zero_le hq₁ hn
  have hq₂n : ‖q₂ ^ n‖₊ < 1 := by
    rw [nnnorm_pow]; exact pow_lt_one₀ zero_le hq₂ hn
  have h₁ : (1 : K) - q₁ ^ n ≠ 0 := one_sub_ne_zero_of_lt_one hq₁n
  have h₂ : (1 : K) - q₂ ^ n ≠ 0 := one_sub_ne_zero_of_lt_one hq₂n
  simp only [term]
  field_simp
  ring

theorem nnnorm_term_sub_term_succ_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) (m : ℕ) :
    ‖term c q₁ (m + 1) - term c q₂ (m + 1)‖₊
      ≤ (max ‖q₁‖₊ ‖q₂‖₊) ^ m * ‖q₁ - q₂‖₊ := by
  have hq₁n : ‖q₁ ^ (m + 1)‖₊ < 1 := by
    rw [nnnorm_pow]; exact pow_lt_one₀ zero_le hq₁ (Nat.succ_ne_zero m)
  have hq₂n : ‖q₂ ^ (m + 1)‖₊ < 1 := by
    rw [nnnorm_pow]; exact pow_lt_one₀ zero_le hq₂ (Nat.succ_ne_zero m)
  have hden : ‖(1 - q₁ ^ (m + 1)) * (1 - q₂ ^ (m + 1))‖₊ = 1 := by
    rw [nnnorm_mul, nnnorm_one_sub_of_lt_one hq₁n, nnnorm_one_sub_of_lt_one hq₂n, one_mul]
  rw [term_sub_term c hq₁ hq₂ (Nat.succ_ne_zero m)]
  rw [nnnorm_mul, nnnorm_div, hden, div_one]
  calc ‖(c (m + 1) : K)‖₊ * ‖q₁ ^ (m + 1) - q₂ ^ (m + 1)‖₊
      ≤ 1 * ((max ‖q₁‖₊ ‖q₂‖₊) ^ m * ‖q₁ - q₂‖₊) :=
        mul_le_mul' (nnnorm_natCast_le_one K (c (m + 1)))
          (nnnorm_pow_succ_sub_pow_succ_le q₁ q₂ m)
    _ = (max ‖q₁‖₊ ‖q₂‖₊) ^ m * ‖q₁ - q₂‖₊ := one_mul _

theorem nnnorm_term_sub_term_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) (n : ℕ) :
    ‖term c q₁ n - term c q₂ n‖₊ ≤ ‖q₁ - q₂‖₊ := by
  rcases Nat.eq_zero_or_pos n with rfl | hn
  · simp
  obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
  have hmax1 : (max ‖q₁‖₊ ‖q₂‖₊) ^ m ≤ 1 :=
    pow_le_one₀ zero_le (max_le hq₁.le hq₂.le)
  calc ‖term c q₁ (m + 1) - term c q₂ (m + 1)‖₊
      ≤ (max ‖q₁‖₊ ‖q₂‖₊) ^ m * ‖q₁ - q₂‖₊ := nnnorm_term_sub_term_succ_le c hq₁ hq₂ m
    _ ≤ 1 * ‖q₁ - q₂‖₊ := mul_le_mul' hmax1 le_rfl
    _ = ‖q₁ - q₂‖₊ := one_mul _

theorem nnnorm_term_sub_term_le_mul (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) {n : ℕ} (hn : 2 ≤ n) :
    ‖term c q₁ n - term c q₂ n‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
  obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
  have hm : 1 ≤ m := by omega
  have hmax : (max ‖q₁‖₊ ‖q₂‖₊) ^ m ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
    calc (max ‖q₁‖₊ ‖q₂‖₊) ^ m ≤ (max ‖q₁‖₊ ‖q₂‖₊) ^ 1 :=
          pow_le_pow_of_le_one zero_le (max_le hq₁.le hq₂.le) hm
      _ = max ‖q₁‖₊ ‖q₂‖₊ := pow_one _
  calc ‖term c q₁ (m + 1) - term c q₂ (m + 1)‖₊
      ≤ (max ‖q₁‖₊ ‖q₂‖₊) ^ m * ‖q₁ - q₂‖₊ := nnnorm_term_sub_term_succ_le c hq₁ hq₂ m
    _ ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := mul_le_mul' hmax le_rfl

variable [CompleteSpace K]

theorem summable_term_ite (hq : ‖q₁‖₊ < 1) :
    Summable fun n => if n = 1 then (0 : K) else term c q₁ n := by
  refine NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_
  rw [Nat.cofinite_eq_atTop]
  refine squeeze_zero_norm (fun n => ?_)
    (tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg q₁) ?_)
  · rcases eq_or_ne n 1 with rfl | hn
    · have hif : (if (1 : ℕ) = 1 then (0 : K) else term c q₁ 1) = 0 := if_pos rfl
      rw [hif, norm_zero]
      positivity
    · rw [if_neg hn]
      exact_mod_cast nnnorm_term_le c hq n
  · exact_mod_cast hq

theorem nnnorm_coeffSum_sub_coeffSum_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖coeffSum c q₁ - coeffSum c q₂‖₊ ≤ ‖q₁ - q₂‖₊ := by
  have hsum : coeffSum c q₁ - coeffSum c q₂ = ∑' n, (term c q₁ n - term c q₂ n) :=
    (((summable_term c hq₁).hasSum.sub (summable_term c hq₂).hasSum).tsum_eq).symm
  rw [hsum]
  exact nnnorm_tsum_le_of_forall_le fun n => nnnorm_term_sub_term_le c hq₁ hq₂ n

theorem nnnorm_coeffSum_sub_coeffSum_sub_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖coeffSum c q₁ - coeffSum c q₂ - (c 1 : K) * (q₁ - q₂)‖₊
      ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
  have hq₁M : ‖q₁‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := le_max_left _ _
  have hq₂M : ‖q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := le_max_right _ _
  have h1q₁ : (1 : K) - q₁ ≠ 0 := one_sub_ne_zero_of_lt_one hq₁
  have h1q₂ : (1 : K) - q₂ ≠ 0 := one_sub_ne_zero_of_lt_one hq₂

  have hsplit₁ : coeffSum c q₁ = term c q₁ 1 + ∑' n, if n = 1 then (0 : K) else term c q₁ n :=
    (summable_term c hq₁).tsum_eq_add_tsum_ite 1
  have hsplit₂ : coeffSum c q₂ = term c q₂ 1 + ∑' n, if n = 1 then (0 : K) else term c q₂ n :=
    (summable_term c hq₂).tsum_eq_add_tsum_ite 1

  have htail : (∑' n, if n = 1 then (0 : K) else term c q₁ n)
        - (∑' n, if n = 1 then (0 : K) else term c q₂ n)
      = ∑' n, ((if n = 1 then (0 : K) else term c q₁ n)
        - (if n = 1 then (0 : K) else term c q₂ n)) :=
    (((summable_term_ite c hq₁).hasSum.sub (summable_term_ite c hq₂).hasSum).tsum_eq).symm
  have htail_le : ‖(∑' n, if n = 1 then (0 : K) else term c q₁ n)
        - (∑' n, if n = 1 then (0 : K) else term c q₂ n)‖₊
      ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
    rw [htail]
    refine nnnorm_tsum_le_of_forall_le fun n => ?_
    rcases eq_or_ne n 1 with rfl | hn
    · simp
    rw [if_neg hn, if_neg hn]
    rcases Nat.eq_zero_or_pos n with rfl | hn0
    · simp
    have h2n : 2 ≤ n := by omega
    exact nnnorm_term_sub_term_le_mul c hq₁ hq₂ h2n

  have hfac : ‖q₁ + q₂ - q₁ * q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
    have h1 : ‖q₁ + q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := nnnorm_add_le_of_le hq₁M hq₂M
    have h2 : ‖q₁ * q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
      rw [nnnorm_mul]
      calc ‖q₁‖₊ * ‖q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ * 1 := mul_le_mul' hq₁M hq₂.le
        _ = max ‖q₁‖₊ ‖q₂‖₊ := mul_one _
    calc ‖q₁ + q₂ - q₁ * q₂‖₊ = ‖(q₁ + q₂) + -(q₁ * q₂)‖₊ := by rw [sub_eq_add_neg]
      _ ≤ max ‖q₁‖₊ ‖q₂‖₊ := nnnorm_add_le_of_le h1 (by rw [nnnorm_neg]; exact h2)
  have hlead : ‖(term c q₁ 1 - (c 1 : K) * q₁) - (term c q₂ 1 - (c 1 : K) * q₂)‖₊
      ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
    have hkey : (term c q₁ 1 - (c 1 : K) * q₁) - (term c q₂ 1 - (c 1 : K) * q₂)
        = (c 1 : K) * ((q₁ - q₂) * (q₁ + q₂ - q₁ * q₂) / ((1 - q₁) * (1 - q₂))) := by
      rw [term_one, term_one]
      field_simp
      ring
    have hden : ‖(1 - q₁) * (1 - q₂)‖₊ = 1 := by
      rw [nnnorm_mul, nnnorm_one_sub_of_lt_one hq₁, nnnorm_one_sub_of_lt_one hq₂, one_mul]
    have hnum : ‖(q₁ - q₂) * (q₁ + q₂ - q₁ * q₂)‖₊ ≤ ‖q₁ - q₂‖₊ * max ‖q₁‖₊ ‖q₂‖₊ := by
      rw [nnnorm_mul]
      exact mul_le_mul' le_rfl hfac
    calc ‖(term c q₁ 1 - (c 1 : K) * q₁) - (term c q₂ 1 - (c 1 : K) * q₂)‖₊
        = ‖(c 1 : K)‖₊ * (‖(q₁ - q₂) * (q₁ + q₂ - q₁ * q₂)‖₊ / ‖(1 - q₁) * (1 - q₂)‖₊) := by
          rw [hkey, nnnorm_mul, nnnorm_div]
      _ = ‖(c 1 : K)‖₊ * ‖(q₁ - q₂) * (q₁ + q₂ - q₁ * q₂)‖₊ := by rw [hden, div_one]
      _ ≤ 1 * (‖q₁ - q₂‖₊ * max ‖q₁‖₊ ‖q₂‖₊) :=
          mul_le_mul' (nnnorm_natCast_le_one K (c 1)) hnum
      _ = max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by ring

  have hassemble : coeffSum c q₁ - coeffSum c q₂ - (c 1 : K) * (q₁ - q₂)
      = ((term c q₁ 1 - (c 1 : K) * q₁) - (term c q₂ 1 - (c 1 : K) * q₂))
        + ((∑' n, if n = 1 then (0 : K) else term c q₁ n)
          - (∑' n, if n = 1 then (0 : K) else term c q₂ n)) := by
    rw [hsplit₁, hsplit₂]; ring
  rw [hassemble]
  exact nnnorm_add_le_of_le hlead htail_le

end CoeffSumDiff

section CoefficientsDiff

variable [CompleteSpace K] {q₁ q₂ : K}

theorem nnnorm_a₄_sub_a₄_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖a₄ q₁ - a₄ q₂‖₊ ≤ ‖q₁ - q₂‖₊ := by
  have h : a₄ q₁ - a₄ q₂
      = -(coeffSum (fun n => 5 * n ^ 3) q₁ - coeffSum (fun n => 5 * n ^ 3) q₂) := by
    rw [a₄, a₄]; ring
  rw [h, nnnorm_neg]
  exact nnnorm_coeffSum_sub_coeffSum_le _ hq₁ hq₂

theorem nnnorm_a₆_sub_a₆_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖a₆ q₁ - a₆ q₂‖₊ ≤ ‖q₁ - q₂‖₊ := by
  have h : a₆ q₁ - a₆ q₂ = -(coeffSum b q₁ - coeffSum b q₂) := by
    rw [a₆, a₆]; ring
  rw [h, nnnorm_neg]
  exact nnnorm_coeffSum_sub_coeffSum_le _ hq₁ hq₂

theorem nnnorm_a₆_sub_a₆_add_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖a₆ q₁ - a₆ q₂ + (q₁ - q₂)‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
  have h := nnnorm_coeffSum_sub_coeffSum_sub_le (K := K) b hq₁ hq₂
  rw [b_one, Nat.cast_one, one_mul] at h
  have hkey : a₆ q₁ - a₆ q₂ + (q₁ - q₂)
      = -(coeffSum b q₁ - coeffSum b q₂ - (q₁ - q₂)) := by
    rw [a₆, a₆]; ring
  rw [hkey, nnnorm_neg]
  exact h

theorem nnnorm_c₄_sub_c₄_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖(curve q₁).c₄ - (curve q₂).c₄‖₊ ≤ ‖q₁ - q₂‖₊ := by
  have hkey : (curve q₁).c₄ - (curve q₂).c₄ = -(48 * (a₄ q₁ - a₄ q₂)) := by
    rw [curve_c₄, curve_c₄]; ring
  rw [hkey, nnnorm_neg, nnnorm_mul]
  calc ‖(48 : K)‖₊ * ‖a₄ q₁ - a₄ q₂‖₊ ≤ 1 * ‖q₁ - q₂‖₊ := by
        gcongr
        · exact_mod_cast nnnorm_natCast_le_one K 48
        · exact nnnorm_a₄_sub_a₄_le hq₁ hq₂
    _ = ‖q₁ - q₂‖₊ := one_mul _

theorem nnnorm_Δ_sub_Δ_sub_le (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖(curve q₁).Δ - (curve q₂).Δ - (q₁ - q₂)‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
  have hM1 : max ‖q₁‖₊ ‖q₂‖₊ < 1 := max_lt hq₁ hq₂
  have ha₄₁ : ‖a₄ q₁‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := (nnnorm_a₄_le hq₁).trans (le_max_left _ _)
  have ha₄₂ : ‖a₄ q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := (nnnorm_a₄_le hq₂).trans (le_max_right _ _)
  have ha₆₁ : ‖a₆ q₁‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := (nnnorm_a₆_le hq₁).trans (le_max_left _ _)
  have ha₆₂ : ‖a₆ q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := (nnnorm_a₆_le hq₂).trans (le_max_right _ _)
  have hd₄ : ‖a₄ q₁ - a₄ q₂‖₊ ≤ ‖q₁ - q₂‖₊ := nnnorm_a₄_sub_a₄_le hq₁ hq₂
  have hd₆ : ‖a₆ q₁ - a₆ q₂‖₊ ≤ ‖q₁ - q₂‖₊ := nnnorm_a₆_sub_a₆_le hq₁ hq₂
  have hd₆' : ‖a₆ q₁ - a₆ q₂ + (q₁ - q₂)‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ :=
    nnnorm_a₆_sub_a₆_add_le hq₁ hq₂
  have hMM : max ‖q₁‖₊ ‖q₂‖₊ * max ‖q₁‖₊ ‖q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
    calc max ‖q₁‖₊ ‖q₂‖₊ * max ‖q₁‖₊ ‖q₂‖₊ ≤ 1 * max ‖q₁‖₊ ‖q₂‖₊ :=
          mul_le_mul' hM1.le le_rfl
      _ = max ‖q₁‖₊ ‖q₂‖₊ := one_mul _

  have hsplit : (curve q₁).Δ - (curve q₂).Δ - (q₁ - q₂)
      = -(a₆ q₁ - a₆ q₂ + (q₁ - q₂))
        + (a₄ q₁ - a₄ q₂) * (a₄ q₁ + a₄ q₂)
        + -(64 * ((a₄ q₁ - a₄ q₂) * (a₄ q₁ ^ 2 + a₄ q₁ * a₄ q₂ + a₄ q₂ ^ 2)))
        + -(432 * ((a₆ q₁ - a₆ q₂) * (a₆ q₁ + a₆ q₂)))
        + 72 * (a₄ q₁ * (a₆ q₁ - a₆ q₂) + a₆ q₂ * (a₄ q₁ - a₄ q₂)) := by
    rw [curve_Δ, curve_Δ]; ring
  rw [hsplit]
  have h64 : ‖(64 : K)‖₊ ≤ 1 := by exact_mod_cast nnnorm_natCast_le_one K 64
  have h432 : ‖(432 : K)‖₊ ≤ 1 := by exact_mod_cast nnnorm_natCast_le_one K 432
  have h72 : ‖(72 : K)‖₊ ≤ 1 := by exact_mod_cast nnnorm_natCast_le_one K 72
  refine nnnorm_add_le_of_le (nnnorm_add_le_of_le (nnnorm_add_le_of_le (nnnorm_add_le_of_le
    ?_ ?_) ?_) ?_) ?_
  ·
    rw [nnnorm_neg]; exact hd₆'
  ·
    rw [nnnorm_mul]
    calc ‖a₄ q₁ - a₄ q₂‖₊ * ‖a₄ q₁ + a₄ q₂‖₊
        ≤ ‖q₁ - q₂‖₊ * max ‖q₁‖₊ ‖q₂‖₊ :=
          mul_le_mul' hd₄ (nnnorm_add_le_of_le ha₄₁ ha₄₂)
      _ = max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := mul_comm _ _
  ·
    rw [nnnorm_neg, nnnorm_mul, nnnorm_mul]
    have hquad : ‖a₄ q₁ ^ 2 + a₄ q₁ * a₄ q₂ + a₄ q₂ ^ 2‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
      have h1 : ‖a₄ q₁ ^ 2‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
        rw [nnnorm_pow, sq]
        exact (mul_le_mul' ha₄₁ ha₄₁).trans hMM
      have h2 : ‖a₄ q₁ * a₄ q₂‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
        rw [nnnorm_mul]
        exact (mul_le_mul' ha₄₁ ha₄₂).trans hMM
      have h3 : ‖a₄ q₂ ^ 2‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ := by
        rw [nnnorm_pow, sq]
        exact (mul_le_mul' ha₄₂ ha₄₂).trans hMM
      exact nnnorm_add_le_of_le (nnnorm_add_le_of_le h1 h2) h3
    calc ‖(64 : K)‖₊ * (‖a₄ q₁ - a₄ q₂‖₊ * ‖a₄ q₁ ^ 2 + a₄ q₁ * a₄ q₂ + a₄ q₂ ^ 2‖₊)
        ≤ 1 * (‖q₁ - q₂‖₊ * max ‖q₁‖₊ ‖q₂‖₊) :=
          mul_le_mul' h64 (mul_le_mul' hd₄ hquad)
      _ = max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by ring
  ·
    rw [nnnorm_neg, nnnorm_mul, nnnorm_mul]
    calc ‖(432 : K)‖₊ * (‖a₆ q₁ - a₆ q₂‖₊ * ‖a₆ q₁ + a₆ q₂‖₊)
        ≤ 1 * (‖q₁ - q₂‖₊ * max ‖q₁‖₊ ‖q₂‖₊) :=
          mul_le_mul' h432 (mul_le_mul' hd₆ (nnnorm_add_le_of_le ha₆₁ ha₆₂))
      _ = max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by ring
  ·
    rw [nnnorm_mul]
    have hinner : ‖a₄ q₁ * (a₆ q₁ - a₆ q₂) + a₆ q₂ * (a₄ q₁ - a₄ q₂)‖₊
        ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
      have h1 : ‖a₄ q₁ * (a₆ q₁ - a₆ q₂)‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
        rw [nnnorm_mul]; exact mul_le_mul' ha₄₁ hd₆
      have h2 : ‖a₆ q₂ * (a₄ q₁ - a₄ q₂)‖₊ ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := by
        rw [nnnorm_mul]; exact mul_le_mul' ha₆₂ hd₄
      exact nnnorm_add_le_of_le h1 h2
    calc ‖(72 : K)‖₊ * ‖a₄ q₁ * (a₆ q₁ - a₆ q₂) + a₆ q₂ * (a₄ q₁ - a₄ q₂)‖₊
        ≤ 1 * (max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊) := mul_le_mul' h72 hinner
      _ = max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := one_mul _

end CoefficientsDiff

section TateParameter

variable [CompleteSpace K]

noncomputable def jInversionStep (j₀ q : K) : K :=
  (curve q).c₄ ^ 3 / j₀ - ((curve q).Δ - q)

theorem jInversionStep_eq_self_iff {j₀ q : K} (hj₀ : j₀ ≠ 0) :
    jInversionStep j₀ q = q ↔ (curve q).c₄ ^ 3 = j₀ * (curve q).Δ := by
  rw [jInversionStep]
  constructor
  · intro h
    have h2 : (curve q).c₄ ^ 3 / j₀ = (curve q).Δ := by linear_combination h
    rw [div_eq_iff hj₀] at h2
    linear_combination h2
  · intro h
    have h2 : (curve q).c₄ ^ 3 / j₀ = (curve q).Δ := by
      rw [div_eq_iff hj₀]; linear_combination h
    linear_combination h2

theorem nnnorm_jInversionStep {j₀ q : K} (hj : 1 < ‖j₀‖₊) (hq : ‖q‖₊ ≤ ‖j₀‖₊⁻¹) :
    ‖jInversionStep j₀ q‖₊ = ‖j₀‖₊⁻¹ := by
  have hpos : (0 : ℝ≥0) < ‖j₀‖₊ := lt_trans zero_lt_one hj
  have hρpos : (0 : ℝ≥0) < ‖j₀‖₊⁻¹ := by
    rw [inv_pos]; exact hpos
  have hρlt : ‖j₀‖₊⁻¹ < 1 := by
    have h := mul_lt_mul_of_pos_left hj (inv_pos.mpr hpos)
    rwa [mul_one, inv_mul_cancel₀ hpos.ne'] at h
  have hq1 : ‖q‖₊ < 1 := lt_of_le_of_lt hq hρlt

  have hmain : ‖(curve q).c₄ ^ 3 / j₀‖₊ = ‖j₀‖₊⁻¹ := by
    rw [nnnorm_div, nnnorm_pow, nnnorm_c₄ hq1, one_pow, one_div]

  have hcorr : ‖(curve q).Δ - q‖₊ < ‖j₀‖₊⁻¹ := by
    calc ‖(curve q).Δ - q‖₊ ≤ ‖q‖₊ ^ 2 := nnnorm_Δ_sub_le hq1
      _ ≤ ‖j₀‖₊⁻¹ ^ 2 := pow_le_pow_left' hq 2
      _ < ‖j₀‖₊⁻¹ := by
          calc ‖j₀‖₊⁻¹ ^ 2 = ‖j₀‖₊⁻¹ * ‖j₀‖₊⁻¹ := sq _
            _ < 1 * ‖j₀‖₊⁻¹ := mul_lt_mul_of_pos_right hρlt hρpos
            _ = ‖j₀‖₊⁻¹ := one_mul _

  rw [jInversionStep]
  rw [show (curve q).c₄ ^ 3 / j₀ - ((curve q).Δ - q)
      = (curve q).c₄ ^ 3 / j₀ - ((curve q).Δ - q) from rfl]
  refine nnnorm_eq_of_nnnorm_sub_lt ?_ |>.trans hmain
  rw [sub_sub_cancel_left, nnnorm_neg, hmain]
  exact hcorr

theorem nnnorm_jInversionStep_sub_le {j₀ q₁ q₂ : K} (hj : 1 < ‖j₀‖₊)
    (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1) :
    ‖jInversionStep j₀ q₁ - jInversionStep j₀ q₂‖₊
      ≤ max (max ‖q₁‖₊ ‖q₂‖₊) ‖j₀‖₊⁻¹ * ‖q₁ - q₂‖₊ := by
  have hpos : (0 : ℝ≥0) < ‖j₀‖₊ := lt_trans zero_lt_one hj
  have hc₄₁ : ‖(curve q₁).c₄‖₊ = 1 := nnnorm_c₄ hq₁
  have hc₄₂ : ‖(curve q₂).c₄‖₊ = 1 := nnnorm_c₄ hq₂

  have hsplit : jInversionStep j₀ q₁ - jInversionStep j₀ q₂
      = ((curve q₁).c₄ ^ 3 - (curve q₂).c₄ ^ 3) / j₀
        + -((curve q₁).Δ - (curve q₂).Δ - (q₁ - q₂)) := by
    rw [jInversionStep, jInversionStep]; ring
  rw [hsplit]
  refine nnnorm_add_le_of_le ?_ ?_
  ·

    have hcube : ‖(curve q₁).c₄ ^ 3 - (curve q₂).c₄ ^ 3‖₊ ≤ ‖q₁ - q₂‖₊ := by
      have hfactor : (curve q₁).c₄ ^ 3 - (curve q₂).c₄ ^ 3
          = ((curve q₁).c₄ - (curve q₂).c₄)
            * ((curve q₁).c₄ ^ 2 + (curve q₁).c₄ * (curve q₂).c₄ + (curve q₂).c₄ ^ 2) := by
        ring
      have hquad : ‖(curve q₁).c₄ ^ 2 + (curve q₁).c₄ * (curve q₂).c₄ + (curve q₂).c₄ ^ 2‖₊
          ≤ 1 := by
        have h1 : ‖(curve q₁).c₄ ^ 2‖₊ ≤ 1 := by rw [nnnorm_pow, hc₄₁, one_pow]
        have h2 : ‖(curve q₁).c₄ * (curve q₂).c₄‖₊ ≤ 1 := by
          rw [nnnorm_mul, hc₄₁, hc₄₂, one_mul]
        have h3 : ‖(curve q₂).c₄ ^ 2‖₊ ≤ 1 := by rw [nnnorm_pow, hc₄₂, one_pow]
        exact nnnorm_add_le_of_le (nnnorm_add_le_of_le h1 h2) h3
      calc ‖(curve q₁).c₄ ^ 3 - (curve q₂).c₄ ^ 3‖₊
          = ‖(curve q₁).c₄ - (curve q₂).c₄‖₊
            * ‖(curve q₁).c₄ ^ 2 + (curve q₁).c₄ * (curve q₂).c₄ + (curve q₂).c₄ ^ 2‖₊ := by
            rw [hfactor, nnnorm_mul]
        _ ≤ ‖q₁ - q₂‖₊ * 1 := mul_le_mul' (nnnorm_c₄_sub_c₄_le hq₁ hq₂) hquad
        _ = ‖q₁ - q₂‖₊ := mul_one _
    calc ‖((curve q₁).c₄ ^ 3 - (curve q₂).c₄ ^ 3) / j₀‖₊
        = ‖(curve q₁).c₄ ^ 3 - (curve q₂).c₄ ^ 3‖₊ * ‖j₀‖₊⁻¹ := by
          rw [nnnorm_div, div_eq_mul_inv]
      _ ≤ ‖q₁ - q₂‖₊ * ‖j₀‖₊⁻¹ := mul_le_mul' hcube le_rfl
      _ ≤ ‖q₁ - q₂‖₊ * max (max ‖q₁‖₊ ‖q₂‖₊) ‖j₀‖₊⁻¹ :=
          mul_le_mul' le_rfl (le_max_right _ _)
      _ = max (max ‖q₁‖₊ ‖q₂‖₊) ‖j₀‖₊⁻¹ * ‖q₁ - q₂‖₊ := mul_comm _ _
  ·
    rw [nnnorm_neg]
    calc ‖(curve q₁).Δ - (curve q₂).Δ - (q₁ - q₂)‖₊
        ≤ max ‖q₁‖₊ ‖q₂‖₊ * ‖q₁ - q₂‖₊ := nnnorm_Δ_sub_Δ_sub_le hq₁ hq₂
      _ ≤ max (max ‖q₁‖₊ ‖q₂‖₊) ‖j₀‖₊⁻¹ * ‖q₁ - q₂‖₊ :=
          mul_le_mul' (le_max_left _ _) le_rfl

theorem exists_tateParameter_c₄ (j₀ : K) (hj : 1 < ‖j₀‖₊) :
    ∃ q : K, q ≠ 0 ∧ ‖q‖₊ = ‖j₀‖₊⁻¹ ∧ (curve q).c₄ ^ 3 = j₀ * (curve q).Δ := by
  have hpos : (0 : ℝ≥0) < ‖j₀‖₊ := lt_trans zero_lt_one hj
  have hj₀0 : j₀ ≠ 0 := by
    intro h
    rw [h, nnnorm_zero] at hj
    exact (lt_irrefl _ (lt_trans zero_lt_one hj)).elim
  have hρpos : (0 : ℝ≥0) < ‖j₀‖₊⁻¹ := by rw [inv_pos]; exact hpos
  have hρlt : ‖j₀‖₊⁻¹ < 1 := by
    have h := mul_lt_mul_of_pos_left hj (inv_pos.mpr hpos)
    rwa [mul_one, inv_mul_cancel₀ hpos.ne'] at h

  set B : Set K := Metric.closedBall (0 : K) ((‖j₀‖₊⁻¹ : ℝ≥0) : ℝ) with hBdef
  have hmem : ∀ x : K, x ∈ B ↔ ‖x‖₊ ≤ ‖j₀‖₊⁻¹ := by
    intro x
    rw [hBdef, Metric.mem_closedBall, dist_zero_right, ← coe_nnnorm, NNReal.coe_le_coe]
  haveI : CompleteSpace B := Metric.isClosed_closedBall.completeSpace_coe
  have h0B : (0 : K) ∈ B := by
    rw [hBdef]
    exact Metric.mem_closedBall_self (NNReal.coe_nonneg _)
  haveI : Nonempty B := ⟨⟨0, h0B⟩⟩

  have hmaps : ∀ x : K, ‖x‖₊ ≤ ‖j₀‖₊⁻¹ → ‖jInversionStep j₀ x‖₊ ≤ ‖j₀‖₊⁻¹ := fun x hx =>
    le_of_eq (nnnorm_jInversionStep hj hx)
  let φ : B → B := fun z => ⟨jInversionStep j₀ (z : K), (hmem _).mpr (hmaps _ ((hmem _).mp z.2))⟩

  have hlip : LipschitzWith ‖j₀‖₊⁻¹ φ := by
    refine LipschitzWith.of_dist_le_mul fun x y => ?_
    have hx : ‖(x : K)‖₊ ≤ ‖j₀‖₊⁻¹ := (hmem _).mp x.2
    have hy : ‖(y : K)‖₊ ≤ ‖j₀‖₊⁻¹ := (hmem _).mp y.2
    have hx1 : ‖(x : K)‖₊ < 1 := lt_of_le_of_lt hx hρlt
    have hy1 : ‖(y : K)‖₊ < 1 := lt_of_le_of_lt hy hρlt
    have key : ‖jInversionStep j₀ (x : K) - jInversionStep j₀ (y : K)‖₊
        ≤ ‖j₀‖₊⁻¹ * ‖(x : K) - (y : K)‖₊ := by
      refine (nnnorm_jInversionStep_sub_le hj hx1 hy1).trans ?_
      refine mul_le_mul' ?_ le_rfl
      exact max_le (max_le hx hy) le_rfl
    calc dist (φ x) (φ y)
        = ‖jInversionStep j₀ (x : K) - jInversionStep j₀ (y : K)‖ := by
          rw [show dist (φ x) (φ y)
              = dist (jInversionStep j₀ (x : K)) (jInversionStep j₀ (y : K)) from rfl,
            dist_eq_norm]
      _ ≤ ((‖j₀‖₊⁻¹ * ‖(x : K) - (y : K)‖₊ : ℝ≥0) : ℝ) := by
          rw [← coe_nnnorm]
          exact_mod_cast key
      _ = (‖j₀‖₊⁻¹ : ℝ≥0) * dist (x : K) (y : K) := by
          rw [NNReal.coe_mul, coe_nnnorm, dist_eq_norm]
      _ = (‖j₀‖₊⁻¹ : ℝ≥0) * dist x y := rfl
  have hcontract : ContractingWith ‖j₀‖₊⁻¹ φ := ⟨hρlt, hlip⟩

  obtain ⟨x, hfixB⟩ : ∃ y : B, φ y = y :=
    ⟨ContractingWith.fixedPoint φ hcontract, hcontract.fixedPoint_isFixedPt⟩
  have hfix : jInversionStep j₀ (x : K) = (x : K) := congrArg Subtype.val hfixB

  have hxnorm : ‖(x : K)‖₊ = ‖j₀‖₊⁻¹ := by
    rw [← hfix]
    exact nnnorm_jInversionStep hj ((hmem _).mp x.2)
  have hx0 : (x : K) ≠ 0 := by
    intro h
    rw [h, nnnorm_zero] at hxnorm
    exact hρpos.ne' hxnorm.symm
  exact ⟨(x : K), hx0, hxnorm, (jInversionStep_eq_self_iff hj₀0).mp hfix⟩

theorem tateParameter_unique {j₀ q₁ q₂ : K} (hj : 1 < ‖j₀‖₊)
    (hq₁ : ‖q₁‖₊ < 1) (hq₂ : ‖q₂‖₊ < 1)
    (h₁ : (curve q₁).c₄ ^ 3 = j₀ * (curve q₁).Δ)
    (h₂ : (curve q₂).c₄ ^ 3 = j₀ * (curve q₂).Δ) : q₁ = q₂ := by
  have hpos : (0 : ℝ≥0) < ‖j₀‖₊ := lt_trans zero_lt_one hj
  have hj₀0 : j₀ ≠ 0 := by
    intro h
    rw [h, nnnorm_zero] at hj
    exact (lt_irrefl _ (lt_trans zero_lt_one hj)).elim
  have hρlt : ‖j₀‖₊⁻¹ < 1 := by
    have h := mul_lt_mul_of_pos_left hj (inv_pos.mpr hpos)
    rwa [mul_one, inv_mul_cancel₀ hpos.ne'] at h
  by_contra hne
  have hd : (0 : ℝ≥0) < ‖q₁ - q₂‖₊ := by
    rw [pos_iff_ne_zero, ne_eq, nnnorm_eq_zero, sub_eq_zero]
    exact hne
  have hfix₁ : jInversionStep j₀ q₁ = q₁ := (jInversionStep_eq_self_iff hj₀0).mpr h₁
  have hfix₂ : jInversionStep j₀ q₂ = q₂ := (jInversionStep_eq_self_iff hj₀0).mpr h₂
  have hkey : ‖q₁ - q₂‖₊ ≤ max (max ‖q₁‖₊ ‖q₂‖₊) ‖j₀‖₊⁻¹ * ‖q₁ - q₂‖₊ := by
    conv_lhs => rw [← hfix₁, ← hfix₂]
    exact nnnorm_jInversionStep_sub_le hj hq₁ hq₂
  have hr : max (max ‖q₁‖₊ ‖q₂‖₊) ‖j₀‖₊⁻¹ < 1 := max_lt (max_lt hq₁ hq₂) hρlt
  have hlt : ‖q₁ - q₂‖₊ < ‖q₁ - q₂‖₊ := by
    calc ‖q₁ - q₂‖₊ ≤ max (max ‖q₁‖₊ ‖q₂‖₊) ‖j₀‖₊⁻¹ * ‖q₁ - q₂‖₊ := hkey
      _ < 1 * ‖q₁ - q₂‖₊ := mul_lt_mul_of_pos_right hr hd
      _ = ‖q₁ - q₂‖₊ := one_mul _
  exact lt_irrefl _ hlt

theorem curve_j_eq {q j₀ : K} (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (h : (curve q).c₄ ^ 3 = j₀ * (curve q).Δ) :
    haveI := isElliptic hq0 hq
    (curve q).j = j₀ := by
  letI := isElliptic hq0 hq
  have hΔ0 : (curve q).Δ ≠ 0 := Δ_ne_zero hq0 hq
  rw [WeierstrassCurve.j, Units.val_inv_eq_inv_val, WeierstrassCurve.coe_Δ', h,
    mul_comm j₀ ((curve q).Δ), ← mul_assoc, inv_mul_cancel₀ hΔ0, one_mul]

theorem c₄_pow_eq_of_curve_j_eq {q j₀ : K} (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (h : (haveI := isElliptic hq0 hq; (curve q).j) = j₀) :
    (curve q).c₄ ^ 3 = j₀ * (curve q).Δ := by
  letI := isElliptic hq0 hq
  have hΔ0 : (curve q).Δ ≠ 0 := Δ_ne_zero hq0 hq
  rw [WeierstrassCurve.j, Units.val_inv_eq_inv_val, WeierstrassCurve.coe_Δ'] at h
  calc (curve q).c₄ ^ 3 = ((curve q).Δ * (curve q).Δ⁻¹) * (curve q).c₄ ^ 3 := by
        rw [mul_inv_cancel₀ hΔ0, one_mul]
    _ = (curve q).Δ * ((curve q).Δ⁻¹ * (curve q).c₄ ^ 3) := by ring
    _ = (curve q).Δ * j₀ := by rw [h]
    _ = j₀ * (curve q).Δ := mul_comm _ _

theorem exists_tateParameter (j₀ : K) (hj : 1 < ‖j₀‖₊) :
    ∃ q : K, ∃ (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1),
      ‖q‖₊ = ‖j₀‖₊⁻¹ ∧ (haveI := isElliptic hq0 hq; (curve q).j) = j₀ := by
  obtain ⟨q, hq0, hqnorm, halg⟩ := exists_tateParameter_c₄ j₀ hj
  have hpos : (0 : ℝ≥0) < ‖j₀‖₊ := lt_trans zero_lt_one hj
  have hρlt : ‖j₀‖₊⁻¹ < 1 := by
    have h := mul_lt_mul_of_pos_left hj (inv_pos.mpr hpos)
    rwa [mul_one, inv_mul_cancel₀ hpos.ne'] at h
  have hq : ‖q‖₊ < 1 := by rw [hqnorm]; exact hρlt
  exact ⟨q, hq0, hq, hqnorm, curve_j_eq hq0 hq halg⟩

theorem exists_tateParameter_of_isElliptic (E : WeierstrassCurve K) [E.IsElliptic]
    (hE : 1 < ‖E.j‖₊) :
    ∃ q : K, ∃ (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1),
      ‖q‖₊ = ‖E.j‖₊⁻¹ ∧ (haveI := isElliptic hq0 hq; (curve q).j) = E.j :=
  exists_tateParameter E.j hE

end TateParameter

end TateCurve