-- 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : (↑r' : ℝ≥0∞) < r
hr'0 : 0 < r'
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / (↑r' : ℝ) ^ n
L : E × E → ℝ :=
  fun (y : E × E) ↦
    C * HPow.hPow (β := ℕ) (a / (↑r' : ℝ)) 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) *
      (a / HPow.hPow (β := ℕ) (1 - a) 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) (↑r' : ℝ≥0∞)
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F :=
  fun (n : ℕ) ↦
    HSub.hSub (α := F) (β := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.1 - x : F)
      ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y.2 - x : F)
h :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      (∑ x_1 ∈ Finset.range 1,
          HSub.hSub (α := F) (β := F) ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.1 - x : F)
            ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x_2 : Fin x_1) ↦ y.2 - x : F) +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
h₁ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      (HSub.hSub (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.1 - x : F)
          ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.2 - x : F) +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
h₂ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      (HSub.hSub (β := F) (f x) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y.2 - x : F) +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
h₃ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      (f x - f x +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
h₄ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      (0 +
        HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
          ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F))
h₅ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      HSub.hSub (α := F) (β := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.1 - x : F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F)
h₆ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      HSub.hSub (α := F) (β := F)
        ((p 1 : (a : (i : Fin 1) → E) → F) (Pi.single (M := fun (x : Fin 1) ↦ E) 0 (y.1 - x)) : F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F)
h₇ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      HSub.hSub (α := F) (β := F)
        ((p 1 : (a : (i : Fin 1) → E) → F) (Function.update (β := fun (x : Fin 1) ↦ E) 0 0 (y.1 - x)) : F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x_1 : Fin 1) ↦ y.2 - x : F)
h₈ :
  HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      HSub.hSub (α := F) (β := F)
        ((p 1 : (a : (i : Fin 1) → E) → F) (Function.update (β := fun (x : Fin 1) ↦ E) 0 0 (y.1 - x)) : F)
        ((p 1 : (a : (i : Fin 1) → E) → F) (Pi.single (M := fun (x : Fin 1) ↦ E) 0 (y.2 - x)) : F)
⊢ HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
    f y.1 - f y.2 -
      ∑ i ∈ Finset.range 2,
        HSub.hSub (α := F) (β := F) ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.1 - x : F)
          ((p i : (a : (i : Fin i) → E) → F) fun (x_1 : Fin i) ↦ y.2 - x : F)
have h₉ : HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F) =
  f y.1 - f y.2 -
    HSub.hSub (α := F) (β := F)
      ((p 1 : (a : (i : Fin 1) → E) → F) (Function.update (β := fun (x : Fin 1) ↦ E) 0 0 (y.1 - x)) : F)
      ((p 1 : (a : (i : Fin 1) → E) → F) (Function.update (β := fun (x : Fin 1) ↦ E) 0 0 (y.2 - x)) : F)
Tactic: rw [Finset.sum_range_succ, Finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
        zero_add, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single,
        ← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x), Pi.single, ← (p 1).map_update_sub,
        ← Pi.single, Subsingleton.pi_single_eq, sub_sub_sub_cancel_right]