-- 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:
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
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u

Tactic:
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩

Result:
case intro.intro.intro.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
v : Set G
vu : v ⊆ u
v_open : IsOpen v
hv : g (f (x + y)) ∈ v
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u

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

Tactic:
apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2

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
⊢ ∀ (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

Proof state:
case intro.intro.intro.intro.intro.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
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 :
  Tendsto (fun b => q.partialSum a (p.partialSum b y - (p 0) fun x => 0)) atTop (𝓝 (q.partialSum a (f (x + y) - f x)))
⊢ q.partialSum a (f (x + y) - f x) ∈ u

Tactic:
apply u_closed.mem_of_tendsto this

Result:
case intro.intro.intro.intro.intro.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
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 :
  Tendsto (fun b => q.partialSum a (p.partialSum b y - (p 0) fun x => 0)) atTop (𝓝 (q.partialSum a (f (x + y) - f x)))
⊢ ∀ᶠ (x : ℕ) in atTop, q.partialSum a (p.partialSum x y - (p 0) fun x => 0) ∈ u

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
A : ContinuousAt (fun y => f (x + y) - f x) 0
⊢ EMetric.ball 0 q.radius ∈ 𝓝 (f (x + 0) - f x)

Tactic:
simpa using EMetric.ball_mem_nhds _ hq

Result:
no goals