case inl
α : Type u_1
β : Type u_2
γ : Type ?u.84459
δ : Type ?u.84462
δ' : Type ?u.84465
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.84459
δ : Type ?u.84462
δ' : Type ?u.84465
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
α : Type u_1
β : Type u_2
γ : Type ?u.84459
δ : Type ?u.84462
δ' : Type ?u.84465
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
cases' (s ×ˢ t).eq_empty_or_nonempty with h h
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.84459
δ : Type ?u.84462
δ' : Type ?u.84465
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
simp [h, prod_eq_empty_iff.mp h]
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.84459
δ : Type ?u.84462
δ' : Type ?u.84465
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]