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