no goals
α : Type u_1
β : Type u_2
γ : Type ?u.85521
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s₁ s₂ : Finset α
x✝ : β
⊢ x✝ ∈ image f (s₁ ∪ s₂) ↔ x✝ ∈ image f s₁ ∪ image f s₂
simp only [mem_image, mem_union, exists_prop, or_and_right, exists_or]