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

Tactic:
ring1