case h
α : Type u
α' : Type ?u.65611
β : Type v
β' : Type ?u.65616
γ : Type u_1
φ : Type ?u.65622
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
f : β →𝒄 γ
x✝ : β
⊢ ↑(comp f id).toOrderHom x✝ = ↑f.toOrderHom x✝
α : Type u
α' : Type ?u.65611
β : Type v
β' : Type ?u.65616
γ : Type u_1
φ : Type ?u.65622
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
f : β →𝒄 γ
⊢ comp f id = f
ext
no goals
case h
α : Type u
α' : Type ?u.65611
β : Type v
β' : Type ?u.65616
γ : Type u_1
φ : Type ?u.65622
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
f : β →𝒄 γ
x✝ : β
⊢ ↑(comp f id).toOrderHom x✝ = ↑f.toOrderHom x✝
rfl