case h
F : Type ?u.74354
α : Type u_1
β : Type u_2
γ : Type ?u.74363
δ : Type ?u.74366
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ ↑{ toMonoidHom := ↑f, monotone' := h } a✝ = ↑f a✝
F : Type ?u.74354
α : Type u_1
β : Type u_2
γ : Type ?u.74363
δ : Type ?u.74366
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g f : α →*o β
h : Monotone (↑↑f).toFun
⊢ { toMonoidHom := ↑f, monotone' := h } = f
ext
no goals
case h
F : Type ?u.74354
α : Type u_1
β : Type u_2
γ : Type ?u.74363
δ : Type ?u.74366
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ ↑{ toMonoidHom := ↑f, monotone' := h } a✝ = ↑f a✝
rfl