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