have h1 : g z ≠ 0 := λ h => fz_nonzero (by simp [Eventually.self_of_nhds hg, h, n_pos.ne.symm])
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))