case zero => exact hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[zero] f) U
no goals