case mk
x y : ℝ
hp : 0 < (x, y).snd
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
p : ℝ × ℝ
hp : 0 < p.snd
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
cases' p with x y
case mk
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
case mk
x y : ℝ
hp : 0 < (x, y).snd
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
dsimp only at hp
case mk.inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)

case mk.inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
case mk
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
obtain hx | rfl := ne_or_eq x 0
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)
case mk.inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
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)
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)
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)
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
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)
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)
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'
no goals
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)
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 _))
no goals
case mk.inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
exact continuousAt_rpow_of_ne (x, y) hx
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
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)
rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
no goals
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
exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'