ext
case h.e'_3
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ (fun σ => x ^ σ * C) = (fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg
case h.e'_3.h
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
x✝ : ℝ
⊢ x ^ x✝ * C = ((fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg) x✝