no goals
α : Type ?u.60026
β : Type ?u.60029
R : Type u_1
S : Type u_3
F : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
n : ℕ
h✝ : NeZero ↑n
inst✝ : RingHomClass F R S
f : F
hf : Function.Injective ↑f
h : ↑n = 0
⊢ ↑f ↑n = ↑f 0
simpa only [map_natCast, map_zero f]