-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma natDegree_coeff_ΨSq_ofNat (n : ℕ) :
    (W.ΨSq n).natDegree ≤ n ^ 2 - 1 ∧ (W.ΨSq n).coeff (n ^ 2 - 1) = (n ^ 2 : ℤ)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ (↑n + 1) ^ 2 = (if Even (n + 1) then (↑n + 1) / 2 else ↑n + 1) ^ 2 * if Even (n + 1) then 4 else 1

Tactic:
split_ifs <;> ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
⊢ (W.ΨSq ↑(n + 1)).natDegree ≤ (n + 1) ^ 2 - 1 ∧ (W.ΨSq ↑(n + 1)).coeff ((n + 1) ^ 2 - 1) = ↑(↑(n + 1) ^ 2)

Tactic:
have hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0 := by
  push_cast [← @Nat.cast_inj ℤ, add_sq, expDegree_cast (by omega : n + 1 ≠ 0)]
  split_ifs <;> ring1

Result:
case succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ (W.ΨSq ↑(n + 1)).natDegree ≤ (n + 1) ^ 2 - 1 ∧ (W.ΨSq ↑(n + 1)).coeff ((n + 1) ^ 2 - 1) = ↑(↑(n + 1) ^ 2)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
⊢ (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0

Tactic:
push_cast [← @Nat.cast_inj ℤ, add_sq, expDegree_cast (by omega : n + 1 ≠ 0)]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
⊢ ↑n ^ 2 + 2 * ↑n * 1 = (↑n ^ 2 + 2 * ↑n * 1 + 1 - if Even (n + 1) then 4 else 1) + if Even (n + 1) then 3 else 0

Proof state:
case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤ if Even (n + 1) then 3 else 0

Tactic:
split_ifs <;> simp only [apply_ite natDegree, natDegree_one.le, W.natDegree_Ψ₂Sq_le]

Result:
no goals

Proof state:
case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
      (2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
    ↑(↑(n + 1) ^ 2)

Tactic:
rw [coeff_mul_of_natDegree_le (dp h.1), coeff_pow_of_natDegree_le h.1, h.2, apply_ite₂ coeff,
  coeff_Ψ₂Sq, coeff_one_zero, hc]

Result:
case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (↑(WeierstrassCurve.expCoeff (n + 1)) ^ 2 * if Even (n + 1) then 4 else 1) =
    ↑(WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1)

case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤ if Even (n + 1) then 3 else 0

Proof state:
case succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (↑(WeierstrassCurve.expCoeff (n + 1)) ^ 2 * if Even (n + 1) then 4 else 1) =
    ↑(WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1)

Tactic:
norm_cast

Result:
no goals