∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {P : Type u_7} [inst : NormedAddCommGroup P]
  {f : α → P}, MeasureTheory.Integrable f μ → ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ