-- Mathlib/Analysis/Analytic/Inverse.lean
lemma HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp
    {f : E → G} {q : FormalMultilinearSeries 𝕜 F G}
    {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    (hf : HasFPowerSeriesAt f (q.comp p) x) (hq : 0 < q.radius) (hp : 0 < p.radius) :
    ∀ᶠ y in 𝓝 0, Tendsto (fun (a : ℕ × ℕ) ↦ q.partialSum a.1 (p.partialSum a.2 y
      - p 0 (fun _ ↦ 0))) atTop (𝓝 (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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 (f (x + y)))

Tactic:
rcases q.comp_summable_nnreal p hq hp with ⟨r1, r1_pos : 0 < r1, hr1⟩

Result:
case 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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 (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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := r0 ⊓ ↑r1
this : EMetric.ball 0 r ∈ 𝓝 0
y : E
hy : y ∈ EMetric.ball 0 r
hy0 : y ∈ EMetric.ball 0 r0
n : ℕ
c : Composition n
⊢ ‖(q.compAlongComposition p c) fun _j => y‖ ≤ ‖q.compAlongComposition p c‖ * ∏ _j : Fin n, ‖y‖

Tactic:
apply ContinuousMultilinearMap.le_opNorm

Result:
no goals

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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := r0 ⊓ ↑r1
this : EMetric.ball 0 r ∈ 𝓝 0
y : E
hy : y ∈ EMetric.ball 0 r
hy0 : y ∈ EMetric.ball 0 r0
A : HasSum (fun i => (q.compAlongComposition p i.snd) fun _j => y) (f (x + y))
B :
  Tendsto (fun n => ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j => y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n => q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b => y)) atTop (𝓝 (f (x + y)))
⊢ ∀ a ∈ Set.Ici (0, 1),
    q.partialSum a.1 (∑ a ∈ Ico 1 a.2, (p a) fun _b => y) = q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)

Tactic:
rintro ⟨-, n⟩ ⟨-, (hn : 1 ≤ n)⟩

Result:
case h.mk.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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := r0 ⊓ ↑r1
this : EMetric.ball 0 r ∈ 𝓝 0
y : E
hy : y ∈ EMetric.ball 0 r
hy0 : y ∈ EMetric.ball 0 r0
A : HasSum (fun i => (q.compAlongComposition p i.snd) fun _j => y) (f (x + y))
B :
  Tendsto (fun n => ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j => y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n => q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b => y)) atTop (𝓝 (f (x + y)))
fst✝ n : ℕ
hn : 1 ≤ n
⊢ q.partialSum (fst✝, n).1 (∑ a ∈ Ico 1 (fst✝, n).2, (p a) fun _b => y) =
    q.partialSum (fst✝, n).1 (p.partialSum (fst✝, n).2 y - (p 0) fun x => 0)

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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := r0 ⊓ ↑r1
this : EMetric.ball 0 r ∈ 𝓝 0
y : E
hy : y ∈ EMetric.ball 0 r
hy0 : y ∈ EMetric.ball 0 r0
⊢ ∀ (i : (n : ℕ) × Composition n),
    ‖(q.compAlongComposition p i.snd) fun _j => y‖ ≤ ‖q.compAlongComposition p i.snd‖ * ↑r1 ^ i.fst

Tactic:
rintro ⟨n, c⟩

Result:
case mk
𝕜 : 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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := r0 ⊓ ↑r1
this : EMetric.ball 0 r ∈ 𝓝 0
y : E
hy : y ∈ EMetric.ball 0 r
hy0 : y ∈ EMetric.ball 0 r0
n : ℕ
c : Composition n
⊢ ‖(q.compAlongComposition p ⟨n, c⟩.snd) fun _j => y‖ ≤ ‖q.compAlongComposition p ⟨n, c⟩.snd‖ * ↑r1 ^ ⟨n, c⟩.fst

Proof state:
case hab
𝕜 : 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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := r0 ⊓ ↑r1
this : EMetric.ball 0 r ∈ 𝓝 0
y : E
hy : ‖y‖ₑ < r
hy0 : y ∈ EMetric.ball 0 r0
n : ℕ
c : Composition n
⊢ ‖y‖ ≤ ↑r1

Tactic:
have := le_trans (le_of_lt hy) (min_le_right _ _)

Result:
case hab
𝕜 : 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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := r0 ⊓ ↑r1
this✝ : EMetric.ball 0 r ∈ 𝓝 0
y : E
hy : ‖y‖ₑ < r
hy0 : y ∈ EMetric.ball 0 r0
n : ℕ
c : Composition n
this : ‖y‖ₑ ≤ ↑r1
⊢ ‖y‖ ≤ ↑r1