-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
inl : IsEmpty J → (partialSections F H).Nonempty
inr inr₁ : Nonempty J → (partialSections F H).Nonempty
inr₂ : Nonempty J → ∀ (this : IsCofiltered J), (partialSections F H).Nonempty
h₁ :
  Nonempty J →
    ∀ (this : IsCofiltered J),
      (fun (j : J) ↦
          if hj : j ∈ G then
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                  F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
                (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj j) : Type v))
              (Nonempty.some ⋯)
          else ⋯.some) ∈
        partialSections F H
⊢ (partialSections F H).Nonempty
have h₂ : Nonempty J →
  ∀ (this : IsCofiltered J) (X Y : J) (hX : X ∈ G) (hY : Y ∈ G) (f : X ⟶ Y)
    (hf :
      PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
              (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))) ∈
        H),
    Eq (α :=
      (↑(F.obj
            (PSigma.fst (β := fun (Y_1 : J) ↦
              (_ :
                PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                    (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                      (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                        (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                          (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                  G) ×'
                (_ : Y_1 ∈ G) ×'
                  (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                      (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                        (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                          (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                            (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                    Y_1))
              (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                  (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                    (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                      (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))))) :
        Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
              F.obj
                (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                  (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                    (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                      (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                        (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))))
              (Y :=
              F.obj
                (PSigma.fst (β := fun (Y_1 : J) ↦
                  (_ :
                    PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                        (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                          (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                            (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                              (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                      G) ×'
                    (_ : Y_1 ∈ G) ×'
                      (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                          (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                            (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                              (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                        Y_1))
                  (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                    (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                      (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                        (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                          (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))))))
              (F.map
                (PSigma.snd (β :=
                  fun
                    (x :
                      PSigma.fst (β := fun (Y_1 : J) ↦
                          (_ :
                            PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                                (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                  (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                    (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                      (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                              G) ×'
                            (_ : Y_1 ∈ G) ×'
                              (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                                  (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                    (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                      (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                        (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                                Y_1))
                          (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                            (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                              (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                  (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))) ∈
                        G) ↦
                  PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                      (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                        (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                          (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                            (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                    PSigma.fst (β := fun (Y_1 : J) ↦
                      (_ :
                        PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                            (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                              (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                  (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                          G) ×'
                        (_ : Y_1 ∈ G) ×'
                          (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                              (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                  (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                    (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                            Y_1))
                      (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                        (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                          (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                            (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                              (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))))
                  (PSigma.snd (β :=
                    fun
                      (x :
                        PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                            (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                              (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                  (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                          G) ↦
                    (_ :
                      PSigma.fst (β := fun (Y_1 : J) ↦
                          (_ :
                            PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                                (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                  (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                    (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                      (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                              G) ×'
                            (_ : Y_1 ∈ G) ×'
                              (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                                  (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                    (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                      (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                        (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                                Y_1))
                          (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                            (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                              (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                  (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))) ∈
                        G) ×'
                      (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                          (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                            (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                              (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                        PSigma.fst (β := fun (Y_1 : J) ↦
                          (_ :
                            PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                                (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                  (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                    (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                      (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                              G) ×'
                            (_ : Y_1 ∈ G) ×'
                              (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                                  (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                    (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                      (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                        (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                                Y_1))
                          (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                            (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                              (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                  (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))))))
                    (PSigma.snd (β := fun (Y_1 : J) ↦
                      (_ :
                        PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                            (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                              (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                  (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                          G) ×'
                        (_ : Y_1 ∈ G) ×'
                          (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                              (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                                (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                                  (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                                    (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                            Y_1))
                      (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                        (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                          (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                            (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                              (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))))))) :
            (a : (↑(F.obj ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.fst) : Type v)) → (↑(F.obj ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.snd.fst) : Type v))
          ((fun (j : J) ↦
              (if hj : j ∈ G then
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                        (X := F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
                      (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj j) : Type v))
                    (Nonempty.some sorry)
                else sorry.some :
                (↑(F.obj j) : Type v)))
            (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
              (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                  (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                    (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))))) :
        (↑(F.obj
              (PSigma.fst (β := fun (Y_1 : J) ↦
                (_ :
                  PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                      (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                        (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                          (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                            (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                    G) ×'
                  (_ : Y_1 ∈ G) ×'
                    (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                        (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                          (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                            (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                              (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                      Y_1))
                (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                  (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                    (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                      (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                        (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))))) :
          Type v))
      ((fun (j : J) ↦
            (if hj : j ∈ G then
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                      (X := F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
                    (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj j) : Type v))
                  (Nonempty.some sorry)
              else sorry.some :
              (↑(F.obj j) : Type v)))
          (PSigma.fst (β := fun (Y_1 : J) ↦
            (_ :
              PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                  (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                    (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                      (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                        (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                G) ×'
              (_ : Y_1 ∈ G) ×'
                (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                    (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                      (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                        (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                          (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                  Y_1))
            (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
              (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                  (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                    (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))))) :
        (↑(F.obj
              (PSigma.fst (β := fun (Y_1 : J) ↦
                (_ :
                  PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                      (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                        (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                          (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                            (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ∈
                    G) ×'
                  (_ : Y_1 ∈ G) ×'
                    (PSigma.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                        (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                          (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                            (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                              (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f)))) ⟶
                      Y_1))
                (PSigma.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))
                  (PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
                    (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
                      (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
                        (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))))))) :
          Type v))
Tactic: classical
  cases isEmpty_or_nonempty J
  · exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩
  haveI : IsCofiltered J := ⟨⟩
  use fun j : J =>
    if hj : j ∈ G then F.map (IsCofiltered.infTo G H hj) (h (IsCofiltered.inf G H)).some
    else (h _).some
  rintro ⟨X, Y, hX, hY, f⟩ hf
  dsimp only
  rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]