α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)
symm
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
cases' eq_empty_or_nonempty (s ×ˢ t) with h h
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
rw [prod_eq_prod_iff_of_nonempty h]
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
rw [nonempty_iff_ne_empty, Ne.def, prod_eq_empty_iff] at h
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
simp_rw [h, false_and_iff, or_false_iff]
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and_iff,
  or_iff_right_iff_imp]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₂ : Set α
t t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = ∅ ∨ t = ∅
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅
rintro ⟨rfl, rfl⟩
no goals
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.88795
δ : Type ?u.88798
s s₂ : Set α
t t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = ∅ ∨ t = ∅
exact prod_eq_empty_iff.mp h