-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₁ :
  Eq (α := Ideal W.CoordinateRing)
    (span
      (insert (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
          W.CoordinateRing)
        (insert (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              (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])) :
            W.CoordinateRing)
          (insert (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                (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])) :
              W.CoordinateRing)
            (singleton (α := W.CoordinateRing)
              ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
                  (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)) :
                AdjoinRoot (R := F[X]) W.polynomial))))))
    ⊤
⊢ HMul.hMul (α := Ideal W.CoordinateRing)
      (span
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
            W.CoordinateRing)))
      (span
        (insert (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
            W.CoordinateRing)
          (insert (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                (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])) :
              W.CoordinateRing)
            (insert (α := W.CoordinateRing)
              ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                  (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])) :
                W.CoordinateRing)
              (singleton (α := W.CoordinateRing)
                ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
                    (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)) :
                  AdjoinRoot (R := F[X]) W.polynomial)))))) =
    XIdeal W x
have convert_2 : IsTwoSided (α := W.CoordinateRing)
  (span
    (singleton (α := W.CoordinateRing)
      ((mk W : (a : F[X][Y]) → W.CoordinateRing)
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
        W.CoordinateRing)))
Tactic: convert! mul_top (_ : Ideal W.CoordinateRing) using 2