case intro
𝕜 : Type u_1
α : Type ?u.32706
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
𝕜 : Type u_1
α : Type ?u.32706
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
hn : n < 0
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
case intro
𝕜 : Type u_1
α : Type ?u.32706
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
N : ℕ
hn : 0 < N
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
case intro
𝕜 : Type u_1
α : Type ?u.32706
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
rw [← neg_pos, ← h, Nat.cast_pos] at hn
no goals
case intro
𝕜 : Type u_1
α : Type ?u.32706
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
N : ℕ
hn : 0 < N
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'