-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
⊢ (C : (a : R[X]) → R[X][Y])
      (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]))) =
    HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
          ((C : (a : R[X]) → R[X][Y])
              (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])) :
            R[X][Y]) *
        HSub.hSub (β := R[X][Y])
          (HSub.hSub (α := R[X][Y]) (β := 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'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
              R[X][Y]))
          ((C : (a : R[X]) → R[X][Y])
              (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])) :
            R[X][Y]) +
      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])
have eval_simp : (C : (a : R[X]) → R[X][Y])
    (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])) =
  HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
        ((C : (a : R[X]) → R[X][Y])
            (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])) :
          R[X][Y]) *
      HSub.hSub (β := R[X][Y])
        (HSub.hSub (α := R[X][Y]) (β := 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'.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
            R[X][Y]))
        ((C : (a : R[X]) → R[X][Y])
            (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])) :
          R[X][Y]) +
    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])
Tactic: eval_simp