no goals
S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval k (pochhammer ℕ n)) = eval (↑k) (pochhammer S n)
rw [← pochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S), eval₂_at_nat_cast,
  Nat.cast_id, eq_natCast]