-- 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 even.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))
h₅ :
  (W.preΨ' (m + 5)).natDegree ≤ WeierstrassCurve.expDegree (m + 5) ∧
    (W.preΨ' (m + 5)).coeff (WeierstrassCurve.expDegree (m + 5)) = ↑(WeierstrassCurve.expCoeff (m + 5))
⊢ (W.preΨ' (2 * (m + 3))).natDegree ≤ WeierstrassCurve.expDegree (2 * (m + 3))

Tactic:
nth_rw 1 [preΨ'_even, ← max_self <| expDegree _, (expDegree_rec m).1.1, (expDegree_rec m).1.2]

Result:
case even.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))
h₅ :
  (W.preΨ' (m + 5)).natDegree ≤ WeierstrassCurve.expDegree (m + 5) ∧
    (W.preΨ' (m + 5)).coeff (WeierstrassCurve.expDegree (m + 5)) = ↑(WeierstrassCurve.expCoeff (m + 5))
⊢ (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2).natDegree ≤
    (2 * WeierstrassCurve.expDegree (m + 2) + WeierstrassCurve.expDegree (m + 3) + WeierstrassCurve.expDegree (m + 5)) ⊔
      (WeierstrassCurve.expDegree (m + 1) + WeierstrassCurve.expDegree (m + 3) + 2 * WeierstrassCurve.expDegree (m + 4))

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

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

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
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
⊢ natDegree 0 ≤ WeierstrassCurve.expDegree 0

Tactic:
rfl

Result:
no goals

Proof state:
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))
⊢ ((↑(WeierstrassCurve.expCoeff (m + 4)) * ↑(WeierstrassCurve.expCoeff (m + 2)) ^ 3 * if Even m then 4 ^ 2 else 1) -
      ↑(WeierstrassCurve.expCoeff (m + 1)) * ↑(WeierstrassCurve.expCoeff (m + 3)) ^ 3 * if Even m then 1 else 4 ^ 2) =
    ↑((WeierstrassCurve.expCoeff (m + 4) * WeierstrassCurve.expCoeff (m + 2) ^ 3 * if Even m then 4 ^ 2 else 1) -
        WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) ^ 3 * if Even m then 1 else 4 ^ 2)

Tactic:
norm_cast

Result:
no goals