-- Mathlib/Topology/Separation/Profinite.lean
theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] :
    IsTopologicalBasis { s : Set H | IsClopen s }

Proof state:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x => ↑↑x
f1 : IsOpenEmbedding fun x => ↑↑x
f2 : IsOpen v
⊢ IsOpen (Subtype.val '' V)

Tactic:
have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
  rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]

Result:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x => ↑↑x
f1 : IsOpenEmbedding fun x => ↑↑x
f2 : IsOpen v
f3 : Subtype.val '' V = (fun x => ↑↑x) '' v
⊢ IsOpen (Subtype.val '' V)

Proof state:
case intro.intro.intro
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U

Tactic:
lift x to s using interior_subset xs

Result:
case intro.intro.intro.intro
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U

Proof state:
case intro.intro.intro
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U

Tactic:
let u : Set s := ((↑) : s → H) ⁻¹' interior s

Result:
case intro.intro.intro
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U

Proof state:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x => ↑↑x
f1 : IsOpenEmbedding fun x => ↑↑x
f2 : IsOpen v
f3 : Subtype.val '' V = (fun x => ↑↑x) '' v
⊢ IsOpen ((fun x => ↑↑x) '' v)

Tactic:
apply f1.isOpenMap v f2

Result:
no goals

Proof state:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
⊢ IsOpen (Subtype.val '' V)

Tactic:
have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl

Result:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
⊢ IsOpen (Subtype.val '' V)

Proof state:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝¹ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this✝ : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x => ↑↑x
this : (range fun x => ↑↑x) = interior s
⊢ IsOpen (interior s)

Tactic:
apply isOpen_interior

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
VisClopen' : IsClopen (Subtype.val '' V)
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U

Tactic:
use (↑) '' V, VisClopen', by simp [Vx], Subset.trans (by simp) sU

Result:
no goals

Proof state:
case intro.intro.intro.intro
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨V : Set s, VisClopen, Vx, V_sub⟩ := compact_exists_isClopen_in_isOpen u_open_in_s xs

Result:
case intro.intro.intro.intro.intro.intro.intro
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U