α : Type u_2
β : Type u_1
γ : Type ?u.90755
δ : Type ?u.90758
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ s = ∅ ∧ s₁ = ∅ → s = s₁
α : Type u_2
β : Type u_1
γ : Type ?u.90755
δ : Type ?u.90758
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁
simp_rw [prod_eq_prod_iff, ht.ne_empty, and_true_iff, or_iff_left_iff_imp,
  or_false_iff]
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.90755
δ : Type ?u.90758
s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ ∅ = ∅
α : Type u_2
β : Type u_1
γ : Type ?u.90755
δ : Type ?u.90758
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ s = ∅ ∧ s₁ = ∅ → s = s₁
rintro ⟨rfl, rfl⟩
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.90755
δ : Type ?u.90758
s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ ∅ = ∅
rfl