no goals
α : Type u_2
β : Type u_1
γ : Type ?u.122048
inst✝ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a : α
b c : β
f : α → β
x : β
⊢ (x ∈ Finset.biUnion s fun a => {f a}) ↔ x ∈ image f s
simp only [mem_biUnion, mem_image, mem_singleton, eq_comm]