[GOAL]
α β : PreordCat
e : ↑α ≃o ↑β
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PreordCat
e : ↑α ≃o ↑β
x : (forget PreordCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x = ↑(𝟙 α) x
[PROOFSTEP]
exact e.symm_apply_apply x
[GOAL]
α β : PreordCat
e : ↑α ≃o ↑β
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PreordCat
e : ↑α ≃o ↑β
x : (forget PreordCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x = ↑(𝟙 β) x
[PROOFSTEP]
exact e.apply_symm_apply x
[GOAL]
X✝ Y✝ : PreordCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordCatToCat.map a₁✝ = preordCatToCat.map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext x
[GOAL]
case w
X✝ Y✝ : PreordCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordCatToCat.map a₁✝ = preordCatToCat.map a₂✝
x : (forget PreordCat).obj X✝
⊢ ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
exact Functor.congr_obj h x
