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