-- 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
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 ⋯)
                  else ⋯.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 ⋯)
                else ⋯.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))
⊢ (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 Y) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj X) : Type v)) → (↑(F.obj Y) : Type v))
          (if hj : X ∈ 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 X) : Type v))
              (Nonempty.some sorry)
          else sorry.some) :
        (↑(F.obj Y) : Type v))
      (if hj : Y ∈ 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 Y) : Type v))
            (Nonempty.some sorry)
        else sorry.some :
        (↑(F.obj Y) : 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]