-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.elim_nhds_subcover' (hs : IsLindelof s) (U : ∀ x ∈ s, Set X)
    (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) :
    ∃ t : Set s, t.Countable ∧ s ⊆ ⋃ x ∈ t, U (x : s) x.2

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
use r, hr

Result:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ s ⊆ ⋃ x ∈ r, U ↑x ⋯

Proof state:
case right.h
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
i : ↑s
hi : i ∈ r
⊢ (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
apply Subset.trans interior_subset

Result:
case right.h
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
i : ↑s
hi : i ∈ r
⊢ U ↑i ⋯ ⊆ ⋃ x ∈ r, U ↑x ⋯

Proof state:
case right.h
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
i : ↑s
hi : i ∈ r
⊢ U ↑i ⋯ ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
exact subset_iUnion_of_subset i (subset_iUnion_of_subset hi (Subset.refl _))

Result:
no goals

Proof state:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
apply iUnion₂_subset

Result:
case right.h
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ∀ i ∈ r, (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
have := hs.elim_countable_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
  fun x hx ↦
    mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
this : ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯

Proof state:
case right.h
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ∀ i ∈ r, (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
intro i hi

Result:
case right.h
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
i : ↑s
hi : i ∈ r
⊢ (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯

Proof state:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ s ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
apply Subset.trans hs

Result:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
this : ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
rcases this with ⟨r, ⟨hr, hs⟩⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯