-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
C_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]) =
    -(1 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HAdd.hAdd (β := R[X])
                (-HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) ℓ : R[X]) 2 -
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) ((C : (a : R) → R[X]) ℓ : R[X]))
                ((C : (a : R) → R[X]) W'.a₂ : R[X]) *
              HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          (HMul.hMul (α := R[X]) (β := R[X]) (2 : R[X]) ((C : (a : R) → R[X]) x : R[X]) *
                  HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) ℓ : R[X]) 2 +
                HMul.hMul (β := R[X])
                  (HSub.hSub (β := R[X])
                    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X])
                        ((C : (a : R) → R[X]) x : R[X]) -
                      HMul.hMul (α := R[X]) (β := R[X]) (2 : R[X]) ((C : (a : R) → R[X]) y : R[X]))
                    ((C : (a : R) → R[X]) W'.a₃ : R[X]))
                  ((C : (a : R) → R[X]) ℓ : R[X]) +
              HAdd.hAdd (β := R[X])
                (HMul.hMul (α := R[X]) (β := R[X]) (-(C : (a : R) → R[X]) W'.a₁ : R[X]) ((C : (a : R) → R[X]) y : R[X]))
                ((C : (a : R) → R[X]) W'.a₄ : R[X])) *
            X +
        (-HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) x : R[X]) 2 *
              HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) ℓ : R[X]) 2 +
            HMul.hMul (β := R[X])
              (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) (2 : R[X]) ((C : (a : R) → R[X]) x : R[X]))
                  ((C : (a : R) → R[X]) y : R[X]) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₃ : R[X]) ((C : (a : R) → R[X]) x : R[X]))
              ((C : (a : R) → R[X]) ℓ : R[X]) -
          HSub.hSub (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) y : R[X]) 2 +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₃ : R[X]) ((C : (a : R) → R[X]) y : R[X]))
            ((C : (a : R) → R[X]) W'.a₆ : R[X])))
⊢ 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:
C_simp