-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
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 := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
zero : natDegree (W.preΨ' 0) ≤ expDegree 0 ∧ coeff (W.preΨ' 0) (expDegree 0) = (↑(expCoeff 0) : R)
one : natDegree (W.preΨ' 1) ≤ expDegree 1 ∧ coeff (W.preΨ' 1) (expDegree 1) = (↑(expCoeff 1) : R)
two : natDegree (W.preΨ' 2) ≤ expDegree 2 ∧ coeff (W.preΨ' 2) (expDegree 2) = (↑(expCoeff 2) : R)
three : natDegree (W.preΨ' 3) ≤ expDegree 3 ∧ coeff (W.preΨ' 3) (expDegree 3) = (↑(expCoeff 3) : R)
four : natDegree (W.preΨ' 4) ≤ expDegree 4 ∧ coeff (W.preΨ' 4) (expDegree 4) = (↑(expCoeff 4) : R)
even :
  ∀ (m : ℕ)
    (h₁ :
      natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
        coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R))
    (h₂ :
      natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
        coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R))
    (h₃ :
      natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
        coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R))
    (h₄ :
      natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
        coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R))
    (h₅ :
      natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
        coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)),
    natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3)) ∧
      coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)
odd :
  ∀ (m : ℕ)
    (h₁ :
      natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
        coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R))
    (h₂ :
      natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
        coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R))
    (h₃ :
      natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
        coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R))
    (h₄ :
      natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
        coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)),
    natDegree (W.preΨ' (2 * (m + 2) + 1)) ≤ expDegree (2 * (m + 2) + 1) ∧
      coeff (W.preΨ' (2 * (m + 2) + 1)) (expDegree (2 * (m + 2) + 1)) = (↑(expCoeff (2 * (m + 2) + 1)) : R)
⊢ natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R)

Tactic:
induction n using normEDSRec with
  | zero => simpa only [preΨ'_zero] using ⟨natDegree_zero.le, Int.cast_zero.symm⟩
  | one => simpa only [preΨ'_one] using ⟨natDegree_one.le, coeff_one_zero.trans Int.cast_one.symm⟩
  | two => simpa only [preΨ'_two] using ⟨natDegree_one.le, coeff_one_zero.trans Int.cast_one.symm⟩
  | three => simpa only [preΨ'_three] using ⟨W.natDegree_Ψ₃_le, W.coeff_Ψ₃ ▸ Int.cast_three.symm⟩
  | four => simpa only [preΨ'_four] using ⟨W.natDegree_preΨ₄_le, W.coeff_preΨ₄ ▸ Int.cast_two.symm⟩
  | even m h₁ h₂ h₃ h₄ h₅ =>
    constructor
    · nth_rw 1 [preΨ'_even, ← max_self <| expDegree _, (expDegree_rec m).1.1, (expDegree_rec m).1.2]
      exact natDegree_sub_le_of_le (dm (dm (dp h₂.1) h₃.1) h₅.1) (dm (dm h₁.1 h₃.1) (dp h₄.1))
    · nth_rw 1 [preΨ'_even, coeff_sub, (expDegree_rec m).1.1, cm (dm (dp h₂.1) h₃.1) h₅.1,
        cm (dp h₂.1) h₃.1, cp h₂.1, h₂.2, h₃.2, h₅.2, (expDegree_rec m).1.2,
        cm (dm h₁.1 h₃.1) (dp h₄.1), cm h₁.1 h₃.1, h₁.2, cp h₄.1, h₃.2, h₄.2, (expCoeff_rec m).1]
      norm_cast
  | odd m h₁ h₂ h₃ h₄ =>
    rw [preΨ'_odd]
    constructor
    · nth_rw 1 [← max_self <| expDegree _, (expDegree_rec m).2.1, (expDegree_rec m).2.2]
      refine natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp h₃.1)) ?_) <;>
        split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]
    · nth_rw 1 [coeff_sub, (expDegree_rec m).2.1, cm (dm h₄.1 (dp h₂.1)), cm h₄.1 (dp h₂.1),
        h₄.2, cp h₂.1, h₂.2, apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_Ψ₂Sq, coeff_one_zero,
        (expDegree_rec m).2.2, cm (dm h₁.1 (dp h₃.1)), cm h₁.1 (dp h₃.1), h₁.2, cp h₃.1, h₃.2,
        apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_one_zero, coeff_Ψ₂Sq, (expCoeff_rec m).2]
      · norm_cast
      all_goals split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

Premises used: WeierstrassCurve.coeff_Ψ₂Sq, apply_ite₂, WeierstrassCurve.preΨ'_zero, _private.0.WeierstrassCurve.expDegree, WeierstrassCurve.preΨ'_one, WeierstrassCurve.preΨ'_even, Eq.le, max_self, WeierstrassCurve.preΨ'_three, Polynomial.coeff, WeierstrassCurve.preΨ'_odd, Polynomial.natDegree_one, Polynomial.coeff_sub, WeierstrassCurve.natDegree_Ψ₂Sq_le, Polynomial.coeff_one_zero, WeierstrassCurve.preΨ'_two, WeierstrassCurve.preΨ'_four