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