no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1321854
δ : Type ?u.1321857
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ‖toL1 f hf‖ = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
rw [norm_toL1, lintegral_norm_eq_lintegral_edist]