p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
⊢ 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
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ 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 A : p.1 ≠ 0 := by intro h; simp [h, lt_irrefl] at hp
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
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
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
⊢ 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) :=
  ((isOpen_ne.preimage continuous_fst).eventually_mem A).mono fun p hp =>
    cpow_def_of_ne_zero hp _
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    (p.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
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
rw [cpow_sub _ _ A, cpow_one, mul_div_left_comm, mul_smul, mul_smul]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
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.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    (p.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
no goals
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
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.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
simpa only [cpow_def_of_ne_zero A, div_eq_mul_inv, mul_smul, add_comm, smul_add] using
  ((hasStrictFDerivAt_fst.clog hp).mul hasStrictFDerivAt_snd).cexp
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
h : p.fst = 0
⊢ False
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ p.fst ≠ 0
intro h
no goals
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
h : p.fst = 0
⊢ False
simp [h, lt_irrefl] at hp