-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma Ψ_even (m : ℤ) : W.Ψ (2 * m) * W.ψ₂ =
    W.Ψ (m - 1) ^ 2 * W.Ψ m * W.Ψ (m + 2) - W.Ψ (m - 2) * W.Ψ m * W.Ψ (m + 1) ^ 2

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

Tactic:
rw [Ψ]

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

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

Tactic:
ring1

Result:
no goals

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

Tactic:
repeat rw [Ψ]

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

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

Tactic:
simp_rw [preΨ_even, if_pos <| even_two_mul _, Int.even_add_one, show m + 2 = m + 1 + 1 by ring1,
  Int.even_add_one, show m - 2 = m - 1 - 1 by ring1, Int.even_sub_one, ite_not]

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

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

Tactic:
split_ifs <;> C_simp <;> ring1

Result:
no goals

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

Tactic:
ring1

Result:
no goals