-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem f_iUnion {s : ℕ → Set α} (h : ∀ i, IsCaratheodory m (s i)) (hd : Pairwise (Disjoint on s)) :
    m (⋃ i, s i) = ∑' i, m (s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x ∈ Finset.range n, m (s x) = m (⋃ i, ⋃ (_ : i < n), s i)
⊢ m (⋃ i, ⋃ (_ : i < n), s i) ≤ m (⋃ i, s i)

Tactic:
exact m.mono (iUnion₂_subset fun i _ => subset_iUnion _ i)

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ i ∈ Finset.range n, m (univ ∩ s i) = m (univ ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)

Tactic:
simp only [inter_comm, inter_univ, univ_inter] at this

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x ∈ Finset.range n, m (s x) = m (⋃ i, ⋃ (_ : i < n), s i)
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)

Tactic:
have := @isCaratheodory_sum _ m _ h hd univ n

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ i ∈ Finset.range n, m (univ ∩ s i) = m (univ ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x ∈ Finset.range n, m (s x) = m (⋃ i, ⋃ (_ : i < n), s i)
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)

Tactic:
simp only [this]

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x ∈ Finset.range n, m (s x) = m (⋃ i, ⋃ (_ : i < n), s i)
⊢ m (⋃ i, ⋃ (_ : i < n), s i) ≤ m (⋃ i, s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ m (⋃ i, s i) = ∑' (i : ℕ), m (s i)

Tactic:
refine le_antisymm (measure_iUnion_le s) ?_

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), m (s i) ≤ m (⋃ i, s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), m (s i) ≤ m (⋃ i, s i)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat]

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ ⨆ i, ∑ a ∈ Finset.range i, m (s a) ≤ m (⋃ i, s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ ⨆ i, ∑ a ∈ Finset.range i, m (s a) ≤ m (⋃ i, s i)

Tactic:
refine iSup_le fun n => ?_

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)