no goals
F : Type ?u.86859
α : Type u_2
β : Type u_1
γ : Type ?u.86868
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
f : α →+* β
x✝ y : α
h : ↑f 1 = 0
x : α
⊢ ↑f x = 0
rw [← mul_one x, map_mul, h, mul_zero]