beta_reduce
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), (fun s => ↑x ^ (-s) * f s) (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)