-- 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₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Eq (α := Ideal W.CoordinateRing)
    (span
      (insert (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
          W.CoordinateRing)
        (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])
                    ((C : (a : F) → F[X])
                      (eval x₂
                        (HAdd.hAdd (β := F[X])
                          (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                          ((C : (a : F) → F[X]) y₁ : F[X])))) :
                  F[X][Y])) :
            W.CoordinateRing))))
    (span
      (insert (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
          W.CoordinateRing)
        (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])
                    (HAdd.hAdd (β := F[X])
                      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                      ((C : (a : F) → F[X]) y₁ : F[X])) :
                  F[X][Y])) :
            W.CoordinateRing))))
have rw : Eq (α := Ideal W.CoordinateRing)
  (span
    (insert (α := W.CoordinateRing)
      ((mk W : (a : F[X][Y]) → W.CoordinateRing)
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
        W.CoordinateRing)
      (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])
                    ((C : (a : F) → F[X])
                      (eval x₂
                        (HAdd.hAdd (β := F[X])
                          (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                          ((C : (a : F) → F[X]) y₁ : F[X])))) :
                  F[X][Y]) +
              HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                  F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (-W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
          W.CoordinateRing))))
  (span
    (insert (α := W.CoordinateRing)
      ((mk W : (a : F[X][Y]) → W.CoordinateRing)
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
        W.CoordinateRing)
      (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])
                  (HAdd.hAdd (β := F[X])
                    (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                      (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                    ((C : (a : F) → F[X]) y₁ : F[X])) :
                F[X][Y])) :
          W.CoordinateRing))))
Tactic: rw [← span_pair_add_left_mul _ _ <| mk W <| C <| C <| -W.slope x₁ x₂ y₁ y₂, ← map_mul, ← map_add]