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

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n : ℕ
⊢ m (t \ ⋃ i, s i) ≤ m (t \ ⋃ i, ⋃ (_ : i < n), s i)

Tactic:
refine m.mono (diff_subset_diff_right ?_)

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n : ℕ
⊢ ⋃ i, ⋃ (_ : i < n), s i ⊆ ⋃ i, s i

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ ⨆ i, m (t ∩ ⋃ i_1, ⋃ (_ : i_1 < i), s i_1) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
refine iSup_le fun n => le_trans (add_le_add_left ?_ _)
  (ge_of_eq (isCaratheodory_iUnion_lt m (fun i _ => h i) _))

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n : ℕ
⊢ m (t \ ⋃ i, s i) ≤ m (t \ ⋃ i, ⋃ (_ : i < n), s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ (⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
rw [ENNReal.iSup_add]

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ ⨆ i, m (t ∩ ⋃ i_1, ⋃ (_ : i_1 < i), s i_1) + m (t \ ⋃ i, s i) ≤ m t

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

Tactic:
intro t

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

Proof state:
case h.e'_4
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) = ∑' (i : ℕ), m (t ∩ s i)

Tactic:
simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n : ℕ
⊢ ⋃ i, ⋃ (_ : i < n), s i ⊆ ⋃ i, s i

Tactic:
exact 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)
⊢ m.IsCaratheodory (⋃ i, s i)

Tactic:
apply (isCaratheodory_iff_le' m).mpr

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

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

Tactic:
simp [inter_iUnion]

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ m (t ∩ ⋃ i, s i) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
refine le_trans (add_le_add_right hp _) ?_

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ (⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)) + m (t \ ⋃ i, s i) ≤ m t

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)

Tactic:
convert measure_iUnion_le (μ := m) fun i => t ∩ s i using 1

Result:
case h.e'_3
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ m (t ∩ ⋃ i, s i) = m (⋃ i, t ∩ s i)

case h.e'_4
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) = ∑' (i : ℕ), m (t ∩ s i)