case inl
α : Type u_1
β : Type ?u.9604
γ : Type ?u.9607
δ : Type ?u.9610
δ' : Type ?u.9613
ι : Sort ?u.9616
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : p
⊢ MeasurableSet s

case inr
α : Type u_1
β : Type ?u.9604
γ : Type ?u.9607
δ : Type ?u.9610
δ' : Type ?u.9613
ι : Sort ?u.9616
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : ¬p
⊢ MeasurableSet t
α : Type u_1
β : Type ?u.9604
γ : Type ?u.9607
δ : Type ?u.9610
δ' : Type ?u.9613
ι : Sort ?u.9616
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
⊢ MeasurableSet (if p then s else t)
split_ifs with h
no goals
case inl
α : Type u_1
β : Type ?u.9604
γ : Type ?u.9607
δ : Type ?u.9610
δ' : Type ?u.9613
ι : Sort ?u.9616
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : p
⊢ MeasurableSet s

case inr
α : Type u_1
β : Type ?u.9604
γ : Type ?u.9607
δ : Type ?u.9610
δ' : Type ?u.9613
ι : Sort ?u.9616
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : ¬p
⊢ MeasurableSet t
exacts [hs h, ht h]