-- 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])
            (W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3 * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 -
              W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3 * 1) :
          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]) W.ψ₂ *
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂) 3 -
          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]) *
            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]))
              3 +
        HMul.hMul (β := R[X][Y])
          (W.toAffine.polynomial *
            (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
          ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3) : R[X][Y])
⊢ HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((C : (a : R[X]) → R[X][Y])
          ((W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3 *
              if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
            W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3 *
              if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 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])
            (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) : R[X][Y])
              (if Even m then W.ψ₂ else 1))
            3 -
        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) *
          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))
            3 +
      HMul.hMul (β := R[X][Y])
        (W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
        ((C : (a : R[X]) → R[X][Y])
            (if Even m then W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3
            else -W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3) :
          R[X][Y])
have neg : ¬Even m →
  HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((C : (a : R[X]) → R[X][Y])
          (W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3 * 1 -
            W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3 *
              HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 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]) *
          HPow.hPow (β := ℕ)
            (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]))
            3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : 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]) W.ψ₂) 3 +
      HMul.hMul (β := R[X][Y])
        (W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
        ((C : (a : R[X]) → R[X][Y]) (-W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3) : R[X][Y])
Tactic: split_ifs