f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
f : StieltjesFunction
a b : ℝ
⊢ length f (Ioc a b) = ofReal (↑f b - ↑f a)
refine'
  le_antisymm (iInf_le_of_le a <| iInf₂_le b Subset.rfl)
    (le_iInf fun a' => le_iInf fun b' => le_iInf fun h => ENNReal.coe_le_coe.2 _)
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')

case inr
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
cases' le_or_lt b a with ab ab
case inr.intro
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
h₁ : b ≤ b'
h₂ : a' ≤ a
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
case inr
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
cases' (Ioc_subset_Ioc_iff ab).1 h with h₁ h₂
no goals
case inr.intro
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
h₁ : b ≤ b'
h₂ : a' ≤ a
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
exact Real.toNNReal_le_toNNReal (sub_le_sub (f.mono h₁) (f.mono h₂))
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ 0 ≤ Real.toNNReal (↑f b' - ↑f a')
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
rw [Real.toNNReal_of_nonpos (sub_nonpos.2 (f.mono ab))]
no goals
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ 0 ≤ Real.toNNReal (↑f b' - ↑f a')
apply zero_le