-- 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
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty.{v + 1} (j0 ⟶ X)
f : (s : (↑S : Type (max u v))) → s ∈ G → (j0 ⟶ j s) := fun (s : (↑S : Type (max u v))) (hs : s ∈ G) ↦ Nonempty.some ⋯
W : (↑S : Type (max u v)) →
  Set (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  fun (s : (↑S : Type (max u v))) ↦
    if hs : s ∈ G then
      (⇑(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)))
              (F.map (f s hs))) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑X.toTop : Type (max u v)))
                (F.obj j0)) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                (↑X.toTop : Type (max u v)))
              (F.obj (j s))) ⁻¹'
        V s
    else Set.univ
s : (↑S : Type (max u v))
hs : s ∈ G
⊢ IsClopen (X :=
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : 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)))
            (F.map (f s hs))) :
        (a : (↑(F.obj j0).toTop : Type (max u v))) → (↑(F.obj (j s)).toTop : Type (max u v))) ⁻¹'
      V s)

Tactic:
⟨(hV s).1.1.preimage (F.map _).hom.hom.continuous,
      (hV s).1.2.preimage (F.map _).hom.hom.continuous⟩

Premises used: ContinuousMap.continuous, CategoryTheory.Functor.map, And.right, And.left, TopCat.Hom.hom, And.intro, IsClosed.preimage, IsClopen, CategoryTheory.InducedCategory.Hom.hom, IsOpen.preimage