deriv_zpow_mul_eventuallyEq

theorem deriv_zpow_mul_eventuallyEq {f : ℂ → ℂ} {x : ℂ} {n : ℤ}    (g : ℂ → ℂ) (hg_an : AnalyticAt ℂ g x)    (hg_eq : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z) :    deriv f =ᶠ[𝓝[≠] x]      (fun z ↦ (z - x) ^ (n - 1)) * (fun z ↦ (n : ℂ) * g z + (z - x) * deriv g z) := by  have key : ∀ᶠ z in 𝓝 x, z ≠ x → f z = (z - x) ^ n • g z := eventually_nhdsWithin_iff.mp hg_eq  obtain ⟨V, hV_sub, hV_open, hxV⟩ := eventually_nhds_iff.mp key  filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (hV_open.mem_nhds hxV),    hg_an.eventually_analyticAt.filter_mono nhdsWithin_le_nhds] with z₀ hz₀ne hz₀V hg_an_z₀  have hz₀x : z₀ - x ≠ 0 := sub_ne_zero.mpr hz₀ne  have hloc : f =ᶠ[𝓝 z₀] fun z ↦ (z - x) ^ n * g z := by    filter_upwards [(hV_open.sdiff isClosed_singleton).mem_nhds ⟨hz₀V, hz₀ne⟩] with z hz    rw [hV_sub z hz.1 hz.2, smul_eq_mul]  have hd1 : HasDerivAt (fun z : ℂ ↦ (z - x) ^ n) ((n : ℂ) * (z₀ - x) ^ (n - 1)) z₀ := by    convert! (hasDerivAt_zpow n (z₀ - x) (Or.inl hz₀x)).comp z₀ ((hasDerivAt_id z₀).sub_const x) using 1    ring  have hprod : HasDerivAt f ((n : ℂ) * (z₀ - x) ^ (n - 1) * g z₀ + (z₀ - x) ^ n * deriv g z₀) z₀ :=    (hd1.mul hg_an_z₀.differentiableAt.hasDerivAt).congr_of_eventuallyEq hloc  rw [hprod.deriv]; simp only [Pi.mul_apply]  rw [show (z₀ - x) ^ (n - 1) = (z₀ - x) ^ n * (z₀ - x)⁻¹ by rw [zpow_sub_one₀ hz₀x]]; field_simp