-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem TotallyBounded.image [UniformSpace β] {f : α → β} {s : Set α} (hs : TotallyBounded s)
    (hf : UniformContinuous f) : TotallyBounded (f '' s) := fun t ht =>
  have : { p : α × α | (f p.1, f p.2) ∈ t } ∈ 𝓤 α := hf ht
  let ⟨c, hfc, hct⟩ := hs _ this
  ⟨f '' c, hfc.image f, by
    simp only [mem_image, iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, image_subset_iff,
      preimage_iUnion, preimage_setOf_eq]
    simp? [subset_def] at hct says
      simp only [mem_setOf_eq, subset_def, mem_iUnion, exists_prop] at hct
    intro x hx
    simpa using hct x hx⟩

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : ∀ x ∈ s, ∃ i ∈ c, (f x, f i) ∈ t
⊢ s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}

Tactic:
intro x hx

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : ∀ x ∈ s, ∃ i ∈ c, (f x, f i) ∈ t
x : α
hx : x ∈ s
⊢ x ∈ ⋃ i ∈ c, {a | (f a, f i) ∈ t}

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : s ⊆ ⋃ y ∈ c, {x | (x, y) ∈ {p | (f p.1, f p.2) ∈ t}}
⊢ f '' s ⊆ ⋃ y ∈ f '' c, {x | (x, y) ∈ t}

Tactic:
simp only [mem_image, iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, image_subset_iff,
  preimage_iUnion, preimage_setOf_eq]

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : s ⊆ ⋃ y ∈ c, {x | (x, y) ∈ {p | (f p.1, f p.2) ∈ t}}
⊢ s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : s ⊆ ⋃ y ∈ c, {x | (x, y) ∈ {p | (f p.1, f p.2) ∈ t}}
⊢ s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}

Tactic:
simp only [mem_setOf_eq, subset_def, mem_iUnion, exists_prop] at hct

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : ∀ x ∈ s, ∃ i ∈ c, (f x, f i) ∈ t
⊢ s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : ∀ x ∈ s, ∃ i ∈ c, (f x, f i) ∈ t
x : α
hx : x ∈ s
⊢ x ∈ ⋃ i ∈ c, {a | (f a, f i) ∈ t}

Tactic:
simpa using hct x hx

Result:
no goals

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : s ⊆ ⋃ y ∈ c, {x | (x, y) ∈ {p | (f p.1, f p.2) ∈ t}}
⊢ s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}

Tactic:
simp? [subset_def] at hct says
  simp only [mem_setOf_eq, subset_def, mem_iUnion, exists_prop] at hct

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α
c : Set α
hfc : c.Finite
hct : ∀ x ∈ s, ∃ i ∈ c, (f x, f i) ∈ t
⊢ s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}