-- 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 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
⊢ HasSum (fun n => (q n) fun x_1 => f (x + y) - f x) (g (f (x + y)))

Tactic:
have L : Tendsto (fun n ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y)))) := by
  apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2
  rintro u ⟨hu, u_closed⟩
  simp only [id_eq, eventually_atTop, ge_iff_le]
  rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
  obtain ⟨a₀, b₀, hab⟩ : ∃ a₀ b₀, ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b →
      q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0) ∈ v := by
    simpa using hy (v_open.mem_nhds hv)
  refine ⟨a₀, fun a ha ↦ ?_⟩
  have : Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0)) atTop
      (𝓝 (q.partialSum a (f (x + y) - f x))) := by
    have : ContinuousAt (q.partialSum a) (f (x + y) - f x) :=
      (partialSum_continuous q a).continuousAt
    apply this.tendsto.comp
    apply Tendsto.sub h'y
    convert tendsto_const_nhds
    exact (HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm
  apply u_closed.mem_of_tendsto this
  filter_upwards [Ici_mem_atTop b₀] with b hb using vu (hab _ _ ha hb)

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))))
⊢ HasSum (fun n => (q n) fun x_1 => 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
A : ContinuousAt (fun y => f (x + y) - f x) 0
⊢ ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius

Tactic:
have B : EMetric.ball 0 q.radius ∈ 𝓝 (f (x + 0) - f x) := by
  simpa using EMetric.ball_mem_nhds _ hq

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

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))))
⊢ CauchySeq fun s => ∑ n ∈ s, (q n) fun x_1 => f (x + y) - f x

Tactic:
have Z := q.summable_norm_apply (x := f (x + y) - f x) h''y

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
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

Proof state:
case h.e'_5.h.e'_3
𝕜 : 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)
⊢ f x = (p 0) fun x => 0

Tactic:
exact (HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm

Result:
no goals