-- Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
theorem AnalyticWithinAt.cpow (fa : AnalyticWithinAt ℂ f s x) (ga : AnalyticWithinAt ℂ g s x)
    (m : f x ∈ slitPlane) : AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) s x

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z => f z ^ g z) s x

Tactic:
have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ exp (log (f z) * g z) := by
  filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]
  intro z fz
  simp only [fz, cpow_def, if_false]

Result:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (fun z => f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z => cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (fun z => f z ^ g z) s x

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (fun z => f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z => cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (fun z => f z ^ g z) s x

Tactic:
apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e

Result:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (fun z => f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z => cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (fun z => cexp (log (f z) * g z)) s x

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ (fun z => f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z => cexp (log (f z) * g z)

Tactic:
filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]

Result:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ ∀ (a : E), f a ≠ 0 → f a ^ g a = cexp (log (f a) * g a)

Proof state:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ ∀ (a : E), f a ≠ 0 → f a ^ g a = cexp (log (f a) * g a)

Tactic:
intro z fz

Result:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
z : E
fz : f z ≠ 0
⊢ f z ^ g z = cexp (log (f z) * g z)

Proof state:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
z : E
fz : f z ≠ 0
⊢ f z ^ g z = cexp (log (f z) * g z)

Tactic:
simp only [fz, cpow_def, if_false]

Result:
no goals

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (fun z => f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z => cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (fun z => cexp (log (f z) * g z)) s x

Tactic:
exact ((fa.clog m).mul ga).cexp

Result:
no goals