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

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

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

Result:
no goals

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

Tactic:
simp_rw [preΨ_odd, if_neg m.not_even_two_mul_add_one, show m + 2 = m + 1 + 1 by ring1,
  Int.even_add_one, Int.even_sub_one, ite_not]

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

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

Tactic:
rw [Ψ]

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

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

Tactic:
repeat rw [Ψ]

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

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ m + 2 = m + 1 + 1

Tactic:
ring1

Result:
no goals