-- 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) (β := 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₂))})
have simp_rw : span
      (singleton (α := 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)) *
    (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)) ⊔
          HMul.hMul (α := Ideal W.CoordinateRing)
            (span
              (singleton (α := 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)))
            (span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) ⊔
        HMul.hMul (α := Ideal W.CoordinateRing) (span {XClass W x₁})
          (span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) ⊔
      HMul.hMul (α := Ideal W.CoordinateRing) (span {XClass W x₂})
        (span {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: simp_rw [mul_comm <| XClass W x₁, mul_assoc, ← span_singleton_mul_span_singleton, ← Ideal.mul_sup]