[GOAL]
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
x✝ : (forget BddOrdCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x✝ = ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
x✝ : (forget BddOrdCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x✝ = ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
