-- 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)
this :
  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))}
rw :
  IsClosed (X := (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))})
⊢ IsClosed (partialSections F H)

Tactic:
rw [this]