case inl
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
hneg : p.fst < 0
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p

case inr
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
hpos : 0 < p.fst
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
cases' hp.lt_or_lt with hneg hpos
no goals
case inl
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
hneg : p.fst < 0
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p

case inr
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
hpos : 0 < p.fst
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
exacts
  [(((contDiffAt_fst.log hneg.ne).mul contDiffAt_snd).exp.mul
        (contDiffAt_snd.mul contDiffAt_const).cos).congr_of_eventuallyEq
    ((continuousAt_fst.eventually (gt_mem_nhds hneg)).mono fun p hp => rpow_def_of_neg hp _),
  ((contDiffAt_fst.log hpos.ne').mul contDiffAt_snd).exp.congr_of_eventuallyEq
    ((continuousAt_fst.eventually (lt_mem_nhds hpos)).mono fun p hp => rpow_def_of_pos hp _)]