-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ Eq (α := Ideal W'.CoordinateRing)
    (span
      (insert (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            ((C : (a : R[X]) → R[X][Y])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
          W'.CoordinateRing)
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
                ((C : (a : R[X]) → R[X][Y])
                    ((C : (a : R) → R[X]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
                  R[X][Y])) :
            W'.CoordinateRing))))
    (span
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (β := R[X][Y])
                (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
                  ((C : (a : R[X]) → R[X][Y])
                      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                        ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
                    R[X][Y]))
                ((C : (a : R[X]) → R[X][Y])
                    (HAdd.hAdd (β := R[X])
                      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
                        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X])))
                      ((C : (a : R) → R[X]) y₁ : R[X])) :
                  R[X][Y])) :
            W'.CoordinateRing)) ⊔
      span
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              ((C : (a : R[X]) → R[X][Y])
                (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
            W'.CoordinateRing)))
have rw : Eq (α := Ideal W'.CoordinateRing)
  (span
    (insert (α := W'.CoordinateRing)
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
          ((C : (a : R[X]) → R[X][Y])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
        W'.CoordinateRing)
      (singleton (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
                ((C : (a : R[X]) → R[X][Y])
                    ((C : (a : R) → R[X]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
                  R[X][Y]) +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y])
                    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X])) :
                  R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.a₁ + ℓ)) : R[X][Y])) :
          W'.CoordinateRing))))
  (span
    (insert (α := W'.CoordinateRing)
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
          ((C : (a : R[X]) → R[X][Y])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
        W'.CoordinateRing)
      (singleton (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            (HAdd.hAdd (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y])
                    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                      ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
                  R[X][Y])
                ((C : (a : R[X]) → R[X][Y])
                    (HAdd.hAdd (β := R[X])
                      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
                        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X])))
                      ((C : (a : R) → R[X]) y₁ : R[X])) :
                  R[X][Y]) +
              Y) :
          W'.CoordinateRing))))
Tactic: rw [sub_sub <| -(Y : R[X][Y]), neg_sub_left (Y : R[X][Y]), map_neg, span_singleton_neg, sup_comm,
    ← span_insert, ← span_pair_add_left_mul _ _ <| mk W' <| C <| C <| W'.a₁ + ℓ, ← map_mul,
    ← map_add]