-- Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
    ∃ (j : J) (V : Set (F.obj j)), IsClopen V ∧ U = C.π.app j ⁻¹' V

Proof state:
case intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS :
  S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s => Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
x : ↑C.pt.toTop
T : Set ↑(toTopCat.mapCone C).pt
hT : T ∈ S
hx : x ∈ T
⊢ x ∈ ⋃ i, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i

Tactic:
refine ⟨_, ⟨⟨T, hT⟩, rfl⟩, ?_⟩

Result:
case intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS :
  S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s => Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
x : ↑C.pt.toTop
T : Set ↑(toTopCat.mapCone C).pt
hT : T ∈ S
hx : x ∈ T
⊢ x ∈ (fun i => ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i) ⟨T, hT⟩

Proof state:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS :
  S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s => Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
⊢ ∀ (i : ↑S), IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)

Tactic:
intro s

Result:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS :
  S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s => Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
s : ↑S
⊢ IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) s)

Proof state:
case refine_3.intro.intro.intro.intro.refine_2.h.mp.intro.intro.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS :
  S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s => Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, (fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s => if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h => (fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) s) hs
⊢ ∃ i,
    ∃ (_ : i ∈ G),
      x ∈
        ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
          if h : i ∈ G then ⇑(ConcreteCategory.hom (F.map (f i ⋯))) ⁻¹' V i else Set.univ

Tactic:
refine ⟨s, hs, ?_⟩

Result:
case refine_3.intro.intro.intro.intro.refine_2.h.mp.intro.intro.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS :
  S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s => Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, (fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s => if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h => (fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) s) hs
⊢ x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ