-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hC : IsLimit C
hU : IsClopen U
S : Set (Set (↑(toTopCat.mapCone C).pt : Type (max u v)))
hS :
  S ⊆
    {U : Set (↑(toTopCat.mapCone C).pt : Type (max u v)) |
      ∃ (j : J) (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))),
        Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))))
            ((fun (j : J) ↦
                ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                  Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
              j)
            V ∧
          U =
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                    TopCat.carrier) ((toTopCat.mapCone C).π.app j)) :
                (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj j) : Type (max u v))) →
                  (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
              V}
h : U = ⋃₀ S
j : (↑S : Type (max u v)) → J :=
  fun (s : (↑S : Type (max u v))) ↦
    Exists.choose (p := fun (j : J) ↦
      ∃ (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))),
        Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))))
            ((fun (j : J) ↦
                ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                  Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
              j)
            V ∧
          (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                    TopCat.carrier) ((toTopCat.mapCone C).π.app j)) :
                (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj j) : Type (max u v))) →
                  (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
              V)
      ⋯
V : (s : (↑S : Type (max u v))) →
  Set
    (↑((F.obj (j s)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max u v)) :=
  fun (s : (↑S : Type (max u v))) ↦
    ⋯.choose (p :=
      fun
        (V :
          Set
            (↑((F ⋙ toTopCat).obj
                  (Exists.choose (p := fun (j : J) ↦
                    ∃ (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))),
                      Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))))
                          ((fun (j : J) ↦
                              ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                                Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
                            j)
                          V ∧
                        (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦
                                  C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := TopCat.carrier)
                                  ((toTopCat.mapCone C).π.app j)) :
                              (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj j) : Type (max u v))) →
                                (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
                            V)
                    ⋯)) :
              Type (max u v))) ↦
      Membership.mem (γ :=
          Set
            (Set
              (↑((F ⋙ toTopCat).obj
                    (Exists.choose (p := fun (j : J) ↦
                      ∃ (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))),
                        Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))))
                            ((fun (j : J) ↦
                                ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                                  Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
                              j)
                            V ∧
                          (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦
                                    C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := TopCat.carrier)
                                    ((toTopCat.mapCone C).π.app j)) :
                                (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj j) : Type (max u v))) →
                                  (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
                              V)
                      ⋯)) :
                Type (max u v))))
          ((fun (j : J) ↦
              ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
            (Exists.choose (p := fun (j : J) ↦
              ∃ (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))),
                Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))))
                    ((fun (j : J) ↦
                        ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                          Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
                      j)
                    V ∧
                  (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                            (CC := TopCat.carrier) ((toTopCat.mapCone C).π.app j)) :
                        (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj j) : Type (max u v))) →
                          (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
                      V)
              ⋯))
          V ∧
        (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                  TopCat.carrier) (X :=
                  Functor.obj (Functor.obj (Functor.const J) (toTopCat.mapCone C).pt)
                    (Exists.choose (p := fun (j : J) ↦
                      ∃ (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))),
                        Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))))
                            ((fun (j : J) ↦
                                ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                                  Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
                              j)
                            V ∧
                          (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦
                                    C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := TopCat.carrier)
                                    ((toTopCat.mapCone C).π.app j)) :
                                (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj j) : Type (max u v))) →
                                  (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
                              V)
                      ⋯))
                  ((toTopCat.mapCone C).π.app
                    (Exists.choose (p := fun (j : J) ↦
                      ∃ (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))),
                        Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))))
                            ((fun (j : J) ↦
                                ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
                                  Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
                              j)
                            V ∧
                          (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦
                                    C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := TopCat.carrier)
                                    ((toTopCat.mapCone C).π.app j)) :
                                (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj j) : Type (max u v))) →
                                  (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
                              V)
                      ⋯))) :
              (a : (↑(((Functor.const J).obj (toTopCat.mapCone C).pt).obj (Exists.choose ⋯)) : Type (max u v))) →
                (↑((F ⋙ toTopCat).obj (Exists.choose ⋯)) : Type (max u v))) ⁻¹'
            V)
hV :
  ∀ (s : (↑S : Type (max u v))),
    IsClopen (V s) ∧
      (↑s : Set (↑(toTopCat.mapCone C).pt : Type (max u v))) =
        (⇑(ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v)),
                  (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))))
                (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
                (X := Functor.obj (Functor.obj (Functor.const J) C.pt) (j s)) (C.π.app (j s))) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑X.toTop : Type (max u v)))
                  (((Functor.const J).obj C.pt).obj (j s))) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑X.toTop : Type (max u v)))
                (F.obj (j s))) ⁻¹'
          V s
hUo :
  ∀ (i : (↑S : Type (max u v))),
    IsOpen (X :=
      (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
          (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
        (Functor.obj (Functor.obj (Functor.const J) C.pt) (j i)))
      ((fun (s : (↑S : Type (max u v))) ↦
          ((⇑(ConcreteCategory.hom (FC :=
                    fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))))
                    (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                    (X := Functor.obj (Functor.obj (Functor.const J) C.pt) (j s)) (C.π.app (j s))) :
                (a :
                    (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                        (↑X.toTop : Type (max u v)))
                      (((Functor.const J).obj C.pt).obj (j s))) →
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                      (↑X.toTop : Type (max u v)))
                    (F.obj (j s))) ⁻¹'
              V s :
            Set
              ((fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v)))
                (Functor.obj (Functor.obj (Functor.const J) C.pt) (j s)))))
        i)
hsU :
  U ⊆
    ⋃ (i : (↑S : Type (max u v))),
      (fun (s : (↑S : Type (max u v))) ↦
          ((⇑(ConcreteCategory.hom (FC :=
                    fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))))
                    (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                    (X := Functor.obj (Functor.obj (Functor.const J) C.pt) (j s)) (C.π.app (j s))) :
                (a :
                    (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                        (↑X.toTop : Type (max u v)))
                      (((Functor.const J).obj C.pt).obj (j s))) →
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                      (↑X.toTop : Type (max u v)))
                    (F.obj (j s))) ⁻¹'
              V s :
            Set
              ((fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v)))
                (Functor.obj (Functor.obj (Functor.const J) C.pt) (j s)))))
        i
G : Finset (↑S : Type (max u v))
hG :
  U ⊆
    ⋃ i ∈ G,
      (fun (s : (↑S : Type (max u v))) ↦
          ((⇑(ConcreteCategory.hom (FC :=
                    fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))))
                    (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                    (X := Functor.obj (Functor.obj (Functor.const J) C.pt) (j s)) (C.π.app (j s))) :
                (a :
                    (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                        (↑X.toTop : Type (max u v)))
                      (((Functor.const J).obj C.pt).obj (j s))) →
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                      (↑X.toTop : Type (max u v)))
                    (F.obj (j s))) ⁻¹'
              V s :
            Set
              (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))))
        i
refine_3 :
  ∀ (j0 : J) (hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty.{v + 1} (j0 ⟶ X)),
    ∃ (j : J) (V :
      Set
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
      IsClopen V ∧
        U =
          (⇑(ConcreteCategory.hom (FC :=
                  fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)),
                    (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))))
                  (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v)))
                  (C.π.app j)) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                      (↑X.toTop : Type (max u v)))
                    (((Functor.const J).obj C.pt).obj j)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑X.toTop : Type (max u v)))
                  (F.obj j)) ⁻¹'
            V
⊢ ∃ (j : J) (V :
    Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
    IsClopen V ∧
      U =
        (⇑(ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v)),
                  (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))))
                (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
                (C.π.app j)) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑X.toTop : Type (max u v)))
                  (((Functor.const J).obj C.pt).obj j)) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑X.toTop : Type (max u v)))
                (F.obj j)) ⁻¹'
          V

Tactic:
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists (G.image j)

Premises used: CategoryTheory.IsCofiltered.inf_objs_exists, Finset.image