x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt ((fun p => p.fst ^ p.snd) ∘ fun y => (y, q)) x
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x => x ^ q) x
change ContinuousAt ((fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun y : ℝ => (y, q)) x
case hg
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, q)

case hf
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun y => (y, q)) x
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt ((fun p => p.fst ^ p.snd) ∘ fun y => (y, q)) x
apply ContinuousAt.comp
no goals
case hg
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, q)
exact continuousAt_rpow (x, q) h
no goals
case hf
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun y => (y, q)) x
exact (continuous_id'.prod_mk continuous_const).continuousAt