-- Mathlib/Topology/Compactness/Compact.lean
theorem LocallyFinite.finite_nonempty_inter_compact {f : ι → Set X}
    (hf : LocallyFinite f) (hs : IsCompact s) : { i | (f i ∩ s).Nonempty }.Finite

Proof state:
case intro.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
⊢ i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}

Tactic:
rcases mem_iUnion₂.1 (hsU hx.2) with ⟨c, hct, hcx⟩

Result:
case intro.intro.intro.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
c : X
hct : c ∈ t
hcx : x ∈ U c
⊢ i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hf : LocallyFinite f
hs : IsCompact s
⊢ {i | (f i ∩ s).Nonempty}.Finite

Tactic:
choose U hxU hUf using hf

Result:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
⊢ {i | (f i ∩ s).Nonempty}.Finite

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
⊢ {i | (f i ∩ s).Nonempty}.Finite

Tactic:
rcases hs.elim_nhds_subcover U fun x _ => hxU x with ⟨t, -, hsU⟩

Result:
case intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
⊢ {i | (f i ∩ s).Nonempty}.Finite

Proof state:
case intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
⊢ {i | (f i ∩ s).Nonempty} ⊆ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}

Tactic:
rintro i ⟨x, hx⟩

Result:
case intro.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
⊢ i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}

Proof state:
case intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
⊢ {i | (f i ∩ s).Nonempty}.Finite

Tactic:
refine (t.finite_toSet.biUnion fun x _ => hUf x).subset ?_

Result:
case intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
⊢ {i | (f i ∩ s).Nonempty} ⊆ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}

Proof state:
case intro.intro.intro.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
c : X
hct : c ∈ t
hcx : x ∈ U c
⊢ i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}

Tactic:
exact mem_biUnion hct ⟨x, hx.1, hcx⟩

Result:
no goals