hasseDerivative and ring homomorphis

Stream: lean4

[Sham S]

lemma map_hasseDeriv_commutativity
    (P : K[X]) (i : ℕ): (P.map f).hasseDeriv i = (P.hasseDeriv i).map f := by
    ext n
    simp only [hasseDeriv_apply, coeff_map]

post this I'm unable to proceed, I'm new to lean and would like some help how to go from here