no goals
α : Type u_1
F : Type ?u.1981
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → ℝ
h : Memℒp f 2
⊢ Integrable fun x => f x ^ 2
simpa [← memℒp_one_iff_integrable] using h.norm_rpow two_ne_zero ENNReal.two_ne_top