no goals
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z : R
⊢ span {x, y + x * z} = span {x, y}
rw [span_pair_comm, span_pair_add_mul_left, span_pair_comm]