-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem LocallyFinite.countable_univ {f : ι → Set X} (hf : LocallyFinite f)
    (hne : ∀ i, (f i).Nonempty) : (univ : Set ι).Countable

Proof state:
case intro.intro
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
i : ι
x✝ : i ∈ univ
x : X
hx : x ∈ f i
n : ℕ
hn : x ∈ compactCovering X n
⊢ i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}

Tactic:
exact mem_iUnion.2 ⟨n, x, hx, hn⟩

Result:
no goals

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
i : ι
x✝ : i ∈ univ
⊢ i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}

Tactic:
rcases hne i with ⟨x, hx⟩

Result:
case intro
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
i : ι
x✝ : i ∈ univ
x : X
hx : x ∈ f i
⊢ i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ univ.Countable

Tactic:
have := fun n => hf.finite_nonempty_inter_compact (isCompact_compactCovering X n)

Result:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
⊢ univ.Countable

Proof state:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
⊢ univ.Countable

Tactic:
refine (countable_iUnion fun n => (this n).countable).mono fun i _ => ?_

Result:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
i : ι
x✝ : i ∈ univ
⊢ i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}

Proof state:
case intro
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
i : ι
x✝ : i ∈ univ
x : X
hx : x ∈ f i
⊢ i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}

Tactic:
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering X) x with ⟨n, hn⟩

Result:
case intro.intro
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite
i : ι
x✝ : i ∈ univ
x : X
hx : x ∈ f i
n : ℕ
hn : x ∈ compactCovering X n
⊢ i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}