-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
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₂))})
⊢ 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:
simp_rw [mul_comm <| XClass W x₁, mul_assoc, ← span_singleton_mul_span_singleton, ← Ideal.mul_sup]

Premises used: mul_assoc, Ideal.mul_sup, Ideal.span_singleton_mul_span_singleton, WeierstrassCurve.Affine.CoordinateRing.XClass, mul_comm