[GOAL]
⊢ ConcreteCategory FrmCat
[PROOFSTEP]
unfold FrmCat
[GOAL]
⊢ ConcreteCategory (Bundled Frame)
[PROOFSTEP]
infer_instance
[GOAL]
α β : FrmCat
e : ↑α ≃o ↑β
⊢ {
        toInfTopHom :=
          { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
      {
        toInfTopHom :=
          {
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : FrmCat
e : ↑α ≃o ↑β
x✝ : (forget FrmCat).obj α
⊢ ↑({
            toInfTopHom :=
              { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
                map_top' := (_ : ↑e ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
          {
            toInfTopHom :=
              {
                toInfHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_inf' :=
                      (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
                map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : FrmCat
e : ↑α ≃o ↑β
⊢ {
        toInfTopHom :=
          {
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
      {
        toInfTopHom :=
          { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : FrmCat
e : ↑α ≃o ↑β
x✝ : (forget FrmCat).obj β
⊢ ↑({
            toInfTopHom :=
              {
                toInfHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_inf' :=
                      (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
                map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
          {
            toInfTopHom :=
              { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
                map_top' := (_ : ↑e ⊤ = ⊤) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
