-- 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
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₂))})
⊢ 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₂))})

Tactic:
rw [← neg_eq_iff_eq_neg.mpr <| C_addPolynomial_slope h₁ h₂ hxy, span_singleton_neg,
    C_addPolynomial, map_mul, YClass]

Premises used: Iff.mpr, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, neg_eq_iff_eq_neg, map_mul, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope, WeierstrassCurve.Affine.CoordinateRing.YClass, Ideal.span_singleton_neg