α : Type u_1
β : Type ?u.877
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ (i : ι✝), U i
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
α : Type u_1
β : Type ?u.877
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
⊢ IsCompact s
refine isCompact_iff_finite_subcover.2 fun U hUo hs => ?_
case intro
α : Type u_1
β : Type ?u.877
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ (i : ι✝), U i
t : Finset ι✝
ht : ↑{ carrier := ⋃ (i : ι✝), U i, is_open' := (_ : IsOpen (⋃ (i : ι✝), U i)) } ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
α : Type u_1
β : Type ?u.877
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ (i : ι✝), U i
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
rcases ((noetherianSpace_iff_opens α).mp ‹_› ⟨⋃ i, U i, isOpen_iUnion hUo⟩).elim_finite_subcover U
  hUo Set.Subset.rfl with ⟨t, ht⟩
no goals
case intro
α : Type u_1
β : Type ?u.877
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ (i : ι✝), U i
t : Finset ι✝
ht : ↑{ carrier := ⋃ (i : ι✝), U i, is_open' := (_ : IsOpen (⋃ (i : ι✝), U i)) } ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
exact ⟨t, hs.trans ht⟩