-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
⊢ 1 *
            (Y -
              (-Y -
                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 -
            (-Y -
              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]))) +
        -4 *
          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]) -
      (HPow.hPow (β := ℕ)
                  (HSub.hSub (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y₁) : F[X][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])))
                  2 *
                1 +
              HMul.hMul (α := F[X][Y]) 1 4 *
                (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])) +
            (HMul.hMul (α := F[X][Y]) 1 4 *
                    HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) 2 +
                  HMul.hMul (β := F[X][Y])
                    (HMul.hMul (β := F[X][Y]) (HMul.hMul (α := F[X][Y]) 1 4)
                        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y]) +
                      1 *
                        (HPow.hPow (α := F[X][Y]) (β := ℕ)
                            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y]) 2 +
                          HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (4 : 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]) +
                (HMul.hMul (α := F[X][Y]) 1 4 *
                      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])
                      (1 *
                        (HPow.hPow (α := F[X][Y]) (β := ℕ)
                            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y]) 2 +
                          HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (4 : 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]) +
                  HMul.hMul (α := F[X][Y]) 1 2 *
                    (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (2 : 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])
                        ((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 (β := ℕ)
                (HSub.hSub (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y₁) : F[X][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])))
                2 *
              0 *
            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]) +
        -4 *
          (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]))) =
    0

Tactic:
ring1