case ofNat
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x => x ^ Int.ofNat m) x

case negSucc
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => x ^ Int.negSucc m) x
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℤ
h : x ≠ 0 ∨ 0 ≤ m
⊢ ContinuousAt (fun x => x ^ m) x
cases' m with m m
no goals
case ofNat
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x => x ^ Int.ofNat m) x
simpa only [Int.ofNat_eq_coe, zpow_coe_nat] using continuousAt_pow x m
case negSucc
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
case negSucc
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => x ^ Int.negSucc m) x
simp only [zpow_negSucc]
case negSucc
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
case negSucc
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_le
no goals
case negSucc
α : Type ?u.63846
β : Type ?u.63849
G₀ : Type u_1
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
exact (continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)