case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type ?u.11366
γ : Type ?u.11369
m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i)
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᵐ[μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
ι : Type u_1
α : Type u_2
β : Type ?u.11366
γ : Type ?u.11369
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩
no goals
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type ?u.11366
γ : Type ?u.11369
m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i)
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᵐ[μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
calc
  μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (EventuallyEq.countable_iUnion ht_eq)
  _ = ∑' i, μ (t i) := (measure_iUnion htd htm)
  _ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm