case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
f : StieltjesFunction
a b : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
rcases le_or_lt a b with (hab | hab)
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
A : Disjoint {a} (Ioc a b)
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
have A : Disjoint {a} (Ioc a b) := by simp
no goals
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
A : Disjoint {a} (Ioc a b)
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ENNReal.ofReal_add,
  f.mono.leftLim_le, measure_union A measurableSet_Ioc, f.mono hab]
no goals
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ Disjoint {a} (Ioc a b)
simp
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ 0 = ofReal (↑f b - leftLim (↑f) a)
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
simp only [hab, measure_empty, Icc_eq_empty, not_le]
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ofReal (↑f b - leftLim (↑f) a) = 0
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ 0 = ofReal (↑f b - leftLim (↑f) a)
symm
no goals
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ofReal (↑f b - leftLim (↑f) a) = 0
simp [ENNReal.ofReal_eq_zero, f.mono.le_leftLim hab]