-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
⊢ eval
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
        ((C : (a : R) → R[X]) y : R[X]))
      (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'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.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'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₆ : R[X])) :
          R[X][Y])) =
    -HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X])
              ((C : (a : R) → R[X])
                  { a := 1, b := -HPow.hPow (β := ℕ) ℓ 2 - W'.a₁ * ℓ + W'.a₂,
                      c := 2 * x * HPow.hPow (β := ℕ) ℓ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                      d :=
                        -HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) ℓ 2 + (2 * x * y + W'.a₃ * x) * ℓ -
                          (HPow.hPow (β := ℕ) y 2 + W'.a₃ * y - W'.a₆) :
                      Cubic R }.a :
                R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X])
              ((C : (a : R) → R[X])
                  { a := 1, b := -HPow.hPow (β := ℕ) ℓ 2 - W'.a₁ * ℓ + W'.a₂,
                      c := 2 * x * HPow.hPow (β := ℕ) ℓ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                      d :=
                        -HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) ℓ 2 + (2 * x * y + W'.a₃ * x) * ℓ -
                          (HPow.hPow (β := ℕ) y 2 + W'.a₃ * y - W'.a₆) :
                      Cubic R }.b :
                R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X])
                { a := 1, b := -HPow.hPow (β := ℕ) ℓ 2 - W'.a₁ * ℓ + W'.a₂,
                    c := 2 * x * HPow.hPow (β := ℕ) ℓ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                    d :=
                      -HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) ℓ 2 + (2 * x * y + W'.a₃ * x) * ℓ -
                        (HPow.hPow (β := ℕ) y 2 + W'.a₃ * y - W'.a₆) :
                    Cubic R }.c :
              R[X])
            X)
        ((C : (a : R) → R[X])
            { a := 1, b := -HPow.hPow (β := ℕ) ℓ 2 - W'.a₁ * ℓ + W'.a₂,
                c := 2 * x * HPow.hPow (β := ℕ) ℓ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                d :=
                  -HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) ℓ 2 + (2 * x * y + W'.a₃ * x) * ℓ -
                    (HPow.hPow (β := ℕ) y 2 + W'.a₃ * y - W'.a₆) }.d :
          R[X])
have eval_simp : HPow.hPow (β := ℕ)
        (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
          ((C : (a : R) → R[X]) y : R[X]))
        2 +
      HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X]) *
        HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
          ((C : (a : R) → R[X]) y : R[X]) -
    HAdd.hAdd (β := R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
      ((C : (a : R) → R[X]) W'.a₆ : R[X]) =
  -HAdd.hAdd (β := R[X])
      ((C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (-HPow.hPow (β := ℕ) ℓ 2 - W'.a₁ * ℓ + W'.a₂) : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X])
              (2 * x * HPow.hPow (β := ℕ) ℓ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄)) :
            R[X])
          X)
      ((C : (a : R) → R[X])
          (-HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) ℓ 2 + (2 * x * y + W'.a₃ * x) * ℓ -
            (HPow.hPow (β := ℕ) y 2 + W'.a₃ * y - W'.a₆)) :
        R[X])
Tactic: eval_simp