simp only [integral_mul_right]
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) = ∫ (y_1 : ℝ) in Ioi 0, f₁ (y, y_1)
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f a * g (y / a) / ↑a) * ↑y ^ (s - 1)