Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
⊢ ((∫ (a : Ω), (NNReal.toReal ∘ ↑(nnrealPart f)) a ∂μ) - ∫ (a : Ω), (NNReal.toReal ∘ ↑(nnrealPart (-f))) a ∂μ) =
    (∫ (ω : Ω), ↑(↑(nnrealPart f) ω) ∂μ) - ∫ (ω : Ω), ↑(↑(nnrealPart (-f)) ω) ∂μ
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
⊢ (∫ (ω : Ω), ↑f ω ∂μ) = (∫ (ω : Ω), ↑(↑(nnrealPart f) ω) ∂μ) - ∫ (ω : Ω), ↑(↑(nnrealPart (-f)) ω) ∂μ
simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub,
  integrable_of_boundedContinuous_to_nnreal]
no goals
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
⊢ ((∫ (a : Ω), (NNReal.toReal ∘ ↑(nnrealPart f)) a ∂μ) - ∫ (a : Ω), (NNReal.toReal ∘ ↑(nnrealPart (-f))) a ∂μ) =
    (∫ (ω : Ω), ↑(↑(nnrealPart f) ω) ∂μ) - ∫ (ω : Ω), ↑(↑(nnrealPart (-f)) ω) ∂μ
rfl