no goals
𝕜 : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g✝ : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesOnBall f p x r
y✝ : E
hy : y✝ ∈ EMetric.ball 0 r
⊢ HasSum (fun n => ↑(compFormalMultilinearSeries g p n) fun x => y✝) ((↑g ∘ f) (x + y✝))
simpa only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
  ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply] using
  g.hasSum (h.hasSum hy)