-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) =
      0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ eval (W'.addX x₁ x₂ ℓ)
      ((C : (a : R) → R[X]) 2 *
              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]) *
            (0 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X]) +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X]) (HSub.hSub (α := R[X]) 1 0) +
              0) +
          ((HMul.hMul (α := R[X]) 0 X +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) (1 : R[X]) +
                0) *
              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]) (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]) *
              (0 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X]) +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X]) (HSub.hSub (α := R[X]) 1 0) +
                0)) -
        ((C : (a : R) → R[X]) (↑3 : R) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 3 1) +
              (0 * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X])
                  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X * 1)) +
            (HMul.hMul (α := R[X]) 0 X +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) (1 : R[X])) +
          0)) =
    0
have simp : eval (W'.addX x₁ x₂ ℓ)
    (HMul.hMul (β := R[X])
          ((C : (a : R) → R[X]) 2 *
            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]))
          ((C : (a : R) → R[X]) ℓ : R[X]) +
        (HMul.hMul (α := R[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])) +
          HMul.hMul (β := R[X])
            (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]))
            ((C : (a : R) → R[X]) ℓ : R[X])) -
      HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) (↑3 : R) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 3 1) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X))
        ((C : (a : R) → R[X]) W'.a₄ : R[X])) =
  0
Tactic: simp only [zero_add, add_zero, sub_zero, zero_mul, mul_one]