-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem _root_.IsComplete.nonempty_iInter_of_nonempty_biInter {s : ℕ → Set α}
    (h0 : IsComplete (s 0)) (hs : ∀ n, IsClosed (s n)) (h's : ∀ n, IsBounded (s n))
    (h : ∀ N, (⋂ n ≤ N, s n).Nonempty) (h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)) :
    (⋂ n, s n).Nonempty

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ (⋂ n, s n).Nonempty

Tactic:
have : CauchySeq u := by
  apply cauchySeq_of_le_tendsto_0 _ _ h'
  intro m n N hm hn
  exact dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
⊢ (⋂ n, s n).Nonempty

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
n N : ℕ
hn : n ≤ N
⊢ u N ∈ s n

Tactic:
apply mem_of_subset_of_mem _ (h N).choose_spec

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
n N : ℕ
hn : n ≤ N
⊢ ⋂ n, ⋂ (_ : n ≤ N), s n ⊆ s n

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
n N : ℕ
hn : n ≤ N
⊢ ⋂ n, ⋂ (_ : n ≤ N), s n ⊆ s n

Tactic:
intro x hx

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
n N : ℕ
hn : n ≤ N
x : α
hx : x ∈ ⋂ n, ⋂ (_ : n ≤ N), s n
⊢ x ∈ s n

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
⊢ (⋂ n, s n).Nonempty

Tactic:
refine ⟨x, mem_iInter.2 fun n => ?_⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
n : ℕ
⊢ x ∈ s n

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
n N : ℕ
hn : n ≤ N
x : α
hx : x ∈ ⋂ n, ⋂ (_ : n ≤ N), s n
⊢ x ∈ s n

Tactic:
simp only [mem_iInter] at hx

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
n N : ℕ
hn : n ≤ N
x : α
hx : ∀ i ≤ N, x ∈ s i
⊢ x ∈ s n

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
⊢ (⋂ n, s n).Nonempty

Tactic:
let u N := (h N).some

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => ⋯.some
⊢ (⋂ n, s n).Nonempty