intro
| inl ⟨x, hs, h⟩ => refine ⟨x, inl hs, h⟩
| inr ⟨x, ht, h⟩ => refine ⟨x, inr ht, h⟩
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.18682
f : α → β
s t : Set α
y : β
⊢ y ∈ (Set.map f s).union (Set.map f t) → y ∈ Set.map f (s.union t)
no goals