calc
  _ = ∫ y in Ioi 0, f (y * x) * g (1 / y) / y := ?_
  _ = _ := ?_
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y = ∫ (y : ℝ) in Ioi 0, g y * f (x / y) / ↑y
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, g y * f (x / y) / ↑y