-- Mathlib/Topology/Separation/Profinite.lean
theorem isTopologicalBasis_isClopen : IsTopologicalBasis { s : Set X | IsClopen s }

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
⊢ ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U

Tactic:
rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
⊢ ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U

Tactic:
have : U ∈ 𝓝 x := IsOpen.mem_nhds U_op hxU

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
⊢ ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds fun U (hU : IsClopen U) => hU.2

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
⊢ ∀ (a : X) (u : Set X), a ∈ u → IsOpen u → ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, a ∈ v ∧ v ⊆ u

Proof state:
case intro.intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U

Tactic:
use V

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ (V ∈ fun U => IsClosed U ∧ IsOpen U) ∧ x ∈ V ∧ V ⊆ U

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ (V ∈ fun U => IsClosed U ∧ IsOpen U) ∧ x ∈ V ∧ V ⊆ U

Tactic:
tauto

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
⊢ ∀ (a : X) (u : Set X), a ∈ u → IsOpen u → ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, a ∈ v ∧ v ⊆ u

Tactic:
intro x U hxU U_op

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen U
⊢ ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U