-- 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:
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)

Tactic:
refine natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp h₃.1)) ?_)

Result:
case odd.left.refine_1
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))
⊢ (if Even m then W.Ψ₂Sq ^ 2 else 1).natDegree ≤ if Even m then 2 * 3 else 0

case odd.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
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))
⊢ (if Even m then 1 else W.Ψ₂Sq ^ 2).natDegree ≤ if Even m then 0 else 2 * 3