f : StieltjesFunction
c : ℝ
t : Set ℝ
⊢ length f (t ∩ Ioi c) + length f (t \ Ioi c) ≤ length f t
f : StieltjesFunction
c : ℝ
⊢ MeasurableSet (Ioi c)
refine OuterMeasure.ofFunction_caratheodory fun t => ?_
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ length f (t ∩ Ioi c) + length f (t \ Ioi c) ≤ ofReal (↑f b - ↑f a)
f : StieltjesFunction
c : ℝ
t : Set ℝ
⊢ length f (t ∩ Ioi c) + length f (t \ Ioi c) ≤ length f t
refine' le_iInf fun a => le_iInf fun b => le_iInf fun h => _
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ length f (t ∩ Ioi c) + length f (t \ Ioi c) ≤ ofReal (↑f b - ↑f a)
refine'
  le_trans
    (add_le_add (f.length_mono <| inter_subset_inter_left _ h)
      (f.length_mono <| diff_subset_diff_left h)) _
case inl.inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
hbc : b ≤ c
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

case inl.inr
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
hbc : c ≤ b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

case inr.inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : c ≤ a
hbc : b ≤ c
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

case inr.inr
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : c ≤ a
hbc : c ≤ b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
cases' le_total a c with hac hac <;> cases' le_total b c with hbc hbc
no goals
case inl.inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
hbc : b ≤ c
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
simp only [Ioc_inter_Ioi, f.length_Ioc, hac, _root_.sup_eq_max, hbc, le_refl, Ioc_eq_empty,
  max_eq_right, min_eq_left, Ioc_diff_Ioi, f.length_empty, zero_add, not_lt]
no goals
case inl.inr
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
hbc : c ≤ b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right,
  _root_.sup_eq_max, ← ENNReal.ofReal_add, f.mono hac, f.mono hbc, sub_nonneg,
  sub_add_sub_cancel, le_refl,
  max_eq_right]
no goals
case inr.inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : c ≤ a
hbc : b ≤ c
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
simp only [hbc, le_refl, Ioc_eq_empty, Ioc_inter_Ioi, min_eq_left, Ioc_diff_Ioi, f.length_empty,
  zero_add, or_true_iff, le_sup_iff, f.length_Ioc, not_lt]
no goals
case inr.inr
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : c ≤ a
hbc : c ≤ b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right, _root_.sup_eq_max,
  le_refl, Ioc_eq_empty, add_zero, max_eq_left, f.length_empty, not_lt]