simp only [this.le, inv_rpow, Function.comp_apply, rpow_neg, inv_inv]
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✝
no goals