-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem addContent_iUnion_eq_sum_of_tendsto_zero (hC : IsSetRing C) (m : AddContent C)
    (hm_ne_top : ∀ s ∈ C, m s ≠ ∞)
    (hm_tendsto : ∀ ⦃s : ℕ → Set α⦄ (_ : ∀ n, s n ∈ C),
      Antitone s → (⋂ n, s n) = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0))
    ⦃f : ℕ → Set α⦄ (hf : ∀ i, f i ∈ C) (hUf : (⋃ i, f i) ∈ C)
    (h_disj : Pairwise (Disjoint on f)) :
    m (⋃ i, f i) = ∑' i, m (f i)

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ ⋂ n, s n = ∅

Tactic:
simp_rw [s, Set.diff_eq]

Result:
case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ ⋂ n, (⋃ i, f i) ∩ (Accumulate f n)ᶜ = ∅

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn : ∀ (n : ℕ), m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
h_tendsto : Tendsto (fun n => m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 0)
⊢ m (⋃ i, f i) = ∑' (i : ℕ), m (f i)

Tactic:
refine tendsto_nhds_unique ?_ (ENNReal.tendsto_nat_tsum fun i ↦ m (f i))

Result:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn : ∀ (n : ℕ), m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
h_tendsto : Tendsto (fun n => m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 0)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, m (f i)) atTop (𝓝 (m (⋃ i, f i)))

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
i j : ℕ
hij : i ≤ j
x : α
hxj : x ∈ s j
⊢ x ∈ s i

Tactic:
rw [Set.mem_diff] at hxj ⊢

Result:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
i j : ℕ
hij : i ≤ j
x : α
hxj : x ∈ ⋃ i, f i ∧ x ∉ Accumulate f j
⊢ x ∈ ⋃ i, f i ∧ x ∉ Accumulate f i

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn : ∀ (n : ℕ), m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
h_tendsto : Tendsto (fun n => m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 0)
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), m (f i) ≤ m (⋃ i, f i)

Tactic:
rw [← addContent_accumulate m hC h_disj hf]

Result:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
hmsn : ∀ (n : ℕ), m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
h_tendsto : Tendsto (fun n => m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 0)
n : ℕ
⊢ m (Accumulate f n) ≤ m (⋃ i, f i)

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Tendsto (fun n => m (s n)) atTop (𝓝 0)

Tactic:
refine hm_tendsto hCs ?_ ?_

Result:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Antitone s

case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ ⋂ n, s n = ∅

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n => m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n => (⋃ i, f i) \ Accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (fun n => m (s n)) atTop (𝓝 0)
n : ℕ
⊢ m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)

Tactic:
rw [addContent_diff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n)
  (Set.accumulate_subset_iUnion _), addContent_accumulate m hC h_disj hf n]

Result:
no goals