no goals
α : Type u_2
β : Type u_1
γ : Type ?u.187796
ι : Type ?u.187799
M : Type u_3
M' : Type ?u.187805
N : Type ?u.187808
P : Type ?u.187811
G : Type ?u.187814
H : Type ?u.187817
R : Type ?u.187820
S : Type ?u.187823
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
⊢ (Finset.biUnion s.support fun a => {f a}) ⊆ image f s.support
rw [Finset.biUnion_singleton]