-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ (C : (a : R[X]) → R[X][Y])
      (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) : R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * (2 * W.a₄ + W.a₁ * W.a₃)) : R[X]) X)
        ((C : (a : R) → R[X]) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) : R[X])) =
    HPow.hPow (β := ℕ)
        (HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) Y)
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W.toAffine.a₃ : R[X])) :
            R[X][Y]))
        2 -
      4 *
        HSub.hSub (β := R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y])
              ((C : (a : R[X]) → R[X][Y])
                  (HAdd.hAdd (β := R[X])
                    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₁ : R[X]) X)
                    ((C : (a : R) → R[X]) W.toAffine.a₃ : R[X])) :
                R[X][Y])
              Y)
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X])
                (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₂ : R[X])
                      (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₄ : R[X]) X)
                ((C : (a : R) → R[X]) W.toAffine.a₆ : R[X])) :
            R[X][Y])
have C_simp : 4 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
        (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₁) : R[X][Y]) 2 +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y]) (4 : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₂) : R[X][Y])) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2 +
      HMul.hMul (β := R[X][Y])
        (2 *
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) (2 : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₄) : R[X][Y]) +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₁) : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₃) : R[X][Y])))
        ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) +
    (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₃) : R[X][Y]) 2 +
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) (4 : R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₆) : R[X][Y])) =
  HPow.hPow (β := ℕ)
      (HMul.hMul (α := R[X][Y]) 2 Y +
        HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₁) : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₃) : R[X][Y]))
      2 -
    4 *
      (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
          HAdd.hAdd (β := R[X][Y])
              (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₁) : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₃) : R[X][Y]) *
            Y -
        HAdd.hAdd (β := R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
              HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₂) : R[X][Y])
                (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2) +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₄) : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.toAffine.a₆) : R[X][Y]))
Tactic: C_simp