-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (XClass W x₂) * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
          span
            {HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
                  (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {HMul.hMul (α := W.CoordinateRing) (XClass W x₁) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {HMul.hMul (α := W.CoordinateRing) (YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) (XClass W x₂) *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
      (span
          (singleton (α := W.CoordinateRing)
            ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                  ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
              W.CoordinateRing)) ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
have rw : span
          {HMul.hMul (α := W.CoordinateRing) (β := 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]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
                W.CoordinateRing)
              ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                  (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                    ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
                W.CoordinateRing)} ⊔
        span
          {HMul.hMul (α := W.CoordinateRing) (β := 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]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
                  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]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
                  W.CoordinateRing) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing) (XClass W x₁)
              ((mk W : (a : F[X][Y]) → W.CoordinateRing)
                  (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
                    ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
                W.CoordinateRing) *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
    span
      {HMul.hMul (α := W.CoordinateRing) (β := 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]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
              W.CoordinateRing)
            (XClass W x₂) *
          XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
  HMul.hMul (α := Ideal W.CoordinateRing) (YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
    (span
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) W.negPolynomial
                ((C : (a : F[X]) → F[X][Y]) (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
            W.CoordinateRing)) ⊔
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Tactic: rw [← neg_eq_iff_eq_neg.mpr <| C_addPolynomial_slope h₁ h₂ hxy, span_singleton_neg,
    C_addPolynomial, map_mul, YClass]