-- Mathlib/Analysis/Analytic/Inverse.lean
lemma HasFPowerSeriesAt.eventually_hasSum_of_comp  {f : E → F} {g : F → G}
    {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    (hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x) (hf : HasFPowerSeriesAt f p x)
    (hq : 0 < q.radius) :
    ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => q n fun _ : Fin n => (f (x + y) - f x)) (g (f (x + y)))

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed u
v : Set G
vu : v ⊆ u
v_open : IsOpen v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x => 0) ∈ v
a : ℕ
ha : a₀ ≤ a
⊢ Tendsto (fun b => q.partialSum a (p.partialSum b y - (p 0) fun x => 0)) atTop (𝓝 (q.partialSum a (f (x + y) - f x)))

Tactic:
have : ContinuousAt (q.partialSum a) (f (x + y) - f x) :=
  (partialSum_continuous q a).continuousAt

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this✝ : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed u
v : Set G
vu : v ⊆ u
v_open : IsOpen v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x => 0) ∈ v
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ Tendsto (fun b => q.partialSum a (p.partialSum b y - (p 0) fun x => 0)) atTop (𝓝 (q.partialSum a (f (x + y) - f x)))

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
L : Tendsto (fun n => q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
Z : Summable fun n => ‖(q n) fun x_1 => f (x + y) - f x‖
⊢ CauchySeq fun s => ∑ n ∈ s, (q n) fun x_1 => f (x + y) - f x

Tactic:
exact cauchySeq_finset_of_norm_bounded _ Z (fun i ↦ le_rfl)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
⊢ ∀ (i : Set G),
    i ∈ 𝓝 (g (f (x + y))) ∧ IsClosed i → ∀ᶠ (x_1 : ℕ) in atTop, q.partialSum x_1 (f (x + y) - f x) ∈ _root_.id i

Tactic:
rintro u ⟨hu, u_closed⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed u
⊢ ∀ᶠ (x_1 : ℕ) in atTop, q.partialSum x_1 (f (x + y) - f x) ∈ _root_.id u

Proof state:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
L : Tendsto (fun n => q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
⊢ HasSum (fun n => (q n) fun x_1 => f (x + y) - f x) (g (f (x + y)))

Tactic:
have C : CauchySeq (fun (s : Finset ℕ) ↦ ∑ n ∈ s, q n fun _ : Fin n => (f (x + y) - f x)) := by
  have Z := q.summable_norm_apply (x := f (x + y) - f x) h''y
  exact cauchySeq_finset_of_norm_bounded _ Z (fun i ↦ le_rfl)

Result:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
L : Tendsto (fun n => q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
C : CauchySeq fun s => ∑ n ∈ s, (q n) fun x_1 => f (x + y) - f x
⊢ HasSum (fun n => (q n) fun x_1 => f (x + y) - f x) (g (f (x + y)))