-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem isSigmaSubadditive_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)) :
    m.IsSigmaSubadditive

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
refine le_of_tendsto_of_tendsto' h_tendsto h_tendsto' fun _ ↦ ?_

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
x✝ : ℕ
⊢ m ((partialSups f) x✝) ≤ ∑ i ∈ Finset.range (x✝ + 1), m (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
x✝ : ℕ
⊢ m ((partialSups f) x✝) ≤ ∑ i ∈ Finset.range (x✝ + 1), m (f i)

Tactic:
rw [partialSups_eq_biUnion_range]

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
x✝ : ℕ
⊢ m (⋃ i ∈ Finset.range (x✝ + 1), f i) ≤ ∑ i ∈ Finset.range (x✝ + 1), m (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
⊢ Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))

Tactic:
rw [tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (f i))) 1]

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
⊢ Tendsto (fun k => ∑ i ∈ Finset.range k, m (f i)) atTop (𝓝 (∑' (i : ℕ), m (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ ⋃ i, (partialSups f) i ∈ C

Tactic:
rwa [← iSup_eq_iUnion, iSup_partialSups_eq]

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)
⊢ m.IsSigmaSubadditive

Tactic:
intro f hf hf_Union

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), m (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))

Tactic:
rw [← iSup_eq_iUnion, ← iSup_partialSups_eq]

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⨆ i, (partialSups 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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
have h_tendsto' : Tendsto (fun n ↦ ∑ i ∈ range (n + 1), m (f i)) atTop (𝓝 (∑' i, m (f i))) := by
  rw [tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (f i))) 1]
  exact ENNReal.tendsto_nat_tsum _

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), m (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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
h_tendsto' : Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))
x✝ : ℕ
⊢ m (⋃ i ∈ Finset.range (x✝ + 1), f i) ≤ ∑ i ∈ Finset.range (x✝ + 1), m (f i)

Tactic:
exact addContent_biUnion_le hC (fun _ _ ↦ hf _)

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 : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
⊢ Tendsto (fun k => ∑ i ∈ Finset.range k, m (f i)) atTop (𝓝 (∑' (i : ℕ), m (f i)))

Tactic:
exact ENNReal.tendsto_nat_tsum _

Result:
no goals