-- 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
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
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
let W : S → Set (F.obj j0) := fun s => if hs : s ∈ G then F.map (f s hs) ⁻¹' V s else Set.univ

Result:
case refine_3.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
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Proof state:
case refine_1
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
⊢ ∀ (j : J), TopologicalSpace.IsTopologicalBasis ((fun j => {W | IsClopen W}) j)

Tactic:
intro i

Result:
case refine_1
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
i : J
⊢ TopologicalSpace.IsTopologicalBasis ((fun j => {W | IsClopen W}) i)

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 ∈ (fun i => ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i) ⟨T, hT⟩

Tactic:
dsimp only

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 ∈ ⇑(ConcreteCategory.hom (C.π.app (j ⟨T, hT⟩))) ⁻¹' V ⟨T, hT⟩

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 ∈ ⇑(ConcreteCategory.hom (C.π.app (j ⟨T, hT⟩))) ⁻¹' V ⟨T, hT⟩

Tactic:
rwa [← (hV ⟨T, hT⟩).2]

Result:
no goals

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
hUo : ∀ (i : ↑S), IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
⊢ U ⊆ ⋃ i, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i

Tactic:
rw [h]

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
hUo : ∀ (i : ↑S), IsOpen ((fun s => ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
⊢ ⋃₀ S ⊆ ⋃ i, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i