no goals
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ) in Ioi a, g (x * b)) = abs b⁻¹ • ∫ (x : ℝ) in Ioi (a * b), g x
simpa only [mul_comm] using integral_comp_mul_left_Ioi g a hb