no goals
α : Type u_1
β : Type u_2
γ : Type ?u.29829
ι : Sort ?u.29832
ι' : Sort ?u.29835
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' (s ∪ t) → x ∈ f '' s ∪ f '' t
rintro ⟨a, h | h, rfl⟩ <;> [left; right] <;> exact ⟨_, h, rfl⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.29829
ι : Sort ?u.29832
ι' : Sort ?u.29835
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' s ∪ f '' t → x ∈ f '' (s ∪ t)
rintro (⟨a, h, rfl⟩ | ⟨a, h, rfl⟩) <;> refine' ⟨_, _, rfl⟩ <;> [left; right] <;> exact h