have lh3 := eventually_eventually_nhds.mpr hp.eq_pow_order_mul_iterate_dslope
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
lh3 :
  ∀ᶠ (y : ℂ) in 𝓝 z₀,
    ∀ᶠ (x : ℂ) in 𝓝 y,
      f x = (x - z₀) ^ FormalMultilinearSeries.order p • (swap dslope z₀)^[FormalMultilinearSeries.order p] f x
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z