by_cases s_eq_neg_one : s = -1
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s
case pos
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
⊢ f t s * ↑x ^ (-s) = f (t / x) s