convert (Complex.mul_cpow_ofReal_nonneg tpos.le (inv_pos.mpr xpos).le s).symm using 2
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
case h.e'_2.h.e'_6
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑x ^ (-s) = ↑x⁻¹ ^ s

case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t / ↑x = ↑t * ↑x⁻¹