no goals
α : Type u_1
β : Type u_2
γ : Type ?u.37468
f✝ : α ↪ β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
s₁ s₂ : Finset α
⊢ ↑(map f (s₁ ∪ s₂)) = ↑(map f s₁ ∪ map f s₂)
simp only [coe_map, coe_union, Set.image_union]