[GOAL]
α β : SemilatSupCat
e : α.X ≃o β.X
⊢ { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_bot' := (_ : ↑e ⊥ = ⊥) } ≫
      {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatSupCat
e : α.X ≃o β.X
x✝ : (forget SemilatSupCat).obj α
⊢ ↑({ toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_bot' := (_ : ↑e ⊥ = ⊥) } ≫
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : SemilatSupCat
e : α.X ≃o β.X
⊢ {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) } ≫
      { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_bot' := (_ : ↑e ⊥ = ⊥) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatSupCat
e : α.X ≃o β.X
x✝ : (forget SemilatSupCat).obj β
⊢ ↑({
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) } ≫
          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_bot' := (_ : ↑e ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
[GOAL]
α β : SemilatInfCat
e : α.X ≃o β.X
⊢ { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
        map_top' := (_ : ↑e ⊤ = ⊤) } ≫
      {
        toInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_inf' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatInfCat
e : α.X ≃o β.X
x✝ : (forget SemilatInfCat).obj α
⊢ ↑({ toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) } ≫
          {
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : SemilatInfCat
e : α.X ≃o β.X
⊢ {
        toInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_inf' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) } ≫
      { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
        map_top' := (_ : ↑e ⊤ = ⊤) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatInfCat
e : α.X ≃o β.X
x✝ : (forget SemilatInfCat).obj β
⊢ ↑({
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) } ≫
          { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
