simp only [RCLike.ofReal_mul, zero_mul, eq_inv_smul_iff₀ (ne_of_gt ha)] at this
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (x : ℝ) in Ioi 0, (fun y => f y / ↑y) (x * a) = a⁻¹ • ∫ (x : ℝ) in Ioi (0 * a), (fun y => f y / ↑y) x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : a • ∫ (x : ℝ) in Ioi 0, f (x * a) / (↑x * ↑a) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y