case intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℤ
hm : -m < 0
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[{0}ᶜ] 0) atTop
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℤ
hm : m < 0
⊢ Tendsto (fun x => ‖x ^ m‖) (𝓝[{0}ᶜ] 0) atTop
rcases neg_surjective m with ⟨m, rfl⟩
case intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℤ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[{0}ᶜ] 0) atTop
case intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℤ
hm : -m < 0
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[{0}ᶜ] 0) atTop
rw [neg_lt_zero] at hm
case intro.intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < ↑m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[{0}ᶜ] 0) atTop
case intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℤ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[{0}ᶜ] 0) atTop
lift m to ℕ using hm.le
case intro.intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[{0}ᶜ] 0) atTop
case intro.intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < ↑m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[{0}ᶜ] 0) atTop
rw [Int.coe_nat_pos] at hm
case intro.intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x⁻¹‖ ^ m) (𝓝[{0}ᶜ] 0) atTop
case intro.intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[{0}ᶜ] 0) atTop
simp only [norm_pow, zpow_neg, zpow_ofNat, ← inv_pow]
no goals
case intro.intro
α : Type ?u.55104
β : Type ?u.55107
ι : Type ?u.55110
𝕜 : Type u_1
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x⁻¹‖ ^ m) (𝓝[{0}ᶜ] 0) atTop
exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop