-- 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 refine_3.intro.intro.intro.intro.refine_2.h.mp
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
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹' ⋃ s ∈ G, W s

Tactic:
simp_rw [W, Set.preimage_iUnion, Set.mem_iUnion]

Result:
case refine_3.intro.intro.intro.intro.refine_2.h.mp
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
⊢ ∃ 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

Proof state:
case refine_3.intro.intro.intro.intro.refine_2.h.mp
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
⊢ ∃ 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:
obtain ⟨_, ⟨s, rfl⟩, _, ⟨hs, rfl⟩, hh⟩ := hG hx

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
⊢ ∃ 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

Proof state:
case refine_3.intro.intro.intro.intro.refine_2
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
⊢ U = ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹' ⋃ s ∈ G, W s

Tactic:
ext x

Result:
case refine_3.intro.intro.intro.intro.refine_2.h
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
⊢ x ∈ U ↔ x ∈ ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹' ⋃ s ∈ G, W s