Theorem: MeasureTheory.integral_comp_div_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:
calc
  _ = ∫ (y : ℝ) in Ioi 0, f (a * y) / y := ?_
  _ = _ := integral_comp_mul_left_I0i_haar f ha
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (a / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f (a * y) / ↑y

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 (a * y) / ↑y
Tactic:
convert (integral_comp_inv_I0i_haar fun y ↦ f (a * (1 / y))).symm using 4
State after:
case h.e'_2.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a / x✝) = f (a * (1 / x✝))

case h.e'_3.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a * x✝) = f (a * (1 / (1 / x✝)))

State before:
case h.e'_2.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a / x✝) = f (a * (1 / x✝))
Tactic:
rw [mul_one_div]
State after:
no goals

State before:
case h.e'_3.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a * x✝) = f (a * (1 / (1 / x✝)))
Tactic:
rw [one_div_one_div]
State after:
no goals