-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ 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.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.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.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.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.a₆) : R[X][Y]) =
    (C : (a : R[X]) → R[X][Y]) 0 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 3 +
          (C : (a : R[X]) → R[X][Y]) 1 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
        HAdd.hAdd (β := R[X][Y])
            (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 0) : 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]) 0) : 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.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.a₃) : R[X][Y]) *
          Y +
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (-(C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 1) : 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.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.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.a₆) : R[X][Y])
have simp : 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.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.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.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.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.a₆) : R[X][Y]) =
  0 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 3 + 1 * HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
      HAdd.hAdd (β := R[X][Y])
          (0 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
              0 * 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.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.a₃) : R[X][Y]) *
        Y +
    HAdd.hAdd (β := R[X][Y])
      (-1 * 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.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.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.a₆) : R[X][Y])
Tactic: simp only [C_0, C_1]