convert Perron.formulaLtOne (div_pos tpos xpos) ((div_lt_one xpos).mpr t_lt_x) σpos using 2
𝕂 : 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
case h.e'_2.h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = Perron.f (t / x)