-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem countable_cover_nhdsWithin_of_sigmaCompact {f : X → Set X} {s : Set X} (hs : IsClosed s)
    (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i

Tactic:
rcases exists_mem_compactCovering x with ⟨n, hn⟩

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
y : X
hyt : y ∈ t n
hyf : x ∈ s → x ∈ f y
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i

Tactic:
exact ⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩

Result:
no goals

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i

Tactic:
rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
y : X
hyt : y ∈ t n
hyf : x ∈ s → x ∈ f y
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
choose t ht hsub using fun n =>
  ((isCompact_compactCovering X n).inter_right hs).elim_nhds_subcover _ fun x hx => hf x hx.right

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
refine
  ⟨⋃ n, (t n : Set X), iUnion_subset fun n x hx => (ht n x hx).2,
    countable_iUnion fun n => (t n).countable_toSet, fun x hx => mem_iUnion₂.2 ?_⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
simp only [nhdsWithin, mem_inf_principal] at hf

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x