-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
pos :
  Even m →
    HMul.hMul (α := R[X][Y]) (β := R[X][Y])
          ((C : (a : R[X]) → R[X][Y])
              (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m - 1)) 2 * W.preΨ m * W.preΨ (m + 2) -
                HMul.hMul (α := R[X]) (W.preΨ (m - 2)) (W.preΨ m) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 2) :
            R[X][Y])
          W.ψ₂ *
        W.ψ₂ =
      HPow.hPow (β := ℕ)
              (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
                (1 : R[X][Y]))
              2 *
            HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂ *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) W.ψ₂ *
            HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
              (1 : R[X][Y]))
            2
⊢ HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y])
            (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m - 1)) 2 * W.preΨ m * W.preΨ (m + 2) -
              HMul.hMul (α := R[X]) (W.preΨ (m - 2)) (W.preΨ m) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 2) :
          R[X][Y])
        W.ψ₂ *
      W.ψ₂ =
    HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
              (if ¬Even m then W.ψ₂ else 1))
            2 *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y])
            (if Even m then W.ψ₂ else 1) *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
          (if Even m then W.ψ₂ else 1) -
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y])
            (if Even m then W.ψ₂ else 1) *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y])
            (if Even m then W.ψ₂ else 1) *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
            (if ¬Even m then W.ψ₂ else 1))
          2
have neg : ¬Even m →
  HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y])
            (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m - 1)) 2 * W.preΨ m * W.preΨ (m + 2) -
              HMul.hMul (α := R[X]) (W.preΨ (m - 2)) (W.preΨ m) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 2) :
          R[X][Y])
        W.ψ₂ *
      W.ψ₂ =
    HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂) 2 *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) -
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) (1 : R[X][Y]) *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 2
Tactic: split_ifs