-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  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]) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
      HMul.hMul (α := 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])
        (HSub.hSub (α := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HAdd.hAdd (β := F[X])
                (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
            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)) =
    HMul.hMul (α := F[X][Y]) W.polynomial 1
h₁ :
  ∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]) (a_3 : F[X][Y]),
    a_3 *
        HSub.hSub (α := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HAdd.hAdd (β := F[X])
                (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
            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) =
      1 +
            HMul.hMul (β := F[X][Y]) a
              ((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]) +
          a_1 *
            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]) +
        a_2 *
          HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y])
⊢ Eq (α := Ideal F[X][Y])
    (span
      (insert (α := 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])
        {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]),
          HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]),
          HSub.hSub (α := F[X][Y])
            ((C : (a : F[X]) → F[X][Y])
                (HAdd.hAdd (β := F[X])
                  (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                  ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
              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)}))
    ⊤

Tactic:
simp_rw [eq_top_iff_one, mem_span_insert', mem_span_singleton']

Premises used: Ideal.mem_span_singleton', Ideal.eq_top_iff_one, Ideal.mem_span_insert'