-- 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
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) ∧
    ((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).coeff
        (WeierstrassCurve.expDegree (2 * (m + 2) + 1)) =
      ↑(WeierstrassCurve.expCoeff (2 * (m + 2) + 1))

Tactic:
constructor

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 (2 * (m + 2) + 1)

case odd.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))
⊢ ((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).coeff
      (WeierstrassCurve.expDegree (2 * (m + 2) + 1)) =
    ↑(WeierstrassCurve.expCoeff (2 * (m + 2) + 1))

Proof state:
case three
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
⊢ (W.preΨ' 3).natDegree ≤ WeierstrassCurve.expDegree 3 ∧
    (W.preΨ' 3).coeff (WeierstrassCurve.expDegree 3) = ↑(WeierstrassCurve.expCoeff 3)

Tactic:
simpa only [preΨ'_three] using ⟨W.natDegree_Ψ₃_le, W.coeff_Ψ₃ ▸ Int.cast_three.symm⟩

Result:
no goals