[GOAL]
ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
j : ι
⊢ ↑(Pi.evalRingHom (fun x => R) j) ↑x = 0
[PROOFSTEP]
rw [map_natCast, h]
[GOAL]
ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
⊢ ↑(Pi.evalRingHom (fun x => R) i) ↑x = 0
[PROOFSTEP]
rw [h, RingHom.map_zero]
