-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma Ψ_odd_ofNat (m : ℕ) : W.Ψ (2 * (m + 2) + 1) =
    W.Ψ (m + 4) * W.Ψ (m + 2) ^ 3 - W.Ψ (m + 1) * W.Ψ (m + 3) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3
            else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3)

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

Tactic:
rw_mod_cast [Ψ_ofNat]

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

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

Tactic:
repeat rw_mod_cast [Ψ_ofNat]

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

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

Tactic:
simp_rw [preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, Nat.even_add_one, ite_not]

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

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

Tactic:
split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1

Result:
no goals