α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ ∀ (t : Set α),
    ↑(OuterMeasure.ofFunction m h₀) (t ∩ s) + ↑(OuterMeasure.ofFunction m h₀) (t \ s) ≤
      ↑(OuterMeasure.ofFunction m h₀) t
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ MeasurableSet s
apply (isCaratheodory_iff_le _).mpr
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ ↑(OuterMeasure.ofFunction m h₀) (t ∩ s) + ↑(OuterMeasure.ofFunction m h₀) (t \ s) ≤ ∑' (i : ℕ), m (f i)
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ ∀ (t : Set α),
    ↑(OuterMeasure.ofFunction m h₀) (t ∩ s) + ↑(OuterMeasure.ofFunction m h₀) (t \ s) ≤
      ↑(OuterMeasure.ofFunction m h₀) t
refine' fun t => le_iInf fun f => le_iInf fun hf => _
case refine'_1
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t ∩ s ⊆ ⋃ (i : ℕ), (fun i => f i ∩ s) i

case refine'_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t \ s ⊆ ⋃ (i : ℕ), (fun i => f i \ s) i

case refine'_3
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ ((∑' (i : ℕ), m ((fun i => f i ∩ s) i)) + ∑' (i : ℕ), m ((fun i => f i \ s) i)) ≤ ∑' (i : ℕ), m (f i)
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ ↑(OuterMeasure.ofFunction m h₀) (t ∩ s) + ↑(OuterMeasure.ofFunction m h₀) (t \ s) ≤ ∑' (i : ℕ), m (f i)
refine'
  le_trans
    (add_le_add ((iInf_le_of_le fun i => f i ∩ s) <| iInf_le _ _)
      ((iInf_le_of_le fun i => f i \ s) <| iInf_le _ _))
    _
case refine'_1
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t ∩ s ⊆ (⋃ (i : ℕ), f i) ∩ s
case refine'_1
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t ∩ s ⊆ ⋃ (i : ℕ), (fun i => f i ∩ s) i
rw [← iUnion_inter]
no goals
case refine'_1
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t ∩ s ⊆ (⋃ (i : ℕ), f i) ∩ s
exact inter_subset_inter_left _ hf
case refine'_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t \ s ⊆ (⋃ (i : ℕ), f i) \ s
case refine'_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t \ s ⊆ ⋃ (i : ℕ), (fun i => f i \ s) i
rw [← iUnion_diff]
no goals
case refine'_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t \ s ⊆ (⋃ (i : ℕ), f i) \ s
exact diff_subset_diff_left hf
case refine'_3
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ (∑' (a : ℕ), m ((fun i => f i ∩ s) a) + m ((fun i => f i \ s) a)) ≤ ∑' (i : ℕ), m (f i)
case refine'_3
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ ((∑' (i : ℕ), m ((fun i => f i ∩ s) i)) + ∑' (i : ℕ), m ((fun i => f i \ s) i)) ≤ ∑' (i : ℕ), m (f i)
rw [← ENNReal.tsum_add]
no goals
case refine'_3
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ (∑' (a : ℕ), m ((fun i => f i ∩ s) a) + m ((fun i => f i \ s) a)) ≤ ∑' (i : ℕ), m (f i)
exact ENNReal.tsum_le_tsum fun i => hs _