-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A_1 : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
A : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
I :
  ∀ (w : E) (hw : ‖w‖₊ < r'),
    norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ w) ≤ ε / 4
n₁ :
  ‖HSub.hSub (α := F) (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
        (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)‖ =
    ‖HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
        HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)‖
n₂ :
  ‖HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) -
        HAdd.hAdd (α := F) (∑ i ∈ Finset.range k, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)
          (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y)‖ =
    ‖(p.partialSum k z - p.partialSum k y +
          ∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
        -∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y‖
n₃ :
  ‖p.partialSum k z - p.partialSum k y‖ +
        norm.{u_3} (E := F) (∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ z) +
      norm.{u_3} (E := F) (-∑ i ∈ Finset.Ico k n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) ≤
    ε / 4 + ε / 4 + ε / 4
⊢ ‖p.partialSum n z - p.partialSum n y‖ < ε
have n₄ : ε / 4 + ε / 4 + ε / 4 < ε
Tactic: calc
  ‖p.partialSum n z - p.partialSum n y‖
  _ = ‖∑ i ∈ range n, p i (fun _ ↦ z) - ∑ i ∈ range n, p i (fun _ ↦ y)‖ := rfl
  _ = ‖(∑ i ∈ range k, p i (fun _ ↦ z) + ∑ i ∈ Ico k n, p i (fun _ ↦ z))
        - (∑ i ∈ range k, p i (fun _ ↦ y) + ∑ i ∈ Ico k n, p i (fun _ ↦ y))‖ := by
    simp [sum_range_add_sum_Ico _ hkn]
  _ = ‖(p.partialSum k z - p.partialSum k y) + (∑ i ∈ Ico k n, p i (fun _ ↦ z))
        + (- ∑ i ∈ Ico k n, p i (fun _ ↦ y))‖ := by
    congr 1
    simp only [FormalMultilinearSeries.partialSum]
    abel
  _ ≤ ‖p.partialSum k z - p.partialSum k y‖ + ‖∑ i ∈ Ico k n, p i (fun _ ↦ z)‖
      + ‖- ∑ i ∈ Ico k n, p i (fun _ ↦ y)‖ := norm_add₃_le
  _ ≤ ε / 4 + ε / 4 + ε / 4 := by
    gcongr
    · exact I _ h'z
    · simp only [norm_neg]; exact I _ yr'
  _ < ε := by linarith