p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0 ∨ p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
p : ℝ × ℝ
hp : p.fst ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
rw [ne_iff_lt_or_gt] at hp
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd) * cos (x.snd * π)) p
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p

case inl.refine'_2
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => x.snd * π) p
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd) * cos (x.snd * π)) p
refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => log x.fst) p
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p
refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ p.fst ≠ 0
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => log x.fst) p
refine' (continuousAt_log _).comp continuous_fst.continuousAt
no goals
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ p.fst ≠ 0
exact hp.ne
no goals
case inl.refine'_2
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => x.snd * π) p
exact continuous_snd.continuousAt.mul continuousAt_const
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => log x.fst) p
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p
refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ p.fst ≠ 0
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => log x.fst) p
refine' (continuousAt_log _).comp continuous_fst.continuousAt
no goals
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ p.fst ≠ 0
exact hp.lt.ne.symm