no goals
α : Type ?u.62486
β : Type ?u.62489
R✝ : Type ?u.62492
S✝ : Type ?u.62495
F✝ : Type ?u.62498
inst✝⁴ : NonAssocSemiring R✝
inst✝³ : NonAssocSemiring S✝
R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
F : Type u_3
inst✝ : RingHomClass F R S
f : F
n : ℕ
hn : NeZero ↑n
⊢ NeZero (↑f ↑n)
simp only [map_natCast, hn]