(rw [setIntegral_congr (by simp)]; intro y hy; simp only [ofReal_mul])
case calc_4
𝕂 : 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 : ℝ) (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    ∫ (y : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
case calc_4
𝕂 : 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
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)