case h
α : Type u_1
β : Type u_2
γ : Type ?u.6671
δ : Type ?u.6674
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅
α : Type u_1
β : Type u_2
γ : Type ?u.6671
δ : Type ?u.6674
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ ∅ = ∅
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.6671
δ : Type ?u.6674
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅
exact and_false_iff _