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)
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
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
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)
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)
rw [this]
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)

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)
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)
refine' continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp _ _)
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)
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)
ext p
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
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)
erw [coe_rpow, Real.coe_toNNReal _ (Real.rpow_nonneg_of_nonneg p.1.2 _)]
no goals
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
rfl
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
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)
apply Real.continuousAt_rpow
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
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
simp only [Ne.def] at h
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
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
rw [← NNReal.coe_eq_zero x] at h
no goals
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
exact h
no goals
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)
exact ((continuous_subtype_val.comp continuous_fst).prod_mk continuous_snd).continuousAt