-- 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
refine_3 :
  ∀
    (hB :
      TopologicalSpace.IsTopologicalBasis (α := (↑(toTopCat.mapCone C).pt : Type (max u v)))
        {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}),
    ∃ (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
refine_1 :
  ∀ (j : J),
    TopologicalSpace.IsTopologicalBasis (α := (↑((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)
refine_2 :
  ∀ (i j : J) (f : i ⟶ j) (V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))
    (_hV :
      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),
    Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj i) : 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)))))
        i)
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              TopCat.carrier) ((F ⋙ toTopCat).map f)) :
          (a : (↑((F ⋙ toTopCat).obj i) : Type (max u v))) → (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
        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:
have hB := TopCat.isTopologicalBasis_cofiltered_limit.{u, v} (F ⋙ Profinite.toTopCat)
      (Profinite.toTopCat.mapCone C) (isLimitOfPreserves _ hC) (fun j => {W | IsClopen W}) ?_
      (fun i => isClopen_univ) (fun i U1 U2 hU1 hU2 => hU1.inter hU2) ?_