case false
α : Type u_1
β : Type ?u.10031
γ : Type ?u.10034
δ : Type ?u.10037
δ' : Type ?u.10040
ι : Sort ?u.10043
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)

case true
α : Type u_1
β : Type ?u.10031
γ : Type ?u.10034
δ : Type ?u.10037
δ' : Type ?u.10040
ι : Sort ?u.10043
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif true then s₁ else s₂)
α : Type u_1
β : Type ?u.10031
γ : Type ?u.10034
δ : Type ?u.10037
δ' : Type ?u.10040
ι : Sort ?u.10043
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
⊢ MeasurableSet (bif i then s₁ else s₂)
cases i
no goals
case false
α : Type u_1
β : Type ?u.10031
γ : Type ?u.10034
δ : Type ?u.10037
δ' : Type ?u.10040
ι : Sort ?u.10043
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)

case true
α : Type u_1
β : Type ?u.10031
γ : Type ?u.10034
δ : Type ?u.10037
δ' : Type ?u.10040
ι : Sort ?u.10043
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif true then s₁ else s₂)
exacts [h₂, h₁]