f : StieltjesFunction
a b : ℝ
⊢ ↑↑{ toOuterMeasure := StieltjesFunction.outer f,
            m_iUnion :=
              (_ :
                ∀ (_s : ℕ → Set ℝ),
                  (∀ (i : ℕ), MeasurableSet (_s i)) →
                    Pairwise (Disjoint on _s) →
                      ↑(StieltjesFunction.outer f) (⋃ (i : ℕ), _s i) = ∑' (i : ℕ), ↑(StieltjesFunction.outer f) (_s i)),
            trimmed := (_ : OuterMeasure.trim (StieltjesFunction.outer f) = StieltjesFunction.outer f) }
      (Ioc a b) =
    ofReal (↑f b - ↑f a)
f : StieltjesFunction
a b : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ioc a b) = ofReal (↑f b - ↑f a)
rw [StieltjesFunction.measure]
no goals
f : StieltjesFunction
a b : ℝ
⊢ ↑↑{ toOuterMeasure := StieltjesFunction.outer f,
            m_iUnion :=
              (_ :
                ∀ (_s : ℕ → Set ℝ),
                  (∀ (i : ℕ), MeasurableSet (_s i)) →
                    Pairwise (Disjoint on _s) →
                      ↑(StieltjesFunction.outer f) (⋃ (i : ℕ), _s i) = ∑' (i : ℕ), ↑(StieltjesFunction.outer f) (_s i)),
            trimmed := (_ : OuterMeasure.trim (StieltjesFunction.outer f) = StieltjesFunction.outer f) }
      (Ioc a b) =
    ofReal (↑f b - ↑f a)
exact f.outer_Ioc a b