apply Set.ext
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
⊢ Set.map f (s.union t) = (Set.map f s).union (Set.map f t)
case a
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
⊢ ∀ (x : β), x ∈ Set.map f (s.union t) ↔ x ∈ (Set.map f s).union (Set.map f t)