-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem ofFunction_caratheodory {m : Set α → ℝ≥0∞} {s : Set α} {h₀ : m ∅ = 0}
    (hs : ∀ t, m (t ∩ s) + m (t \ s) ≤ m t) :
    MeasurableSet[(OuterMeasure.ofFunction m h₀).caratheodory] s

Proof state:
α : 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

Tactic:
refine fun t => le_iInf fun f => le_iInf fun hf => ?_

Result:
α : 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)

Proof state:
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)

Tactic:
exact ENNReal.tsum_le_tsum fun i => hs _

Result:
no goals

Proof state:
α : 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)

Tactic:
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 _ ?_))
    ?_

Result:
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)

Proof state:
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

Tactic:
rw [← iUnion_inter]

Result:
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

Proof state:
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

Tactic:
exact inter_subset_inter_left _ hf

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ MeasurableSet s

Tactic:
apply (isCaratheodory_iff_le _).mpr

Result:
α : 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

Proof state:
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)

Tactic:
rw [← ENNReal.tsum_add]

Result:
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)

Proof state:
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

Tactic:
rw [← iUnion_diff]

Result:
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

Proof state:
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

Tactic:
exact diff_subset_diff_left hf

Result:
no goals