case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.83787
δ : Type ?u.83790
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
hb : b ∈ t
a : α
ha : a ∈ s
⊢ (fun a => (a, b)) a ∈ s ×ˢ t
α : Type u_2
β : Type u_1
γ : Type ?u.83787
δ : Type ?u.83790
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
hb : b ∈ t
⊢ (fun a => (a, b)) '' s ⊆ s ×ˢ t
rintro _ ⟨a, ha, rfl⟩
no goals
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.83787
δ : Type ?u.83790
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
hb : b ∈ t
a : α
ha : a ∈ s
⊢ (fun a => (a, b)) a ∈ s ×ˢ t
exact ⟨ha, hb⟩