no goals
F : Type ?u.124488
α : Type u_1
β : Type u_2
γ : Type ?u.124497
δ : Type ?u.124500
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ ∀ (a : α), ↑f a = ↑g a
convert FunLike.ext_iff.1 h using 0