no goals
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv 1) f = ↑derivative f
simp only [hasseDeriv_apply, derivative_apply, ← C_mul_X_pow_eq_monomial, Nat.choose_one_right,
  (Nat.cast_commute _ _).eq]