p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)

case this
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
suffices : ∀ᶠ x : ℝ × ℝ in 𝓝 p, x.1 < 0
case this
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)

case this
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
exact
  this.mono fun x hx => by
    dsimp only
    rw [rpow_def_of_neg hx]
no goals
case this
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
exact IsOpen.eventually_mem (isOpen_lt continuous_fst continuous_const) hp_fst
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
x : ℝ × ℝ
hx : x.fst < 0
⊢ x.fst ^ x.snd = exp (log x.fst * x.snd) * cos (x.snd * π)
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
x : ℝ × ℝ
hx : x.fst < 0
⊢ (fun x => x.fst ^ x.snd) x = (fun x => exp (log x.fst * x.snd) * cos (x.snd * π)) x
dsimp only
no goals
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
x : ℝ × ℝ
hx : x.fst < 0
⊢ x.fst ^ x.snd = exp (log x.fst * x.snd) * cos (x.snd * π)
rw [rpow_def_of_neg hx]