calc
  _ = ∫ (x : ℝ) in Ioi 0, ∫ (y : ℝ) in Ioi 0, f₁ (x, y) := ?_
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f₁ (x, y) := setIntegral_integral_swap _ hf
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) := rfl
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * ↑(x * y) ^ (s - 1) * y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (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) := ?_
  _ = _ := integral_mul_right _ _
<;> try (rw [setIntegral_congr (by simp)]; intro y hy; simp only [ofReal_mul])
𝕂 : 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)
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 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) = ∫ (y_1 : ℝ) in Ioi 0, f₁ (y, y_1)

case calc_2
𝕂 : 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 * g (x / y) / ↑y * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y

case calc_3
𝕂 : 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 * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (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)