no goals
F : Type ?u.88572
α : Type u_2
β : Type u_1
γ : Type ?u.88581
x✝³ : NonAssocSemiring α
x✝² : NonAssocSemiring β
f : α →+* β
x✝¹ y✝ : α
h : ∀ (x : α), ↑f x = 0
y : β
x✝ : y ∈ Set.range ↑f
x : α
hx : ↑f x = y
⊢ y ∈ {0}
simp [← hx, h x]
no goals
F : Type ?u.88572
α : Type u_2
β : Type u_1
γ : Type ?u.88581
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
x y✝ : α
h : ∀ (x : α), ↑f x = 0
y : β
hy : y ∈ {0}
⊢ ↑f 0 = y
simpa using hy.symm