simp only [one_div, mul_inv_rev, inv_I, neg_mul, neg_eq_zero, mul_eq_zero, I_ne_zero,
  inv_eq_zero, ofReal_eq_zero, pi_ne_zero, OfNat.ofNat_ne_zero, or_self, false_or]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0