-- 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))
⊢ Tendsto (fun z => q.partialSum z.1 z.2) (atTop ×ˢ 𝓝 (f (x + y) - f x)) (𝓝 (g (f x + (f (x + y) - f x))))

Tactic:
apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)

Result:
case hy
𝕜 : 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))
⊢ f (x + y) - f x ∈ EMetric.ball 0 rg

case h'y
𝕜 : 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))
⊢ f x + (f (x + y) - f x) ∈ insert (f x) t

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))
this : Tendsto (fun z => q.partialSum z.1 z.2) (atTop ×ˢ 𝓝 (f (x + y) - f x)) (𝓝 (g (f x + (f (x + y) - f x))))
⊢ Tendsto (fun n => q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b => y)) atTop (𝓝 (g (f (x + y))))

Tactic:
simpa using this.comp A

Result:
no goals

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
⊢ Tendsto (fun x => ∑ a ∈ Finset.Ico 1 x, (p a) fun x => y) atTop (𝓝 (f (x + y) - f x))

Tactic:
have L : ∀ᶠ n in atTop, (∑ a ∈ Finset.range n, p a fun _b ↦ y) - f x
    = ∑ a ∈ Finset.Ico 1 n, p a fun _b ↦ y := by
  rw [eventually_atTop]
  refine ⟨1, fun n hn => ?_⟩
  symm
  rw [eq_sub_iff_add_eq', Finset.range_eq_Ico, ← Hf.coeff_zero fun _i => y,
    Finset.sum_eq_sum_Ico_succ_bot hn]

Result:
𝕜 : 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
L : ∀ᶠ (n : ℕ) in atTop, (∑ a ∈ Finset.range n, (p a) fun _b => y) - f x = ∑ a ∈ Finset.Ico 1 n, (p a) fun _b => y
⊢ Tendsto (fun x => ∑ a ∈ Finset.Ico 1 x, (p a) fun x => y) atTop (𝓝 (f (x + y) - f x))