x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
  (continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd))
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
case h.e'_10
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ (p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    exp (log p.fst * p.snd) •
      (log p.fst • ContinuousLinearMap.snd ℝ ℝ ℝ + p.snd • p.fst⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd))
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
convert ((hasStrictFDerivAt_fst.log hp.ne').mul hasStrictFDerivAt_snd).exp using 1
no goals
case h.e'_10
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ (p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    exp (log p.fst * p.snd) •
      (log p.fst • ContinuousLinearMap.snd ℝ ℝ ℝ + p.snd • p.fst⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm,
  div_eq_mul_inv, smul_smul, smul_smul, mul_assoc, add_comm]