-- 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)
h :
  ∀ (x : (j : J) → (↑(F.obj j) : Type v)),
    x ∈ partialSections F H ↔
      Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type v)))
        (⋂ f ∈ H,
          {u : (j : J) → (↑(F.obj j) : Type v) |
            Eq (α :=
              (↑(F.obj
                    (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                      (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                        (_ : Y ∈ G) ×'
                          (f.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
                        (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).snd (β :=
                                  fun (Y : J) ↦
                                  (_ :
                                    f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                    (_ : Y ∈ G) ×'
                                      (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                        Y)).snd
                              (β :=
                              fun
                                (x : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ↦
                              (_ :
                                f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                    fun (Y : J) ↦
                                    (_ :
                                      f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈
                                        G) ×'
                                      (_ : Y ∈ G) ×'
                                        (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                          Y)) ∈
                                  G) ×'
                                (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                  f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                    fun (Y : J) ↦
                                    (_ :
                                      f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈
                                        G) ×'
                                      (_ : Y ∈ G) ×'
                                        (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                          Y)))).snd
                          (β :=
                          fun
                            (x :
                              f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                  fun (Y : J) ↦
                                  (_ :
                                    f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                    (_ : Y ∈ G) ×'
                                      (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                        Y)) ∈
                                G) ↦
                          f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                            f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                              fun (Y : J) ↦
                              (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                (_ : Y ∈ G) ×'
                                  (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                    Y))))) :
                    (a : (↑(F.obj f.fst) : Type v)) → (↑(F.obj f.snd.fst) : Type v))
                  (u (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)))) :
                (↑(F.obj
                      (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                        fun (Y : J) ↦
                        (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                          (_ : Y ∈ G) ×'
                            (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
                  Type v))
              (u
                  (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                    (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                      (_ : Y ∈ G) ×'
                        (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))) :
                (↑(F.obj
                      (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                        fun (Y : J) ↦
                        (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                          (_ : Y ∈ G) ×'
                            (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
                  Type v))})
        x
⊢ partialSections F H =
    ⋂ f ∈ H,
      {u : (j : J) → (↑(F.obj j) : Type v) |
        Eq (α :=
          (↑(F.obj
                (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                  (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                    (_ : Y ∈ G) ×'
                      (f.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
                    (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).snd (β := fun (Y : J) ↦
                              (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                (_ : Y ∈ G) ×'
                                  (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)).snd
                          (β :=
                          fun (x : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ↦
                          (_ :
                            f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                fun (Y : J) ↦
                                (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                  (_ : Y ∈ G) ×'
                                    (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)) ∈
                              G) ×'
                            (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                              f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                fun (Y : J) ↦
                                (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                  (_ : Y ∈ G) ×'
                                    (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                      Y)))).snd
                      (β :=
                      fun
                        (x :
                          f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                              fun (Y : J) ↦
                              (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                (_ : Y ∈ G) ×'
                                  (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)) ∈
                            G) ↦
                      f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                        f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                          fun (Y : J) ↦
                          (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                            (_ : Y ∈ G) ×'
                              (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))))) :
                (a : (↑(F.obj f.fst) : Type v)) → (↑(F.obj f.snd.fst) : Type v))
              (u (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)))) :
            (↑(F.obj
                  (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                    (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                      (_ : Y ∈ G) ×'
                        (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
              Type v))
          (u
              (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                  (_ : Y ∈ G) ×' (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))) :
            (↑(F.obj
                  (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                    (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                      (_ : Y ∈ G) ×'
                        (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
              Type v))}

Tactic:
ext1