have := Tendsto.mul_const C (tendsto_rpow_atTop_of_base_lt_one x (by linarith) x_lt_one)
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
this : Tendsto (fun k => x ^ k * C) atTop (𝓝 (0 * C))
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)