-- 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))}
f : FiniteDiagramArrow G
h_1 : f ∈ (↑H : Set (FiniteDiagramArrow G))
h :
  Continuous (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))
    fun (y : (j : J) → (↑(F.obj j) : 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))
      (y (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y))))
h₁ :
  Continuous (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))
    fun (y : (j : J) → (↑(F.obj j) : Type v)) ↦
    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)))
⊢ IsClosed (X := (j : J) → (↑(F.obj j) : Type v))
    {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:
apply isClosed_eq

Premises used: isClosed_eq