no goals
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
c : ℝ
hf : Integrable I l (c • f) vol
hc : c ≠ 0
⊢ Integrable I l f vol
simpa [inv_smul_smul₀ hc] using hf.smul c⁻¹