case hf₁
α : Type u_1
β : Type ?u.20634
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)

case hf₂
α : Type u_1
β : Type ?u.20634
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ Pairwise (Disjoint on fun b => bif b then A else B)
α : Type u_1
β : Type ?u.20634
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ↑v (A ∪ B) = ↑v A + ↑v B
rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]
no goals
case hf₁
α : Type u_1
β : Type ?u.20634
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)

case hf₂
α : Type u_1
β : Type ?u.20634
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ Pairwise (Disjoint on fun b => bif b then A else B)
exacts [fun b => Bool.casesOn b hB hA, pairwise_disjoint_on_bool.2 h]