case refine'_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj X_1 =
      (map (inclusionTopIso X).inv).obj X_1

case refine'_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).map f =
      eqToHom (_ : ?m.132552.obj X_1 = ?m.132553.obj X_1) ≫
        (map (inclusionTopIso X).inv).map f ≫
          eqToHom
            (_ :
              (map (inclusionTopIso X).inv).obj Y =
                (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj Y)
X : TopCat
⊢ IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤))) = map (inclusionTopIso X).inv
refine' CategoryTheory.Functor.ext _ _
case refine'_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).map f =
      eqToHom
          (_ :
            (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj X_1 =
              (map (inclusionTopIso X).inv).obj X_1) ≫
        (map (inclusionTopIso X).inv).map f ≫
          eqToHom
            (_ :
              (map (inclusionTopIso X).inv).obj Y =
                (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj Y)
case refine'_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj X_1 =
      (map (inclusionTopIso X).inv).obj X_1

case refine'_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).map f =
      eqToHom (_ : ?m.132552.obj X_1 = ?m.132553.obj X_1) ≫
        (map (inclusionTopIso X).inv).map f ≫
          eqToHom
            (_ :
              (map (inclusionTopIso X).inv).obj Y =
                (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj Y)
. intro U
  ext x
  exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
no goals
case refine'_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).map f =
      eqToHom
          (_ :
            (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj X_1 =
              (map (inclusionTopIso X).inv).obj X_1) ≫
        (map (inclusionTopIso X).inv).map f ≫
          eqToHom
            (_ :
              (map (inclusionTopIso X).inv).obj Y =
                (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj Y)
. intros U V f
  apply Subsingleton.elim
case refine'_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj U = (map (inclusionTopIso X).inv).obj U
case refine'_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj X_1 =
      (map (inclusionTopIso X).inv).obj X_1
intro U
case refine'_1.h.h
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
x : ↑X
⊢ x ∈ ↑((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj U) ↔
    x ∈ ↑((map (inclusionTopIso X).inv).obj U)
case refine'_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj U = (map (inclusionTopIso X).inv).obj U
ext x
no goals
case refine'_1.h.h
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
x : ↑X
⊢ x ∈ ↑((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj U) ↔
    x ∈ ↑((map (inclusionTopIso X).inv).obj U)
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
case refine'_2
X : TopCat
U V : Opens ↑((toTopCat X).obj ⊤)
f : U ⟶ V
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).map f =
    eqToHom
        (_ :
          (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj U =
            (map (inclusionTopIso X).inv).obj U) ≫
      (map (inclusionTopIso X).inv).map f ≫
        eqToHom
          (_ :
            (map (inclusionTopIso X).inv).obj V =
              (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj V)
case refine'_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).map f =
      eqToHom
          (_ :
            (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj X_1 =
              (map (inclusionTopIso X).inv).obj X_1) ≫
        (map (inclusionTopIso X).inv).map f ≫
          eqToHom
            (_ :
              (map (inclusionTopIso X).inv).obj Y =
                (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj Y)
intros U V f
no goals
case refine'_2
X : TopCat
U V : Opens ↑((toTopCat X).obj ⊤)
f : U ⟶ V
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).map f =
    eqToHom
        (_ :
          (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj U =
            (map (inclusionTopIso X).inv).obj U) ≫
      (map (inclusionTopIso X).inv).map f ≫
        eqToHom
          (_ :
            (map (inclusionTopIso X).inv).obj V =
              (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion ⊤)))).obj V)
apply Subsingleton.elim