no goals
α : Type u_2
E : Type ?u.1053184
F : Type ?u.1053187
𝕜 : Type ?u.1053190
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1055881
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : Integrable f
⊢ ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
rw [integral_norm_eq_lintegral_nnnorm hf.aestronglyMeasurable,
  ENNReal.ofReal_toReal (lt_top_iff_ne_top.mp hf.2)]