-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measurableSet_Ioi {c : ℝ} : MeasurableSet[f.outer.caratheodory] (Ioi c)

Proof state:
f : StieltjesFunction
c : ℝ
⊢ MeasurableSet (Ioi c)

Tactic:
refine OuterMeasure.ofFunction_caratheodory fun t => ?_

Result:
f : StieltjesFunction
c : ℝ
t : Set ℝ
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ f.length t

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

Tactic:
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right,
  le_refl, Ioc_eq_empty, add_zero, max_eq_left, f.length_empty, not_lt]

Result:
no goals

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

Tactic:
simp only [Ioc_inter_Ioi, f.length_Ioc, hac, hbc, le_refl, Ioc_eq_empty,
  max_eq_right, min_eq_left, Ioc_diff_Ioi, f.length_empty, zero_add, not_lt]

Result:
no goals

Proof state:
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal (↑f b - ↑f a)

Tactic:
refine
  le_trans
    (add_le_add (f.length_mono <| inter_subset_inter_left _ h)
      (f.length_mono <| diff_subset_diff_left h)) ?_

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

Proof state:
f : StieltjesFunction
c : ℝ
t : Set ℝ
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ f.length t

Tactic:
refine le_iInf fun a => le_iInf fun b => le_iInf fun h => ?_

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

Proof state:
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

Tactic:
rcases le_total a c with hac | hac <;> rcases le_total b c with hbc | hbc

Result:
case inl.inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
hbc : b ≤ c
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (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
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (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
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (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
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

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

Tactic:
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right,
  ← ENNReal.ofReal_add, f.mono hac, f.mono hbc, sub_nonneg,
  sub_add_sub_cancel, le_refl,
  max_eq_right]

Result:
no goals

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

Tactic:
simp only [hbc, le_refl, Ioc_eq_empty, Ioc_inter_Ioi, min_eq_left, Ioc_diff_Ioi, f.length_empty,
  zero_add, or_true, le_sup_iff, f.length_Ioc, not_lt]

Result:
no goals