no goals
α : Type u_2
β : Type u_1
γ : Type ?u.848051
δ : Type ?u.848054
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
h : Integrable f
⊢ Integrable f
simpa only [smul_smul, ENNReal.inv_mul_cancel h₁ h₂, one_smul] using
  h.smul_measure (ENNReal.inv_ne_top.2 h₁)