[GOAL]
α β : PartOrdCat
e : ↑α ≃o ↑β
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PartOrdCat
e : ↑α ≃o ↑β
x : (forget PartOrdCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x = ↑(𝟙 α) x
[PROOFSTEP]
exact e.symm_apply_apply x
[GOAL]
α β : PartOrdCat
e : ↑α ≃o ↑β
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PartOrdCat
e : ↑α ≃o ↑β
x : (forget PartOrdCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x = ↑(𝟙 β) x
[PROOFSTEP]
exact e.apply_symm_apply x
[GOAL]
X : PreordCat
⊢ { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
            map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
        X)
[PROOFSTEP]
ext x
[GOAL]
case w
X : PreordCat
x :
  (forget PartOrdCat).obj
    ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
      X)
⊢ ↑({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
              map := fun {X Y} f => OrderHom.antisymmetrization f }.map
          (𝟙 X))
      x =
    ↑(𝟙
          ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
                map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
            X))
      x
[PROOFSTEP]
exact Quotient.inductionOn' x fun x => Quotient.map'_mk'' _ (fun a b => id) _
[GOAL]
X✝ Y✝ Z✝ : PreordCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.map
      (f ≫ g) =
    { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
            map := fun {X Y} f => OrderHom.antisymmetrization f }.map
        f ≫
      { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
            map := fun {X Y} f => OrderHom.antisymmetrization f }.map
        g
[PROOFSTEP]
ext x
[GOAL]
case w
X✝ Y✝ Z✝ : PreordCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x :
  (forget PartOrdCat).obj
    ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
      X✝)
⊢ ↑({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
              map := fun {X Y} f => OrderHom.antisymmetrization f }.map
          (f ≫ g))
      x =
    ↑({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
                map := fun {X Y} f => OrderHom.antisymmetrization f }.map
            f ≫
          { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
                map := fun {X Y} f => OrderHom.antisymmetrization f }.map
            g)
      x
[PROOFSTEP]
exact Quotient.inductionOn' x fun x => OrderHom.antisymmetrization_apply_mk _ _
