Theorem: MeasureTheory.integral_comp_mul_left_I0i_haar (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (a * y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
convert integral_comp_mul_right_I0i_haar f ha using 5
State after:
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ a * x✝ = x✝ * a

State before:
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ a * x✝ = x✝ * a
Tactic:
ring
State after:
no goals