-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
            (Y -
              HSub.hSub (β := F[X][Y])
                (HSub.hSub (α := F[X][Y]) (-(C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y])
                  (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y])))
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₃) : F[X][Y])) -
          HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) *
            (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) 2 +
                  HMul.hMul (β := F[X][Y])
                    (HAdd.hAdd (α := F[X][Y]) (β := F[X][Y])
                      ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y])
                      ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y]))
                    ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) +
                HAdd.hAdd (β := F[X][Y])
                  (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) 2 +
                    HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                      ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y])
                      ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]))
                  ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₄) : F[X][Y]) -
              HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
                Y) +
        (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) 2 +
            HMul.hMul (β := F[X][Y])
              (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]))
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₃) : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y])) -
      ((HPow.hPow (α := F[X][Y]) (β := ℕ) Y 2 +
              HAdd.hAdd (β := F[X][Y])
                  (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]))
                  ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₃) : F[X][Y]) *
                Y -
            HAdd.hAdd (β := F[X][Y])
              (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) 3 +
                  HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y])
                    (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) 2) +
                HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₄) : F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]))
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₆) : F[X][Y])) *
          1 +
        HAdd.hAdd (β := F[X][Y])
          (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) 3 +
              HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y])
                (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) 2) +
            HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₄) : F[X][Y])
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]))
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₆) : F[X][Y])) =
    0

Tactic:
ring1