no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1265765
δ : Type ?u.1265768
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α →ₘ[μ] β
⊢ Integrable f ↔ f ∈ Lp β 1
rw [← integrable_coeFn, ← memℒp_one_iff_integrable, Lp.mem_Lp_iff_memℒp]