simp [hx]
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ {f x} ⊆ Finset.map f v.support
no goals