[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0
[PROOFSTEP]
suffices : ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0
[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0
case this α : Type u_1 b : ℂ hb : b ≠ 0 ⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [zero_cpow hx, Pi.zero_apply]
[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => 0 ^ x) x = OfNat.ofNat 0 x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 ^ x = OfNat.ofNat 0 x
[PROOFSTEP]
rw [zero_cpow hx, Pi.zero_apply]
[GOAL]
case this
α : Type u_1
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
[PROOFSTEP]
exact IsOpen.eventually_mem isOpen_ne hb
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)
[PROOFSTEP]
suffices : ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)
case this α : Type u_1 a b : ℂ ha : a ≠ 0 ⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [cpow_def_of_ne_zero hx]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => x ^ b) x = (fun x => Complex.exp (Complex.log x * b)) x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = Complex.exp (Complex.log x * b)
[PROOFSTEP]
rw [cpow_def_of_ne_zero hx]
[GOAL]
case this
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
[PROOFSTEP]
exact IsOpen.eventually_mem isOpen_ne ha
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.fst * x.snd)
[PROOFSTEP]
suffices : ∀ᶠ x : ℂ × ℂ in 𝓝 p, x.1 ≠ 0
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.fst * x.snd)
case this α : Type u_1 p : ℂ × ℂ hp_fst : p.fst ≠ 0 ⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [cpow_def_of_ne_zero hx]
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
x : ℂ × ℂ
hx : x.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) x = (fun x => Complex.exp (Complex.log x.fst * x.snd)) x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
x : ℂ × ℂ
hx : x.fst ≠ 0
⊢ x.fst ^ x.snd = Complex.exp (Complex.log x.fst * x.snd)
[PROOFSTEP]
rw [cpow_def_of_ne_zero hx]
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
[PROOFSTEP]
refine' IsOpen.eventually_mem _ hp_fst
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen fun x => x.fst = 0 → False
[PROOFSTEP]
change IsOpen {x : ℂ × ℂ | x.1 = 0}ᶜ
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen {x | x.fst = 0}ᶜ
[PROOFSTEP]
rw [isOpen_compl_iff]
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsClosed {x | x.fst = 0}
[PROOFSTEP]
exact isClosed_eq continuous_fst continuous_const
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
have cpow_eq : (fun x : ℂ => a ^ x) = fun x => exp (log a * x) :=
  by
  ext1 b
  rw [cpow_def_of_ne_zero ha]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ (fun x => a ^ x) = fun x => Complex.exp (Complex.log a * x)
[PROOFSTEP]
ext1 b
[GOAL]
case h
α : Type u_1
a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = Complex.exp (Complex.log a * b)
[PROOFSTEP]
rw [cpow_def_of_ne_zero ha]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => Complex.exp (Complex.log a * x)
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
rw [cpow_eq]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => Complex.exp (Complex.log a * x)
⊢ ContinuousAt (fun x => Complex.exp (Complex.log a * x)) b
[PROOFSTEP]
exact continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)
[GOAL]
α : Type u_1
a b : ℂ
h : b ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α : Type u_1
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]
[GOAL]
case pos
α : Type u_1
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt 0 b
[PROOFSTEP]
exact continuousAt_const
[GOAL]
case neg
α : Type u_1
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
exact continuousAt_const_cpow ha
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
[PROOFSTEP]
have hp_fst_ne_zero : p.fst ≠ 0 := by
  intro h
  cases' hp_fst with hp_fst hp_fst <;>
    · rw [h] at hp_fst 
      simp at hp_fst 
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ p.fst ≠ 0
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
h : p.fst = 0
⊢ False
[PROOFSTEP]
cases' hp_fst with hp_fst hp_fst
[GOAL]
case inl
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0 < p.fst.re
⊢ False
[PROOFSTEP]
rw [h] at hp_fst 
[GOAL]
case inl
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0 < 0.re
⊢ False
[PROOFSTEP]
simp at hp_fst 
[GOAL]
case inr
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : p.fst.im ≠ 0
⊢ False
[PROOFSTEP]
rw [h] at hp_fst 
[GOAL]
case inr
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0.im ≠ 0
⊢ False
[PROOFSTEP]
simp at hp_fst 
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
[PROOFSTEP]
rw [continuousAt_congr (cpow_eq_nhds' hp_fst_ne_zero)]
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.exp (Complex.log x.fst * x.snd)) p
[PROOFSTEP]
refine' continuous_exp.continuousAt.comp _
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.log x.fst * x.snd) p
[PROOFSTEP]
exact
  ContinuousAt.mul (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
    continuous_snd.continuousAt
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
cases h with
| inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
| inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
cases h with
| inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
| inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
case inl
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]

| inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
[GOAL]
case inl
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
exact (continuousAt_const_cpow h).tendsto.comp hf
[GOAL]
case inr
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]

| inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
case inr
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
have : rpow a = fun x : ℝ => ((a : ℂ) ^ (x : ℂ)).re := by
  ext1 x
  rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : a ≠ 0
⊢ rpow a = fun x => (↑a ^ ↑x).re
[PROOFSTEP]
ext1 x
[GOAL]
case h
a b : ℝ
h : a ≠ 0
x : ℝ
⊢ rpow a x = (↑a ^ ↑x).re
[PROOFSTEP]
rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
rw [this]
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b
[PROOFSTEP]
refine' Complex.continuous_re.continuousAt.comp _
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b
[PROOFSTEP]
refine' (continuousAt_const_cpow _).comp Complex.continuous_ofReal.continuousAt
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ↑a ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
have : rpow a = fun x : ℝ => ((a : ℂ) ^ (x : ℂ)).re := by
  ext1 x
  rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : b ≠ 0
⊢ rpow a = fun x => (↑a ^ ↑x).re
[PROOFSTEP]
ext1 x
[GOAL]
case h
a b : ℝ
h : b ≠ 0
x : ℝ
⊢ rpow a x = (↑a ^ ↑x).re
[PROOFSTEP]
rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
rw [this]
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b
[PROOFSTEP]
refine' Complex.continuous_re.continuousAt.comp _
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b
[PROOFSTEP]
refine' (continuousAt_const_cpow' _).comp Complex.continuous_ofReal.continuousAt
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ↑b ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
[PROOFSTEP]
suffices : ∀ᶠ x : ℝ × ℝ in 𝓝 p, x.1 < 0
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
case this p : ℝ × ℝ hp_fst : p.fst < 0 ⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [rpow_def_of_neg hx]
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
x : ℝ × ℝ
hx : x.fst < 0
⊢ (fun x => x.fst ^ x.snd) x = (fun x => exp (log x.fst * x.snd) * cos (x.snd * π)) x
[PROOFSTEP]
dsimp only
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
x : ℝ × ℝ
hx : x.fst < 0
⊢ x.fst ^ x.snd = exp (log x.fst * x.snd) * cos (x.snd * π)
[PROOFSTEP]
rw [rpow_def_of_neg hx]
[GOAL]
case this
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
[PROOFSTEP]
exact IsOpen.eventually_mem (isOpen_lt continuous_fst continuous_const) hp_fst
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
[PROOFSTEP]
suffices : ∀ᶠ x : ℝ × ℝ in 𝓝 p, 0 < x.1
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
case this p : ℝ × ℝ hp_fst : 0 < p.fst ⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [rpow_def_of_pos hx]
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
x : ℝ × ℝ
hx : 0 < x.fst
⊢ (fun x => x.fst ^ x.snd) x = (fun x => exp (log x.fst * x.snd)) x
[PROOFSTEP]
dsimp only
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
x : ℝ × ℝ
hx : 0 < x.fst
⊢ x.fst ^ x.snd = exp (log x.fst * x.snd)
[PROOFSTEP]
rw [rpow_def_of_pos hx]
[GOAL]
case this
p : ℝ × ℝ
hp_fst : 0 < p.fst
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
[PROOFSTEP]
exact IsOpen.eventually_mem (isOpen_lt continuous_const continuous_fst) hp_fst
[GOAL]
p : ℝ × ℝ
hp : p.fst ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
rw [ne_iff_lt_or_gt] at hp 
[GOAL]
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0 ∨ p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases hp with
| inl hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
  refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
  · refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
    refine' (continuousAt_log _).comp continuous_fst.continuousAt
    exact hp.ne
  · exact continuous_snd.continuousAt.mul continuousAt_const
| inr hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
  refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
  refine' (continuousAt_log _).comp continuous_fst.continuousAt
  exact hp.lt.ne.symm
[GOAL]
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0 ∨ p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases hp with
| inl hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
  refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
  · refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
    refine' (continuousAt_log _).comp continuous_fst.continuousAt
    exact hp.ne
  · exact continuous_snd.continuousAt.mul continuousAt_const
| inr hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
  refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
  refine' (continuousAt_log _).comp continuous_fst.continuousAt
  exact hp.lt.ne.symm
[GOAL]
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]

| inl hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
  refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
  · refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
    refine' (continuousAt_log _).comp continuous_fst.continuousAt
    exact hp.ne
  · exact continuous_snd.continuousAt.mul continuousAt_const
[GOAL]
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
[GOAL]
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd) * cos (x.snd * π)) p
[PROOFSTEP]
refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
[GOAL]
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p
[PROOFSTEP]
refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
[GOAL]
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => log x.fst) p
[PROOFSTEP]
refine' (continuousAt_log _).comp continuous_fst.continuousAt
[GOAL]
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ p.fst ≠ 0
[PROOFSTEP]
exact hp.ne
[GOAL]
case inl.refine'_2
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => x.snd * π) p
[PROOFSTEP]
exact continuous_snd.continuousAt.mul continuousAt_const
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]

| inr hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
  refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
  refine' (continuousAt_log _).comp continuous_fst.continuousAt
  exact hp.lt.ne.symm
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p
[PROOFSTEP]
refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => log x.fst) p
[PROOFSTEP]
refine' (continuousAt_log _).comp continuous_fst.continuousAt
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ p.fst ≠ 0
[PROOFSTEP]
exact hp.lt.ne.symm
[GOAL]
p : ℝ × ℝ
hp : 0 < p.snd
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases' p with x y
[GOAL]
case mk
x y : ℝ
hp : 0 < (x, y).snd
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
dsimp only at hp 
[GOAL]
case mk
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
obtain hx | rfl := ne_or_eq x 0
[GOAL]
case mk.inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
exact continuousAt_rpow_of_ne (x, y) hx
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have A : Tendsto (fun p : ℝ × ℝ => exp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
  tendsto_exp_atBot.comp ((tendsto_log_nhdsWithin_zero.comp tendsto_fst).atBot_mul hp tendsto_snd)
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have B : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
  squeeze_zero_norm (fun p => abs_rpow_le_exp_log_mul p.1 p.2) A
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have C : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0) :=
  by
  rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
  exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'
[GOAL]
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)
[PROOFSTEP]
rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
[GOAL]
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, (0, a).fst ^ (0, a).snd = 0
[PROOFSTEP]
exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
C : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
simpa only [← sup_prod, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ, nhds_prod_eq, ContinuousAt,
  zero_rpow hp.ne'] using B.sup (C.mono_right (pure_le_nhds _))
[GOAL]
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x => x ^ q) x
[PROOFSTEP]
change ContinuousAt ((fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun y : ℝ => (y, q)) x
[GOAL]
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt ((fun p => p.fst ^ p.snd) ∘ fun y => (y, q)) x
[PROOFSTEP]
apply ContinuousAt.comp
[GOAL]
case hg
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, q)
[PROOFSTEP]
exact continuousAt_rpow (x, q) h
[GOAL]
case hf
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun y => (y, q)) x
[PROOFSTEP]
exact (continuous_id'.prod_mk continuous_const).continuousAt
[GOAL]
α : Type u_1
l : Filter α
f : α → ℝ
x p : ℝ
hf : Tendsto f l (𝓝 x)
h : x ≠ 0 ∨ 0 ≤ p
h0 : 0 = p
⊢ Tendsto (fun a => f a ^ 0) l (𝓝 (x ^ 0))
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
z : ℂ
hz : 0 < z.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, z)
[PROOFSTEP]
have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, z)
[PROOFSTEP]
rw [ContinuousAt, zero_cpow hz₀, tendsto_zero_iff_norm_tendsto_zero]
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun e => ‖e.fst ^ e.snd‖) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero (fun _ => norm_nonneg _) (fun _ => abs_cpow_le _ _) _
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re / Real.exp (arg x.fst * x.snd.im)) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
simp only [div_eq_mul_inv, ← Real.exp_neg]
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re * Real.exp (-(arg x.fst * x.snd.im))) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
refine' Tendsto.zero_mul_isBoundedUnder_le _ _
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
convert (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _) _
[GOAL]
case h.e'_5.h.e'_3
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 0 = ‖(0, z).fst‖ ^ (re ∘ Prod.snd) (0, z)
[PROOFSTEP]
simp [hz, Real.zero_rpow hz.ne']
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ‖(0, z).fst‖ ≠ 0 ∨ 0 < (re ∘ Prod.snd) (0, z)
[PROOFSTEP]
simp [hz, Real.zero_rpow hz.ne']
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) ((fun x => ‖x‖) ∘ fun x => Real.exp (-(arg x.fst * x.snd.im)))
[PROOFSTEP]
simp only [Function.comp, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
[PROOFSTEP]
rcases exists_gt |im z| with ⟨C, hC⟩
[GOAL]
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
[PROOFSTEP]
refine' ⟨Real.exp (π * C), eventually_map.2 _⟩
[GOAL]
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun x x_1 => x ≤ x_1) (Real.exp (-(arg a.fst * a.snd.im))) (Real.exp (π * C))
[PROOFSTEP]
refine'
  (((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono fun z hz =>
    Real.exp_le_exp.2 <| (neg_le_abs_self _).trans _
[GOAL]
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |arg z.fst * z.snd.im| ≤ π * C
[PROOFSTEP]
rw [_root_.abs_mul]
[GOAL]
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |arg z.fst| * |z.snd.im| ≤ π * C
[PROOFSTEP]
exact mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _) Real.pi_pos.le
[GOAL]
p : ℂ × ℂ
h₁ : 0 ≤ p.fst.re ∨ p.fst.im ≠ 0
h₂ : 0 < p.snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
[PROOFSTEP]
cases' p with z w
[GOAL]
case mk
z w : ℂ
h₁ : 0 ≤ (z, w).fst.re ∨ (z, w).fst.im ≠ 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
[PROOFSTEP]
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne.def, Classical.not_not, not_le_zero_iff] at h₁ 
[GOAL]
case mk
z w : ℂ
h₁ : (0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0) ∨ (z, w).fst = 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
[PROOFSTEP]
rcases h₁ with (h₁ | (rfl : z = 0))
[GOAL]
case mk.inl
z w : ℂ
h₂ : 0 < (z, w).snd.re
h₁ : 0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
case mk.inr w : ℂ h₂ : 0 < (0, w).snd.re ⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, w)
[PROOFSTEP]
exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]
[GOAL]
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
[GOAL]
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) :=
  continuous_ofReal.continuousAt.prod_map continuousAt_id
[GOAL]
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
refine' (continuousAt_cpow (Or.inl _)).comp this
[GOAL]
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ 0 < (↑(x, y).fst, (x, y).snd).fst.re
[PROOFSTEP]
rwa [ofReal_re]
[GOAL]
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ :=
  by
  rw [ofReal_zero]
  apply continuousAt_cpow_zero_of_re_pos
  tauto
[GOAL]
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
[PROOFSTEP]
rw [ofReal_zero]
[GOAL]
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
apply continuousAt_cpow_zero_of_re_pos
[GOAL]
case hz
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ 0 < y.re
[PROOFSTEP]
tauto
[GOAL]
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ :=
  continuous_ofReal.continuousAt.prod_map continuousAt_id
[GOAL]
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
B : ContinuousAt (fun p => (↑p.fst, p.snd)) (0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
[PROOFSTEP]
exact @ContinuousAt.comp (ℝ × ℂ) (ℂ × ℂ) ℂ _ _ _ _ (fun p => ⟨↑p.1, p.2⟩) ⟨0, y⟩ A B
[GOAL]
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y)
  by
  refine' this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) _)
  exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
[GOAL]
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
refine' this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) _)
[GOAL]
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
⊢ ∀ (x : ℝ × ℂ),
    x ∈ Set.Iio 0 ×ˢ Set.univ → (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) x = (fun p => ↑p.fst ^ p.snd) x
[PROOFSTEP]
exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
[GOAL]
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
[PROOFSTEP]
have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) :=
  ContinuousAt.prod_map continuous_ofReal.continuousAt.neg continuousAt_id
[GOAL]
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
[PROOFSTEP]
apply ContinuousAt.mul
[GOAL]
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => (-↑x.fst) ^ x.snd) (x, y)
[PROOFSTEP]
refine' (continuousAt_cpow (Or.inl _)).comp A
[GOAL]
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ 0 < (-↑(x, y).fst, (x, y).snd).fst.re
[PROOFSTEP]
rwa [neg_re, ofReal_re, neg_pos]
[GOAL]
case inr.inr.hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => exp (↑π * I * x.snd)) (x, y)
[PROOFSTEP]
exact (continuous_exp.comp (continuous_const.mul continuous_snd)).continuousAt
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
have :
  (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) = Real.toNNReal ∘ (fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun p : ℝ≥0 × ℝ => (p.1.1, p.2) :=
  by
  ext p
  erw [coe_rpow, Real.coe_toNNReal _ (Real.rpow_nonneg_of_nonneg p.1.2 _)]
  rfl
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
[PROOFSTEP]
ext p
[GOAL]
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑(p.fst ^ p.snd) = ↑((toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)) p)
[PROOFSTEP]
erw [coe_rpow, Real.coe_toNNReal _ (Real.rpow_nonneg_of_nonneg p.1.2 _)]
[GOAL]
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑p.fst ^ p.snd = ↑p.fst ^ ((fun p => (↑p.fst, p.snd)) p).snd
[PROOFSTEP]
rfl
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
rw [this]
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)) (x, y)
[PROOFSTEP]
refine' continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp _ _)
[GOAL]
case refine'_1
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (↑(x, y).fst, (x, y).snd)
[PROOFSTEP]
apply Real.continuousAt_rpow
[GOAL]
case refine'_1.h
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ (↑(x, y).fst, (x, y).snd).fst ≠ 0 ∨ 0 < (↑(x, y).fst, (x, y).snd).snd
[PROOFSTEP]
simp only [Ne.def] at h 
[GOAL]
case refine'_1.h
x : ℝ≥0
y : ℝ
h : ¬x = 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ (↑(x, y).fst, (x, y).snd).fst ≠ 0 ∨ 0 < (↑(x, y).fst, (x, y).snd).snd
[PROOFSTEP]
rw [← NNReal.coe_eq_zero x] at h 
[GOAL]
case refine'_1.h
x : ℝ≥0
y : ℝ
h : ¬↑x = 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ (↑(x, y).fst, (x, y).snd).fst ≠ 0 ∨ 0 < (↑(x, y).fst, (x, y).snd).snd
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
[PROOFSTEP]
exact ((continuous_subtype_val.comp continuous_fst).prod_mk continuous_snd).continuousAt
[GOAL]
x y : ℝ≥0
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy)
[GOAL]
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < (y - 1 + 1) ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
rw [tsub_add_cancel_of_le hy.le] at hm 
[GOAL]
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
refine' eventually_atTop.2 ⟨m + 1, fun n hn => _⟩
[GOAL]
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
simpa only [NNReal.rpow_one_div_le_iff (Nat.cast_pos.2 <| m.succ_pos.trans_le hn), NNReal.rpow_nat_cast] using
  hm.le.trans (pow_le_pow hy.le (m.le_succ.trans hn))
[GOAL]
x : ℝ≥0
y : ℝ
h✝¹ : x ≠ 0 ∨ 0 ≤ y
h✝ : 0 ≤ y
h : 0 = y
⊢ ContinuousAt (fun z => z ^ 0) x
[PROOFSTEP]
simp only [rpow_zero, continuousAt_const]
[GOAL]
x : ℝ≥0∞
hx : x ≠ ⊤
y : ℝ≥0∞
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
lift x to ℝ≥0 using hx
[GOAL]
case intro
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
by_cases y = ∞
[GOAL]
case intro
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
by_cases y = ∞
[GOAL]
case pos
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
exact eventually_of_forall fun n => h.symm ▸ le_top
[GOAL]
case neg
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
lift y to ℝ≥0 using h
[GOAL]
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y
[PROOFSTEP]
have := NNReal.eventually_pow_one_div_le x (by exact_mod_cast hy : 1 < y)
[GOAL]
x y : ℝ≥0
hy : 1 < ↑y
⊢ 1 < y
[PROOFSTEP]
exact_mod_cast hy
[GOAL]
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y
[PROOFSTEP]
refine' this.congr (eventually_of_forall fun n => _)
[GOAL]
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ x ^ (1 / ↑n) ≤ y ↔ ↑x ^ (1 / ↑n) ≤ ↑y
[PROOFSTEP]
rw [coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]
[GOAL]
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ 0 ≤ 1 / ↑n
[PROOFSTEP]
positivity
[GOAL]
x : ℝ≥0∞
y : ℝ
h : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
by_cases hx : x = ⊤
[GOAL]
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
rw [hx, ContinuousAt]
[GOAL]
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ Tendsto (fun a => a ^ y) (𝓝 ⊤) (𝓝 (⊤ ^ y))
[PROOFSTEP]
convert ENNReal.tendsto_rpow_at_top h
[GOAL]
case h.e'_5.h.e'_3
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ⊤ ^ y = ⊤
[PROOFSTEP]
simp [h]
[GOAL]
case neg
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
lift x to ℝ≥0 using hx
[GOAL]
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (fun a => a ^ y) ↑x
[PROOFSTEP]
rw [continuousAt_coe_iff]
[GOAL]
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt ((fun a => a ^ y) ∘ some) x
[PROOFSTEP]
convert continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1
[GOAL]
case h.e'_5
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ (fun a => a ^ y) ∘ some = some ∘ fun z => z ^ y
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_5.h
y : ℝ
h : 0 < y
x✝ x : ℝ≥0
⊢ ((fun a => a ^ y) ∘ some) x = (some ∘ fun z => z ^ y) x
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ h.le]
[GOAL]
y : ℝ
⊢ Continuous fun a => a ^ y
[PROOFSTEP]
refine continuous_iff_continuousAt.2 fun x => ?_
[GOAL]
y : ℝ
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)
[GOAL]
case inl
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
exact continuousAt_rpow_const_of_pos hy
[GOAL]
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ 0) x
[PROOFSTEP]
simp only [rpow_zero]
[GOAL]
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => 1) x
[PROOFSTEP]
exact continuousAt_const
[GOAL]
case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
obtain ⟨z, hz⟩ : ∃ z, y = -z := ⟨-y, (neg_neg _).symm⟩
[GOAL]
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
have z_pos : 0 < z := by simpa [hz] using hy
[GOAL]
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ 0 < z
[PROOFSTEP]
simpa [hz] using hy
[GOAL]
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
simp_rw [hz, rpow_neg]
[GOAL]
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => (a ^ z)⁻¹) x
[PROOFSTEP]
exact continuous_inv.continuousAt.comp (continuousAt_rpow_const_of_pos z_pos)
[GOAL]
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => c * x ^ y) (𝓝 0) (𝓝 0)
[PROOFSTEP]
convert ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
[GOAL]
case h.e'_5.h.e'_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 = c * 0 ^ y
[PROOFSTEP]
simp [hy]
[GOAL]
case convert_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 ^ y ≠ 0 ∨ c ≠ ⊤
[PROOFSTEP]
exact Or.inr hc
