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

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} => coeff_mul_of_natDegree_le
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 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' :
  (n + 1 + 1) ^ 2 =
    WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ 1 =
    (1 * WeierstrassCurve.expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      WeierstrassCurve.expCoeff (n + 3) * WeierstrassCurve.expCoeff (n + 1) * if Even (n + 1) then 4 else 1

Tactic:
push_cast [← @Int.cast_inj ℚ, expCoeff_cast, Nat.even_add_one, ite_not]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} => coeff_mul_of_natDegree_le
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 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' :
  (n + 1 + 1) ^ 2 =
    WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ 1 =
    (1 * (if Even n then (↑n + 2) / 2 else ↑n + 2) ^ 2 * if Even n then 4 else 1) -
      ((if Even n then ↑n + 3 else (↑n + 3) / 2) * if Even n then ↑n + 1 else (↑n + 1) / 2) * if Even n then 1 else 4

Proof state:
case succ.succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} => coeff_mul_of_natDegree_le
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 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' :
  (n + 1 + 1) ^ 2 =
    WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * WeierstrassCurve.expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      WeierstrassCurve.expCoeff (n + 3) * WeierstrassCurve.expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ (W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1

Tactic:
rw [Nat.cast_add, Nat.cast_one, Φ_ofNat]

Result:
case succ.succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} => coeff_mul_of_natDegree_le
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 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' :
  (n + 1 + 1) ^ 2 =
    WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * WeierstrassCurve.expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      WeierstrassCurve.expCoeff (n + 3) * WeierstrassCurve.expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
      (n + 1 + 1) ^ 2 ∧
    ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
            W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        ((n + 1 + 1) ^ 2) =
      1

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1

Tactic:
let dm {m n p q} : _ → _ → (p * q : R[X]).natDegree ≤ m + n := natDegree_mul_le_of_le

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
⊢ (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1

Proof state:
case succ.succ.left.refine_2
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} => coeff_mul_of_natDegree_le
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 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' :
  (n + 1 + 1) ^ 2 =
    WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * WeierstrassCurve.expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      WeierstrassCurve.expCoeff (n + 3) * WeierstrassCurve.expCoeff (n + 1) * 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