-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : ∀ (j : J), T2Space.{v} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
x : (j : J) → (↑(F.obj j) : Type v)
⊢ x ∈ partialSections F H ↔
    ∀ (i : FiniteDiagramArrow G) (i_1 : i ∈ H),
      Eq (α :=
        (↑(F.obj
              (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                  (_ : Y ∈ G) ×' (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
          Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                (F.map
                  (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).snd (β := fun (Y : J) ↦
                            (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                              (_ : Y ∈ G) ×'
                                (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)).snd
                        (β :=
                        fun (x : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ↦
                        (_ :
                          i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                              fun (Y : J) ↦
                              (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                (_ : Y ∈ G) ×'
                                  (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)) ∈
                            G) ×'
                          (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                            i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                              fun (Y : J) ↦
                              (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                (_ : Y ∈ G) ×'
                                  (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                    Y)))).snd
                    (β :=
                    fun
                      (x :
                        i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                            fun (Y : J) ↦
                            (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                              (_ : Y ∈ G) ×'
                                (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)) ∈
                          G) ↦
                    i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                      i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                        fun (Y : J) ↦
                        (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                          (_ : Y ∈ G) ×'
                            (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))))) :
              (a : (↑(F.obj i.fst) : Type v)) → (↑(F.obj i.snd.fst) : Type v))
            (x (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)))) :
          (↑(F.obj
                (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                  (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                    (_ : Y ∈ G) ×'
                      (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
            Type v))
        (x
            (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
              (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                (_ : Y ∈ G) ×' (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))) :
          (↑(F.obj
                (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                  (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                    (_ : Y ∈ G) ×'
                      (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
            Type v))

Tactic:
rfl