[GOAL]
⊢ ConcreteCategory CompleteLatCat
[PROOFSTEP]
dsimp [CompleteLatCat]
[GOAL]
⊢ ConcreteCategory (Bundled CompleteLattice)
[PROOFSTEP]
infer_instance
[GOAL]
α β : CompleteLatCat
e : ↑α ≃o ↑β
⊢ { tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
      {
        tosInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : CompleteLatCat
e : ↑α ≃o ↑β
x✝ : (forget CompleteLatCat).obj α
⊢ ↑({ tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
          {
            tosInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : CompleteLatCat
e : ↑α ≃o ↑β
⊢ {
        tosInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
      { tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : CompleteLatCat
e : ↑α ≃o ↑β
x✝ : (forget CompleteLatCat).obj β
⊢ ↑({
            tosInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
          { tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
