-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum (hC : IsSetRing C)
    (m_iUnion : ∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : (⋃ i, f i) ∈ C)
      (_hf_disj : Pairwise (Disjoint on f)), m (⋃ i, f i) = ∑' i, m (f i))
    ⦃f : ℕ → Set α⦄ (hf_mono : Monotone f) (hf : ∀ i, f i ∈ C) (hf_Union : ⋃ i, f i ∈ C) :
    Tendsto (fun n ↦ m (f n)) atTop (𝓝 (m (⋃ i, f i)))

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ Tendsto (fun n => m (f n)) atTop (𝓝 (m (⋃ i, f i)))

Tactic:
rw [← iUnion_disjointed, m_iUnion _ (hC.disjointed_mem hf) (by rwa [iUnion_disjointed])
    (disjoint_disjointed f)]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ Tendsto (fun n => m (f n)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ ⋃ i, disjointed f i ∈ C

Tactic:
rwa [iUnion_disjointed]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ Tendsto (fun n => m (f n)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Tactic:
have h n : m (f n) = ∑ i ∈ range (n + 1), m (disjointed f i) := by
  nth_rw 1 [← addContent_accumulate _ hC (disjoint_disjointed f) (hC.disjointed_mem hf),
  ← hf_mono.partialSups_eq, ← partialSups_disjointed, partialSups_eq_biSup, Accumulate]
  rfl

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun n => m (f n)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
n : ℕ
⊢ m (⨆ j, ⨆ (_ : j ≤ n), disjointed f j) = m (⋃ y, ⋃ (_ : y ≤ n), disjointed f y)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun k => ∑ i ∈ Finset.range k, m (disjointed f i)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Tactic:
exact ENNReal.tendsto_nat_tsum _

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
n : ℕ
⊢ m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)

Tactic:
nth_rw 1 [← addContent_accumulate _ hC (disjoint_disjointed f) (hC.disjointed_mem hf),
← hf_mono.partialSups_eq, ← partialSups_disjointed, partialSups_eq_biSup, Accumulate]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
n : ℕ
⊢ m (⨆ j, ⨆ (_ : j ≤ n), disjointed f j) = m (⋃ y, ⋃ (_ : y ≤ n), disjointed f y)

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (disjointed f i)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Tactic:
refine (tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (disjointed f i))) 1).2 ?_

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun k => ∑ i ∈ Finset.range k, m (disjointed f i)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun n => m (f n)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))

Tactic:
simp_rw [h]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h : ∀ (n : ℕ), m (f n) = ∑ i ∈ Finset.range (n + 1), m (disjointed f i)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (disjointed f i)) atTop (𝓝 (∑' (i : ℕ), m (disjointed f i)))