-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma Ψ_even_ofNat (m : ℕ) : W.Ψ (2 * (m + 3)) * W.ψ₂ =
    W.Ψ (m + 2) ^ 2 * W.Ψ (m + 3) * W.Ψ (m + 5) - W.Ψ (m + 1) * W.Ψ (m + 3) * W.Ψ (m + 4) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ W.Ψ (2 * (↑m + 3)) * W.ψ₂ =
    W.Ψ (↑m + 2) ^ 2 * W.Ψ (↑m + 3) * W.Ψ (↑m + 5) - W.Ψ (↑m + 1) * W.Ψ (↑m + 3) * W.Ψ (↑m + 4) ^ 2

Tactic:
repeat rw_mod_cast [Ψ_ofNat]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ (C (W.preΨ' (2 * (m + 3))) * if Even (2 * (m + 3)) then W.ψ₂ else 1) * W.ψ₂ =
    (C (W.preΨ' (m + 2)) * if Even (m + 2) then W.ψ₂ else 1) ^ 2 *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        (C (W.preΨ' (m + 5)) * if Even (m + 5) then W.ψ₂ else 1) -
      (C (W.preΨ' (m + 1)) * if Even (m + 1) then W.ψ₂ else 1) *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        (C (W.preΨ' (m + 4)) * if Even (m + 4) then W.ψ₂ else 1) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ (C (W.preΨ' (2 * (m + 3))) * if Even (2 * (m + 3)) then W.ψ₂ else 1) * W.ψ₂ =
    (C (W.preΨ' (m + 2)) * if Even (m + 2) then W.ψ₂ else 1) ^ 2 *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        (C (W.preΨ' (m + 5)) * if Even (m + 5) then W.ψ₂ else 1) -
      (C (W.preΨ' (m + 1)) * if Even (m + 1) then W.ψ₂ else 1) *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        (C (W.preΨ' (m + 4)) * if Even (m + 4) then W.ψ₂ else 1) ^ 2

Tactic:
simp_rw [preΨ'_even, if_pos <| even_two_mul _, Nat.even_add_one, ite_not]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ C
          (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) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ' (m + 2)) * if Even m then W.ψ₂ else 1) ^ 2 * (C (W.preΨ' (m + 3)) * if Even m then 1 else W.ψ₂) *
        (C (W.preΨ' (m + 5)) * if Even m then 1 else W.ψ₂) -
      (C (W.preΨ' (m + 1)) * if Even m then 1 else W.ψ₂) * (C (W.preΨ' (m + 3)) * if Even m then 1 else W.ψ₂) *
        (C (W.preΨ' (m + 4)) * if Even m then W.ψ₂ else 1) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ (C (W.preΨ' (2 * (m + 3))) * if Even (2 * (m + 3)) then W.ψ₂ else 1) * W.ψ₂ =
    (C (W.preΨ' (m + 2)) * if Even (m + 2) then W.ψ₂ else 1) ^ 2 *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        (C (W.preΨ' (m + 5)) * if Even (m + 5) then W.ψ₂ else 1) -
      (C (W.preΨ' (m + 1)) * if Even (m + 1) then W.ψ₂ else 1) *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        W.Ψ ↑(m + 4) ^ 2

Tactic:
rw_mod_cast [Ψ_ofNat]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ (C (W.preΨ' (2 * (m + 3))) * if Even (2 * (m + 3)) then W.ψ₂ else 1) * W.ψ₂ =
    (C (W.preΨ' (m + 2)) * if Even (m + 2) then W.ψ₂ else 1) ^ 2 *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        (C (W.preΨ' (m + 5)) * if Even (m + 5) then W.ψ₂ else 1) -
      (C (W.preΨ' (m + 1)) * if Even (m + 1) then W.ψ₂ else 1) *
          (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) *
        (C (W.preΨ' (m + 4)) * if Even (m + 4) then W.ψ₂ else 1) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ C
          (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) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ' (m + 2)) * if Even m then W.ψ₂ else 1) ^ 2 * (C (W.preΨ' (m + 3)) * if Even m then 1 else W.ψ₂) *
        (C (W.preΨ' (m + 5)) * if Even m then 1 else W.ψ₂) -
      (C (W.preΨ' (m + 1)) * if Even m then 1 else W.ψ₂) * (C (W.preΨ' (m + 3)) * if Even m then 1 else W.ψ₂) *
        (C (W.preΨ' (m + 4)) * if Even m then W.ψ₂ else 1) ^ 2

Tactic:
split_ifs <;> C_simp <;> ring1

Result:
no goals