-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
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
⊢ ∃ (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
have 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
Tactic: classical
  obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists (G.image j)
  let f : ∀ s ∈ G, j0 ⟶ j s := fun s hs => (hj0 (Finset.mem_image.mpr ⟨s, hs, rfl⟩)).some
  let W : S → Set (F.obj j0) := fun s => if hs : s ∈ G then F.map (f s hs) ⁻¹' V s else Set.univ
  -- Conclude, using the `j0` and the clopen set of `F.obj j0` obtained above.
  refine ⟨j0, ⋃ (s : S) (_ : s ∈ G), W s, ?_, ?_⟩
  · apply isClopen_biUnion_finset
    intro s hs
    dsimp [W]
    rw [dif_pos hs]
    exact ⟨(hV s).1.1.preimage (F.map _).hom.hom.continuous,
      (hV s).1.2.preimage (F.map _).hom.hom.continuous⟩
  · ext x
    constructor
    · intro hx
      simp_rw [W, Set.preimage_iUnion, Set.mem_iUnion]
      obtain ⟨_, ⟨s, rfl⟩, _, ⟨hs, rfl⟩, hh⟩ := hG hx
      refine ⟨s, hs, ?_⟩
      rwa [dif_pos hs, ← Set.preimage_comp, ← CompHausLike.coe_comp, C.w]
    · intro hx
      simp_rw [W, Set.preimage_iUnion, Set.mem_iUnion] at hx
      obtain ⟨s, hs, hx⟩ := hx
      rw [h]
      refine ⟨s.1, s.2, ?_⟩
      rw [(hV s).2]
      rwa [dif_pos hs, ← Set.preimage_comp, ← CompHausLike.coe_comp, C.w] at hx