Theorem: MellinInversion_aux4 (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℂ
σ : ℝ
σ_ne_zero : σ ≠ 0
σ_ne_negOne : σ ≠ -1
fInt : IntegrableOn (fun x => f x * ↑x ^ ↑σ) (Ioi 0) volume
⊢ VerticalIntegral (fun s => ∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s + 1) / (s * (s + 1))) σ =
    ∫ (x : ℝ) in Ioi 0, VerticalIntegral (fun s => f x * ↑x ^ (s + 1) / (s * (s + 1))) σ
Tactic:
sorry
State after:
no goals