convert Perron.f_mul_eq_f tpos xpos s using 1
case h.e'_2.h.e'_6.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = ↑(t / x) ^ s / (s * (s + 1))
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)