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

Tactic:
let s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ Set.Accumulate f 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
⊢ 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
h_tendsto : Tendsto (fun n => m (s n)) atTop (𝓝 0)
hmsn : ∀ (n : ℕ), m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
⊢ m (⋃ i, f i) = ∑' (i : ℕ), m (f i)

Tactic:
simp_rw [hmsn] 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)
⊢ 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
h_tendsto : Tendsto (fun n => m (s n)) atTop (𝓝 0)
⊢ m (⋃ i, f i) = ∑' (i : ℕ), m (f i)

Tactic:
have hmsn n : m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i) := by
  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:
α : 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)
hmsn : ∀ (n : ℕ), m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
⊢ m (⋃ i, f i) = ∑' (i : ℕ), m (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
⊢ Antitone s

Tactic:
intro i j hij x 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 ∈ s j
⊢ x ∈ s 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
⊢ (⋃ i, f i) ∩ (⋃ x, f x)ᶜ = ∅

Tactic:
exact Set.inter_compl_self _

Result:
no goals

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 ∈ ⋃ i, f i ∧ x ∉ Accumulate f j
⊢ x ∈ ⋃ i, f i ∧ x ∉ Accumulate f i

Tactic:
exact ⟨hxj.1, fun hxi ↦ hxj.2 (Set.monotone_accumulate hij hxi)⟩

Result:
no goals

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, (⋃ i, f i) ∩ (Accumulate f n)ᶜ = ∅

Tactic:
rw [Set.iInter_inter_distrib, Set.iInter_const, ← Set.compl_iUnion, Set.iUnion_accumulate]

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
⊢ (⋃ i, f i) ∩ (⋃ x, f x)ᶜ = ∅

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 : ℕ
⊢ m (Accumulate f n) ≤ m (⋃ i, f i)

Tactic:
exact addContent_mono hC.isSetSemiring (hC.accumulate_mem hf n) hUf
  (Set.accumulate_subset_iUnion _)

Result:
no goals