case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.83491
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (f x, g x)) x ∈ (f '' s) ×ˢ (g '' s)
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.83491
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
s : Set α
⊢ (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)
rintro _ ⟨x, hx, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.83491
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (f x, g x)) x ∈ (f '' s) ×ˢ (g '' s)
exact mk_mem_prod (mem_image_of_mem f hx) (mem_image_of_mem g hx)