∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {β : Type u_6}
  {m m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β},
  m ≤ m0 →
    ∀ (f : MeasureTheory.SimpleFunc β F),
      MeasureTheory.Integrable (⇑f) μ → ∫ (x : β), f x ∂μ = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x