rw [asSet] at in_set
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ asSet l
⊢ y ∈ span { x | x ∈ l }
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ span { x | x ∈ l }