The data type changed

Stream: lean4

[SHAO YU]

lemma explore_01 (n k m l:ℕ )(x: ℝ )(h₁: m ≤ n)(h₂: k ≤ m)(h₃:m=2*l)(h₄: k ≤ n):
((1+x)^n)*((1-x)^n)= ∑ m in range (2*n+1),(∑ k in range (m+1),(n.choose k)* n.choose (m-k) * ((-1):ℝ )^ k )* x^m  := by
  have _01 (x : ℝ ) : ( 1 + x ) ^ n = ∑ k in range ( n + 1 ),( n.choose k )* x ^ k := by
    rw [cast_id n]
    rw [add_comm,add_pow]
    rw [Finset.sum_congr];simp
    intro k hk
    simp;
    rw[mul_comm]

The data type of n changed from N to R, causing some strategies to use cast_id, but reported wrong, what should I do?