-- 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
a :
  HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) 1) : F[X][Y])
            (Y -
              HSub.hSub (α := F[X][Y]) (β := F[X][Y]) (-Y)
                ((C : (a : F[X]) → F[X][Y])
                    (HAdd.hAdd (β := F[X]) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₁ : F[X]) X)
                      ((C : (a : F) → F[X]) W.a₃ : F[X])) :
                  F[X][Y])) *
          (Y -
            HSub.hSub (α := F[X][Y]) (β := F[X][Y]) (-Y)
              ((C : (a : F[X]) → F[X][Y])
                  (HAdd.hAdd (β := F[X]) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₁ : F[X]) X)
                    ((C : (a : F) → F[X]) W.a₃ : F[X])) :
                F[X][Y])) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (-4 : F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆)) :
            F[X][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]) (HPow.hPow (β := ℕ) (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) 2)) :
                  F[X][Y])
                (1 : F[X][Y]) +
              HMul.hMul (α := F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 4)) : F[X][Y])
                (HSub.hSub (β := F[X][Y])
                  (HPow.hPow (α := F[X][Y]) (β := ℕ) Y 2 +
                    HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                      ((C : (a : F[X]) → F[X][Y])
                          (HAdd.hAdd (β := F[X])
                            (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₁ : F[X]) X)
                            ((C : (a : F) → F[X]) W.a₃ : F[X])) :
                        F[X][Y])
                      Y)
                  ((C : (a : F[X]) → F[X][Y])
                      (HAdd.hAdd (β := F[X])
                        (HPow.hPow (α := F[X]) (β := ℕ) X 3 +
                            HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) W.a₂ : F[X])
                              (HPow.hPow (α := F[X]) (β := ℕ) X 2) +
                          HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₄ : F[X]) X)
                        ((C : (a : F) → F[X]) W.a₆ : F[X])) :
                    F[X][Y])))
            ((C : (a : F[X]) → F[X][Y])
                (HAdd.hAdd (β := F[X])
                    (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 4) : F[X])
                        (HPow.hPow (α := F[X]) (β := ℕ) X 2) +
                      HMul.hMul (α := F[X]) (β := F[X])
                        ((C : (a : F) → F[X])
                            (HMul.hMul (α := F) 1 4 * x₁ + 1 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂)) :
                          F[X])
                        X)
                    ((C : (a : F) → F[X])
                        (HMul.hMul (α := F) 1 4 * HPow.hPow (β := ℕ) x₁ 2 +
                            1 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * x₁ +
                          HMul.hMul (α := F) 1 2 * (2 * W.a₄ + W.a₁ * W.a₃)) :
                      F[X]) *
                  HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
              F[X][Y]) +
          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]) (HPow.hPow (β := ℕ) (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) 2)) :
                F[X][Y])
              (0 : F[X][Y]))
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
              F[X][Y]) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (-4 : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁)) :
            F[X][Y])) =
    0
⊢ HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) 1) : F[X][Y])
            (Y -
              HSub.hSub (α := F[X][Y]) (β := F[X][Y]) (-Y)
                ((C : (a : F[X]) → F[X][Y])
                    (HAdd.hAdd (β := F[X]) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₁ : F[X]) X)
                      ((C : (a : F) → F[X]) W.a₃ : F[X])) :
                  F[X][Y])) *
          (Y -
            HSub.hSub (α := F[X][Y]) (β := F[X][Y]) (-Y)
              ((C : (a : F[X]) → F[X][Y])
                  (HAdd.hAdd (β := F[X]) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₁ : F[X]) X)
                    ((C : (a : F) → F[X]) W.a₃ : F[X])) :
                F[X][Y])) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (-4 : F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆)) :
            F[X][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]) (HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2)) : F[X][Y])
                (1 : F[X][Y]) +
              HMul.hMul (α := F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 4)) : F[X][Y])
                (HSub.hSub (β := F[X][Y])
                  (HPow.hPow (α := F[X][Y]) (β := ℕ) Y 2 +
                    HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                      ((C : (a : F[X]) → F[X][Y])
                          (HAdd.hAdd (β := F[X])
                            (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₁ : F[X]) X)
                            ((C : (a : F) → F[X]) W.a₃ : F[X])) :
                        F[X][Y])
                      Y)
                  ((C : (a : F[X]) → F[X][Y])
                      (HAdd.hAdd (β := F[X])
                        (HPow.hPow (α := F[X]) (β := ℕ) X 3 +
                            HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) W.a₂ : F[X])
                              (HPow.hPow (α := F[X]) (β := ℕ) X 2) +
                          HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₄ : F[X]) X)
                        ((C : (a : F) → F[X]) W.a₆ : F[X])) :
                    F[X][Y])))
            ((C : (a : F[X]) → F[X][Y])
                (HAdd.hAdd (β := F[X])
                    (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 4) : F[X])
                        (HPow.hPow (α := F[X]) (β := ℕ) X 2) +
                      HMul.hMul (α := F[X]) (β := F[X])
                        ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 4 * x₁ + 1 * b₂ W) : F[X]) X)
                    ((C : (a : F) → F[X])
                        (HMul.hMul (α := F) 1 4 * HPow.hPow (β := ℕ) x₁ 2 + 1 * b₂ W * x₁ +
                          HMul.hMul (α := F) 1 2 * b₄ W) :
                      F[X]) *
                  HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
              F[X][Y]) +
          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]) (HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2)) : F[X][Y])
              (0 : F[X][Y]))
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
              F[X][Y]) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (-4 : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁)) :
            F[X][Y])) =
    0

Tactic:
rw [b₂, b₄, negY]

Premises used: WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.Affine.negY