α : Type u_1
β : Type u_2
γ : Type ?u.28925
ι : Sort ?u.28928
ι' : Sort ?u.28931
f✝ : α → β
s t a b : Set α
f : α → β
h : a ⊆ b
⊢ ∀ (x : β), (∃ x_1, x_1 ∈ a ∧ f x_1 = x) → ∃ x_1, x_1 ∈ b ∧ f x_1 = x
α : Type u_1
β : Type u_2
γ : Type ?u.28925
ι : Sort ?u.28928
ι' : Sort ?u.28931
f✝ : α → β
s t a b : Set α
f : α → β
h : a ⊆ b
⊢ f '' a ⊆ f '' b
simp only [subset_def, mem_image]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.28925
ι : Sort ?u.28928
ι' : Sort ?u.28931
f✝ : α → β
s t a b : Set α
f : α → β
h : a ⊆ b
⊢ ∀ (x : β), (∃ x_1, x_1 ∈ a ∧ f x_1 = x) → ∃ x_1, x_1 ∈ b ∧ f x_1 = x
exact fun x => fun ⟨w, h1, h2⟩ => ⟨w, h h1, h2⟩