field_simp [f, mul_ne_zero s_eq_zero (fun hs ↦ add_eq_zero_iff_eq_neg.mp hs |> s_eq_neg_one)]
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t ^ s * ↑x ^ (-s) = (↑t / ↑x) ^ s