α : Type ?u.63999
β : Type ?u.64002
ι : Type ?u.64005
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ m) x → x ≠ 0 ∨ 0 ≤ m
α : Type ?u.63999
β : Type ?u.64002
ι : Type ?u.64005
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
refine' ⟨_, continuousAt_zpow₀ _ _⟩
α : Type ?u.63999
β : Type ?u.64002
ι : Type ?u.64005
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ x = 0 ∧ m < 0 → ¬ContinuousAt (fun x => x ^ m) x
α : Type ?u.63999
β : Type ?u.64002
ι : Type ?u.64005
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ m) x → x ≠ 0 ∨ 0 ≤ m
contrapose!
case intro
α : Type ?u.63999
β : Type ?u.64002
ι : Type ?u.64005
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
hc : ContinuousAt (fun x => x ^ m) 0
⊢ False
α : Type ?u.63999
β : Type ?u.64002
ι : Type ?u.64005
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ x = 0 ∧ m < 0 → ¬ContinuousAt (fun x => x ^ m) x
rintro ⟨rfl, hm⟩ hc
no goals
case intro
α : Type ?u.63999
β : Type ?u.64002
ι : Type ?u.64005
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
hc : ContinuousAt (fun x => x ^ m) 0
⊢ False
exact not_tendsto_atTop_of_tendsto_nhds (hc.tendsto.mono_left nhdsWithin_le_nhds).norm
  (tendsto_norm_zpow_nhdsWithin_0_atTop hm)