-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma natDegree_coeff_preΨ' (n : ℕ) :
    (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = expCoeff n

Proof state:
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
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
⊢ (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)

Tactic:
let cm {m n p q} : _ → _ → (p * q : R[X]).coeff (m + n) = _ := coeff_mul_of_natDegree_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
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
⊢ (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)

Proof state:
case odd.left
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
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} => coeff_pow_of_natDegree_le
m : ℕ
h₁ :
  (W.preΨ' (m + 1)).natDegree ≤ WeierstrassCurve.expDegree (m + 1) ∧
    (W.preΨ' (m + 1)).coeff (WeierstrassCurve.expDegree (m + 1)) = ↑(WeierstrassCurve.expCoeff (m + 1))
h₂ :
  (W.preΨ' (m + 2)).natDegree ≤ WeierstrassCurve.expDegree (m + 2) ∧
    (W.preΨ' (m + 2)).coeff (WeierstrassCurve.expDegree (m + 2)) = ↑(WeierstrassCurve.expCoeff (m + 2))
h₃ :
  (W.preΨ' (m + 3)).natDegree ≤ WeierstrassCurve.expDegree (m + 3) ∧
    (W.preΨ' (m + 3)).coeff (WeierstrassCurve.expDegree (m + 3)) = ↑(WeierstrassCurve.expCoeff (m + 3))
h₄ :
  (W.preΨ' (m + 4)).natDegree ≤ WeierstrassCurve.expDegree (m + 4) ∧
    (W.preΨ' (m + 4)).coeff (WeierstrassCurve.expDegree (m + 4)) = ↑(WeierstrassCurve.expCoeff (m + 4))
⊢ ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2).natDegree ≤
    WeierstrassCurve.expDegree (2 * (m + 2) + 1)

Tactic:
nth_rw 1 [← max_self <| expDegree _, (expDegree_rec m).2.1, (expDegree_rec m).2.2]

Result:
case odd.left
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
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} => coeff_pow_of_natDegree_le
m : ℕ
h₁ :
  (W.preΨ' (m + 1)).natDegree ≤ WeierstrassCurve.expDegree (m + 1) ∧
    (W.preΨ' (m + 1)).coeff (WeierstrassCurve.expDegree (m + 1)) = ↑(WeierstrassCurve.expCoeff (m + 1))
h₂ :
  (W.preΨ' (m + 2)).natDegree ≤ WeierstrassCurve.expDegree (m + 2) ∧
    (W.preΨ' (m + 2)).coeff (WeierstrassCurve.expDegree (m + 2)) = ↑(WeierstrassCurve.expCoeff (m + 2))
h₃ :
  (W.preΨ' (m + 3)).natDegree ≤ WeierstrassCurve.expDegree (m + 3) ∧
    (W.preΨ' (m + 3)).coeff (WeierstrassCurve.expDegree (m + 3)) = ↑(WeierstrassCurve.expCoeff (m + 3))
h₄ :
  (W.preΨ' (m + 4)).natDegree ≤ WeierstrassCurve.expDegree (m + 4) ∧
    (W.preΨ' (m + 4)).coeff (WeierstrassCurve.expDegree (m + 4)) = ↑(WeierstrassCurve.expCoeff (m + 4))
⊢ ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2).natDegree ≤
    (WeierstrassCurve.expDegree (m + 4) + 3 * WeierstrassCurve.expDegree (m + 2) + if Even m then 2 * 3 else 0) ⊔
      (WeierstrassCurve.expDegree (m + 1) + 3 * WeierstrassCurve.expDegree (m + 3) + if Even m then 0 else 2 * 3)

Proof state:
case even.right
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
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} => coeff_pow_of_natDegree_le
m : ℕ
h₁ :
  (W.preΨ' (m + 1)).natDegree ≤ WeierstrassCurve.expDegree (m + 1) ∧
    (W.preΨ' (m + 1)).coeff (WeierstrassCurve.expDegree (m + 1)) = ↑(WeierstrassCurve.expCoeff (m + 1))
h₂ :
  (W.preΨ' (m + 2)).natDegree ≤ WeierstrassCurve.expDegree (m + 2) ∧
    (W.preΨ' (m + 2)).coeff (WeierstrassCurve.expDegree (m + 2)) = ↑(WeierstrassCurve.expCoeff (m + 2))
h₃ :
  (W.preΨ' (m + 3)).natDegree ≤ WeierstrassCurve.expDegree (m + 3) ∧
    (W.preΨ' (m + 3)).coeff (WeierstrassCurve.expDegree (m + 3)) = ↑(WeierstrassCurve.expCoeff (m + 3))
h₄ :
  (W.preΨ' (m + 4)).natDegree ≤ WeierstrassCurve.expDegree (m + 4) ∧
    (W.preΨ' (m + 4)).coeff (WeierstrassCurve.expDegree (m + 4)) = ↑(WeierstrassCurve.expCoeff (m + 4))
h₅ :
  (W.preΨ' (m + 5)).natDegree ≤ WeierstrassCurve.expDegree (m + 5) ∧
    (W.preΨ' (m + 5)).coeff (WeierstrassCurve.expDegree (m + 5)) = ↑(WeierstrassCurve.expCoeff (m + 5))
⊢ ↑(WeierstrassCurve.expCoeff (m + 2)) ^ 2 * ↑(WeierstrassCurve.expCoeff (m + 3)) *
        ↑(WeierstrassCurve.expCoeff (m + 5)) -
      ↑(WeierstrassCurve.expCoeff (m + 1)) * ↑(WeierstrassCurve.expCoeff (m + 3)) *
        ↑(WeierstrassCurve.expCoeff (m + 4)) ^ 2 =
    ↑(WeierstrassCurve.expCoeff (m + 2) ^ 2 * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 5) -
        WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 4) ^ 2)

Tactic:
norm_cast

Result:
no goals