-- 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
        (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₂))})
have 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 {XClass W x₁} ⊔
          (span {XClass W x₂} ⊔
            span
              (singleton (α := W.CoordinateRing)
                ((mk W : (a : F[X][Y]) → W.CoordinateRing) (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) :
                  W.CoordinateRing))))
        (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: rw [span_singleton_mul_span_singleton, ← span_insert,
    ← span_pair_add_left_mul _ _ <| -(XClass W <| W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂), mul_neg,
    ← sub_eq_add_neg, ← sub_mul, ← map_sub <| mk W, sub_sub_sub_cancel_right, span_insert,
    ← span_singleton_mul_span_singleton, ← sup_rw, ← Ideal.sup_mul, ← Ideal.sup_mul]