How to prove HasDerivAt (1 + x)^n at x

Stream: lean4

[shi shuming]

I want to use intervalIntegral.integral_mul_deriv_eq_deriv_mul theorem to convert one integral into another, but this theorem requires proving that hasDerivAt f f' x, f x is (1 + x) ^ (n + 1). I can only prove that hasDerivAt x ^ (n + 1) x is (n + 1) * x ^ n, but this does not match the proof goal.

import Mathlib

open Nat

open Finset

open BigOperators
open Polynomial
open Algebra
open Real


theorem integral_u_v(n:ℕ) : ∫ (x : ℝ) in (0:ℝ )..1, x * ((1 + x) ^ n) = 1 * ((1 + 1) ^ (n + 1) / (n + 1)) - 0 * ((1 + 0) ^ (n + 1) / (n + 1)) - ∫ (x : ℝ) in (0:ℝ )..1, 1 * ((1 + x) ^ (n + 1) / (n + 1)):= by
  let u : ℝ -> ℝ := (fun x => x)
  let v : ℝ -> ℝ := fun x => (1 + x) ^ (n + 1) / (n + 1)

  let u' : ℝ -> ℝ  := (fun x => 1)
  let v' : ℝ -> ℝ  := fun x => (1 + x) ^ n
  rw [@intervalIntegral.integral_mul_deriv_eq_deriv_mul ℝ 0 1 _ _ _ u v u' v']
  ·
    intro x hx
    exact hasDerivAt_id' x
  ·
    intro x hx
    unfold v'
    unfold v
    sorry
  ·
    unfold u'
    simp
  ·
    unfold v'
    sorry