-- Mathlib/Analysis/Analytic/Composition.lean
theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G}
    {p : FormalMultilinearSeries 𝕜 E F} {x : E} {t : Set F} {s : Set E}
    (hg : HasFPowerSeriesWithinAt g q t (f x)) (hf : HasFPowerSeriesWithinAt f p s x)
    (hs : Set.MapsTo f s t) : HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ EMetric.ball x δ → f z ∈ insert (f x) t ∩ EMetric.ball (f x) rg
rf' : ℝ≥0∞ := rf ⊓ δ
min_pos : 0 < rf' ⊓ ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ EMetric.ball 0 (rf' ⊓ ↑r)
y_mem : y ∈ EMetric.ball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ EMetric.ball (f x) rg
A : Tendsto (fun n => (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x => y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n => q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b => y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n => ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j => y) atTop
    (𝓝 (g (f (x + y))))
⊢ ∀ (i : (n : ℕ) × Composition n),
    ‖(q.compAlongComposition p i.snd) fun _j => y‖ ≤ ‖q.compAlongComposition p i.snd‖ * ↑r ^ i.fst

Tactic:
rintro ⟨n, c⟩

Result:
case mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ EMetric.ball x δ → f z ∈ insert (f x) t ∩ EMetric.ball (f x) rg
rf' : ℝ≥0∞ := rf ⊓ δ
min_pos : 0 < rf' ⊓ ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ EMetric.ball 0 (rf' ⊓ ↑r)
y_mem : y ∈ EMetric.ball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ EMetric.ball (f x) rg
A : Tendsto (fun n => (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x => y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n => q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b => y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n => ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j => y) atTop
    (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
⊢ ‖(q.compAlongComposition p ⟨n, c⟩.snd) fun _j => y‖ ≤ ‖q.compAlongComposition p ⟨n, c⟩.snd‖ * ↑r ^ ⟨n, c⟩.fst

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ EMetric.ball x δ → f z ∈ insert (f x) t ∩ EMetric.ball (f x) rg
rf' : ℝ≥0∞ := rf ⊓ δ
min_pos : 0 < rf' ⊓ ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ EMetric.ball 0 (rf' ⊓ ↑r)
y_mem : y ∈ EMetric.ball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ EMetric.ball (f x) rg
A : Tendsto (fun n => (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x => y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n => q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b => y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n => ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j => y) atTop
    (𝓝 (g (f (x + y))))
⊢ HasSum (fun n => (q.comp p n) fun x => y) ((g ∘ f) (x + y))

Tactic:
have D :
  HasSum (fun i : Σ n, Composition n => q.compAlongComposition p i.2 fun _j => y)
    (g (f (x + y))) :=
  haveI cau :
    CauchySeq fun s : Finset (Σ n, Composition n) =>
      ∑ i ∈ s, q.compAlongComposition p i.2 fun _j => y := by
    apply cauchySeq_finset_of_norm_bounded _ (NNReal.summable_coe.2 hr) _
    simp only [coe_nnnorm, NNReal.coe_mul, NNReal.coe_pow]
    rintro ⟨n, c⟩
    calc
      ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
          ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
        apply ContinuousMultilinearMap.le_opNorm
      _ ≤ ‖compAlongComposition q p c‖ * (r : ℝ) ^ n := by
        rw [Finset.prod_const, Finset.card_fin]
        gcongr
        rw [EMetric.mem_ball, edist_zero_eq_enorm] at hy
        have := le_trans (le_of_lt hy) (min_le_right _ _)
        rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
  tendsto_nhds_of_cauchySeq_of_subseq cau compPartialSumTarget_tendsto_atTop C

Result:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ EMetric.ball x δ → f z ∈ insert (f x) t ∩ EMetric.ball (f x) rg
rf' : ℝ≥0∞ := rf ⊓ δ
min_pos : 0 < rf' ⊓ ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ EMetric.ball 0 (rf' ⊓ ↑r)
y_mem : y ∈ EMetric.ball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ EMetric.ball (f x) rg
A : Tendsto (fun n => (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x => y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n => q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b => y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n => ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j => y) atTop
    (𝓝 (g (f (x + y))))
D : HasSum (fun i => (q.compAlongComposition p i.snd) fun _j => y) (g (f (x + y)))
⊢ HasSum (fun n => (q.comp p n) fun x => y) ((g ∘ f) (x + y))