case pos
α : Type ?u.292640
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x => a ^ x) b

case neg
α : Type ?u.292640
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x => a ^ x) b
α : Type ?u.292640
a b : ℂ
h : b ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b
by_cases ha : a = 0
case pos
α : Type ?u.292640
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt 0 b
case pos
α : Type ?u.292640
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x => a ^ x) b
rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]
no goals
case pos
α : Type ?u.292640
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt 0 b
exact continuousAt_const
no goals
case neg
α : Type ?u.292640
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x => a ^ x) b
exact continuousAt_const_cpow ha