case hs
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ ∀ (t : Set α),
    ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ MeasurableSet s
apply ofFunction_caratheodory
case hs
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t
case hs
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ ∀ (t : Set α),
    ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t
intro t
case hs.inl
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t = ∅
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t

case hs.inr
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : Set.Nonempty t
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t
case hs
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t
cases' t.eq_empty_or_nonempty with h h
no goals
case hs.inl
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t = ∅
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t
simp [h, Set.not_nonempty_empty]
case h.e'_4
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : Set.Nonempty t
⊢ (⨆ (_ : Set.Nonempty t), m t) = m t

case hs.inr.convert_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : Set.Nonempty t
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ m (t ∩ s) + m (t \ s)
case hs.inr
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : Set.Nonempty t
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ ⨆ (_ : Set.Nonempty t), m t
convert le_trans _ (hs t)
no goals
case hs.inr.convert_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : Set.Nonempty t
⊢ ((⨆ (_ : Set.Nonempty (t ∩ s)), m (t ∩ s)) + ⨆ (_ : Set.Nonempty (t \ s)), m (t \ s)) ≤ m (t ∩ s) + m (t \ s)
exact add_le_add iSup_const_le iSup_const_le
no goals
case h.e'_4
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : Set.Nonempty t
⊢ (⨆ (_ : Set.Nonempty t), m t) = m t
simp [h]