no goals
α : Type u_2
β : Type ?u.1130144
γ : Type ?u.1130147
δ : Type ?u.1130150
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
f✝ f : α → 𝕜
h : Integrable f
c : 𝕜
⊢ Integrable fun x => f x / c
simp_rw [div_eq_mul_inv, h.mul_const]