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

Proof state:
case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
x✝ : X
⊢ x✝ ∈ Subtype.val '' t → x✝ ∈ s

Tactic:
simp only [mem_image, Subtype.exists, exists_and_right, exists_eq_right, forall_exists_index]

Result:
case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
x✝ : X
⊢ ∀ (x : x✝ ∈ s), ⟨x✝, ⋯⟩ ∈ t → x✝ ∈ s

Proof state:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
this : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

Tactic:
rwa [← this]

Result:
no goals

Proof state:
case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
x✝ : X
⊢ ∀ (x : x✝ ∈ s), ⟨x✝, ⋯⟩ ∈ t → x✝ ∈ s

Tactic:
tauto

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ (∀ x ∈ Subtype.val '' t, x ∈ s) ∧ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

Tactic:
constructor

Result:
case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ ∀ x ∈ Subtype.val '' t, x ∈ s

case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

Proof state:
case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ ∀ x ∈ Subtype.val '' t, x ∈ s

Tactic:
intro _

Result:
case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
x✝ : X
⊢ x✝ ∈ Subtype.val '' t → x✝ ∈ s

Proof state:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

Tactic:
have : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x := biUnion_image.symm

Result:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
this : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

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

Tactic:
refine ⟨↑t, Countable.image htc Subtype.val, ?_⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ (∀ x ∈ Subtype.val '' t, x ∈ s) ∧ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

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

Tactic:
let ⟨t, ⟨htc, htsub⟩⟩ := hs.elim_nhds_subcover' (fun x _ ↦ U x) hU

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