-- 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
α : 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}

Tactic:
intro x xs

Result:
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
x : α
xs : x ∈ s
⊢ x ∈ ⋃ y ∈ range f, {x | (x, y) ∈ 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}
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
choose f hfs hfr using fun x : u => x.coe_prop.2

Result:
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}

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}
⊢ ∃ i, x ∈ {x | (x, f i) ∈ U}

Tactic:
set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩

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}
z : ↑u := ⟨y, ⋯⟩
⊢ ∃ i, x ∈ {x | (x, f i) ∈ 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
this : Fintype ↑u
⊢ (range f).Finite

Tactic:
exact finite_range f

Result:
no goals

Proof state:
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
x : α
xs : x ∈ s
⊢ x ∈ ⋃ y ∈ range f, {x | (x, y) ∈ U}

Tactic:
obtain ⟨y, hy, xy⟩ := mem_iUnion₂.1 (ks xs)

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}
⊢ x ∈ ⋃ y ∈ range f, {x | (x, y) ∈ 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}
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
let u := k ∩ { y | ∃ x ∈ s, (x, y) ∈ r }

Result:
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}
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩

Result:
case 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
⊢ ∃ t ⊆ s, t.Finite ∧ 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}
z : ↑u := ⟨y, ⋯⟩
⊢ ∃ i, x ∈ {x | (x, f i) ∈ U}

Tactic:
exact ⟨z, rU <| mem_compRel.2 ⟨y, xy, rs (hfr z)⟩⟩

Result:
no goals

Proof state:
case 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
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
rcases hs r hr with ⟨k, fk, ks⟩

Result:
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}
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Proof state:
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

Tactic:
exact range_subset_iff.2 hfs

Result:
no goals