The deriv of tsum?

Stream: mathlib4

[SHAO YU]

import Mathlib

open Nat
open Real
open Finset
open Finsupp
open BigOperators
open PowerSeries
open MeasureTheory
lemma Step2(n k:ℕ)(x:ℝ )(hk:k=n)(hx1:x≥ 0)(hx2:x<1):deriv (fun (x:ℝ) => ∑' (n:ℕ ),(2*n).choose n *(1/(n+1)) *x^(n+1)) x
      = (∑' (n:ℕ ),(2*n).choose n *x^n ) :=by
  --let k := n
  rw [deriv_tsum]
  sorry

How to compelete the sorry?

[Johan Commelin]

I have cleaned up the statement a bit

import Mathlib

lemma Step2 (n : ℕ) (x : ℝ) (hx1 : x ≥ 0) (hx2 : x < 1) :
    deriv (fun (x:ℝ) ↦ ∑' (n:ℕ), (2*n).choose n * (1/(n+1)) * x^(n+1)) x = (∑' (n:ℕ), (2*n).choose n * x^n) := by
  rw [deriv_tsum]
  sorry

[Johan Commelin]

Note that you have 7 goals, not just 1.