-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_rpow {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 < y) :
    ContinuousAt (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) (x, y)

Proof state:
case refine_1.h
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ (↑(x, y).1, (x, y).2).1 ≠ 0 ∨ 0 < (↑(x, y).1, (x, y).2).2

Tactic:
simpa using h

Result:
no goals

Proof state:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)) (x, y)

Tactic:
refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)

Result:
case refine_1
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (↑(x, y).1, (x, y).2)

case refine_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (fun p => (↑p.1, p.2)) (x, y)

Proof state:
case refine_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (fun p => (↑p.1, p.2)) (x, y)

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑p.1 ^ p.2 = ↑p.1 ^ ((fun p => (↑p.1, p.2)) p).2

Tactic:
rfl

Result:
no goals

Proof state:
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑(p.1 ^ p.2) = ↑((toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)) p)

Tactic:
erw [coe_rpow, Real.coe_toNNReal _ (Real.rpow_nonneg p.1.2 _)]

Result:
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑p.1 ^ p.2 = ↑p.1 ^ ((fun p => (↑p.1, p.2)) p).2

Proof state:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)

Tactic:
ext p

Result:
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑(p.1 ^ p.2) = ↑((toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)) p)

Proof state:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Tactic:
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 p.1.2 _)]
  rfl

Result:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Proof state:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (x, y)

Tactic:
rw [this]

Result:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)) (x, y)

Proof state:
case refine_1
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ ContinuousAt (fun p => p.1 ^ p.2) (↑(x, y).1, (x, y).2)

Tactic:
apply Real.continuousAt_rpow

Result:
case refine_1.h
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)
⊢ (↑(x, y).1, (x, y).2).1 ≠ 0 ∨ 0 < (↑(x, y).1, (x, y).2).2