α : Type u_1
β : Type u_2
γ : Type ?u.837801
δ : Type ?u.837804
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : Memℒp f 1
⊢ Memℒp f 1
α : Type u_1
β : Type u_2
γ : Type ?u.837801
δ : Type ?u.837804
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : Integrable f
⊢ Integrable f
rw [← memℒp_one_iff_integrable] at hf⊢
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.837801
δ : Type ?u.837804
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : Memℒp f 1
⊢ Memℒp f 1
exact hf.of_measure_le_smul c hc hμ'_le