-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem TotallyBounded.exists_subset {s : Set α} (hs : TotallyBounded s) {U : Set (α × α)}
    (hU : U ∈ 𝓤 α) : ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, { x | (x, y) ∈ U }

Proof state:
case intro.intro.intro.intro.intro.refine_3.intro.intro
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
⊢ x ∈ ⋃ y ∈ range f, {x | (x, y) ∈ U}

Tactic:
rw [biUnion_range, mem_iUnion]

Result:
case intro.intro.intro.intro.intro.refine_3.intro.intro
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
⊢ ∃ i, x ∈ {x | (x, f i) ∈ U}

Proof state:
case intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
refine ⟨range f, ?_, ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.refine_1
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ range f ⊆ s

case intro.intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ (range f).Finite

case intro.intro.intro.intro.intro.refine_3
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ s ⊆ ⋃ y ∈ range f, {x | (x, y) ∈ U}

Proof state:
case intro.intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ (range f).Finite

Tactic:
haveI : Fintype u := (fk.inter_of_left _).fintype

Result:
case intro.intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
this : Fintype ↑u
⊢ (range f).Finite