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

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