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

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

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