rw [mul_comm (a : 𝕂), div_mul, mul_div_assoc, div_self ?_, mul_one]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ f (x✝ * a) / ↑x✝ = ↑a * (f (x✝ * a) / (↑x✝ * ↑a))
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ ↑a ≠ 0