case hd
ι : Type ?u.12592
α : Type u_1
β : Type ?u.12598
γ : Type ?u.12601
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b => bif b then s else t)

case h
ι : Type ?u.12592
α : Type u_1
β : Type ?u.12598
γ : Type ?u.12601
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t)
ι : Type ?u.12592
α : Type u_1
β : Type ?u.12598
γ : Type ?u.12601
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]
no goals
case hd
ι : Type ?u.12592
α : Type u_1
β : Type ?u.12598
γ : Type ?u.12601
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b => bif b then s else t)

case h
ι : Type ?u.12592
α : Type u_1
β : Type ?u.12598
γ : Type ?u.12601
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t)
exacts [(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs]