-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.2) :
    ContinuousAt (fun p : ℝ × ℝ => p.1 ^ p.2) p

Proof state:
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Tactic:
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'

Result:
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
C : Tendsto (fun p => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Proof state:
case mk
x y : ℝ
hp : 0 < (x, y).2
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Tactic:
dsimp only at hp

Result:
case mk
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Proof state:
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
C : Tendsto (fun p => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Tactic:
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 _))

Result:
no goals

Proof state:
case mk
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Tactic:
obtain hx | rfl := ne_or_eq x 0

Result:
case mk.inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

case mk.inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Proof state:
case mk.inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Tactic:
exact continuousAt_rpow_of_ne (x, y) hx

Result:
no goals

Proof state:
p : ℝ × ℝ
hp : 0 < p.2
⊢ ContinuousAt (fun p => p.1 ^ p.2) p

Tactic:
obtain ⟨x, y⟩ := p

Result:
case mk
x y : ℝ
hp : 0 < (x, y).2
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Proof state:
case mk.inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Tactic:
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)

Result:
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Proof state:
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, (0, a).1 ^ (0, a).2 = 0

Tactic:
exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'

Result:
no goals

Proof state:
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ Tendsto (fun p => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)

Tactic:
rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]

Result:
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, (0, a).1 ^ (0, a).2 = 0

Proof state:
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Tactic:
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

Result:
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)