-- 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:
α : 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 + 1), m (f i)) atTop (𝓝 (m (⋃ i, f i)))

Tactic:
rwa [ENNReal.tendsto_const_sub_nhds_zero_iff (hm_ne_top _ hUf) (fun n ↦ ?_)] at h_tendsto

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 : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), m (f i) ≤ 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
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)))

Tactic:
refine (Filter.tendsto_add_atTop_iff_nat 1).mp ?_

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 + 1), m (f i)) atTop (𝓝 (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
⊢ m (⋃ i, f i) = ∑' (i : ℕ), m (f i)

Tactic:
have hCs n : s n ∈ C := hC.diff_mem hUf (hC.accumulate_mem hf n)

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
⊢ m (⋃ i, f i) = ∑' (i : ℕ), m (f i)