-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ ∑ k ∈ Finset.range (n + 1 + 1),
      (PolynomialModule.comp
            (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
              ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
          (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
        ((PolynomialModule.single ℝ k : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f k s x₀)) =
    HAdd.hAdd (α := PolynomialModule ℝ E) (β := PolynomialModule ℝ E)
      (∑ k ∈ Finset.range (n + 1),
          (PolynomialModule.comp
                (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
                  ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
              (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
            ((PolynomialModule.single ℝ k : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f k s x₀)) :
        PolynomialModule ℝ E)
      ((PolynomialModule.comp
              (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
                ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
            (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
          ((PolynomialModule.single ℝ (n + 1) : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f (n + 1) s x₀)) :
        PolynomialModule ℝ E)
have rw : HAdd.hAdd (α := PolynomialModule ℝ E) (β := PolynomialModule ℝ E)
    (∑ x ∈ Finset.range (n + 1),
        (PolynomialModule.comp
              (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
                ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
            (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
          ((PolynomialModule.single ℝ x : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f x s x₀)) :
      PolynomialModule ℝ E)
    ((PolynomialModule.comp
            (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
              ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
          (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
        ((PolynomialModule.single ℝ (n + 1) : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f (n + 1) s x₀)) :
      PolynomialModule ℝ E) =
  HAdd.hAdd (α := PolynomialModule ℝ E) (β := PolynomialModule ℝ E)
    (∑ k ∈ Finset.range (n + 1),
        (PolynomialModule.comp
              (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
                ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
            (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
          ((PolynomialModule.single ℝ k : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f k s x₀)) :
      PolynomialModule ℝ E)
    ((PolynomialModule.comp
            (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
              ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
          (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
        ((PolynomialModule.single ℝ (n + 1) : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f (n + 1) s x₀)) :
      PolynomialModule ℝ E)
Tactic: rw [Finset.sum_range_succ]