-- Mathlib/Topology/Compactness/Compact.lean
lemma eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open (b : Set (Set X))
    (hb : IsTopologicalBasis b) (U : Set X) (hUc : IsCompact U) (hUo : IsOpen U) :
    ∃ s : Finset b, U = s.toSet.sUnion

Proof state:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
choose s hs hU using eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U hUc hUo

Result:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
have hb' : b = range (fun i ↦ i : b → Set X) := by simp

Result:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
let _ : Fintype s := Fintype.ofFinite _

Result:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
x✝ : Fintype ↑s := Fintype.ofFinite ↑s
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Proof state:
case h
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
x✝ : Fintype ↑s := Fintype.ofFinite ↑s
⊢ U = ⋃₀ (Subtype.val '' ↑s.toFinset)

Tactic:
simp [hU]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ b = range fun i => ↑i

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
rw [hb'] at hb

Result:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
have : Finite s := hs

Result:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
x✝ : Fintype ↑s := Fintype.ofFinite ↑s
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
use s.toFinset

Result:
case h
X : Type u
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i => ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i => ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
x✝ : Fintype ↑s := Fintype.ofFinite ↑s
⊢ U = ⋃₀ (Subtype.val '' ↑s.toFinset)