X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj
      ((map (inclusion U)).obj ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V)) =
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj
      ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V) =
    (𝟭 (Opens ↑X)).obj ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V)
dsimp
no goals
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj
      ((map (inclusion U)).obj ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V)) =
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V
rw [map_functor_eq V]
no goals
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (IsOpenMap.adjunction (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).counit.app
      ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V) =
    eqToHom
      (_ :
        (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj
            ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V) =
          (𝟭 (Opens ↑X)).obj ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj V))
apply Subsingleton.elim