-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
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]) 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]) y) : 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]) x : R[X])) :
                    R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (-ℓ)) : 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]) 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])
                    (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))))
⊢ 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]) 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]) y) : 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]) 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])
                    (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))))

Tactic:
rw [← span_pair_add_left_mul _ _ <| mk W' <| C <| C <| -ℓ, ← map_mul, ← map_add]

Premises used: Polynomial.C, WeierstrassCurve.Affine.CoordinateRing.mk, Ideal.span_pair_add_left_mul, map_add, map_mul