-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
lemma totallyBounded_image_iff {f : α → β} {s : Set α} (hf : IsUniformInducing f) :
    TotallyBounded (f '' s) ↔ TotallyBounded s

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
⊢ TotallyBounded (f '' s) ↔ TotallyBounded s

Tactic:
refine ⟨fun hs ↦ ?_, fun h ↦ h.image hf.uniformContinuous⟩

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
⊢ TotallyBounded s

Proof state:
case right
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : f '' s ⊆ ⋃ y ∈ f '' u, {x | (x, y) ∈ t}
⊢ s ⊆ ⋃ y ∈ u, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}

Tactic:
rwa [biUnion_image, image_subset_iff, preimage_iUnion₂] at h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
⊢ TotallyBounded s

Tactic:
simp_rw [(hf.basis_uniformity (basis_sets _)).totallyBounded_iff]

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
⊢ ∀ i ∈ 𝓤 β, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ Prod.map f f ⁻¹' id i}

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
⊢ ∀ i ∈ 𝓤 β, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ Prod.map f f ⁻¹' id i}

Tactic:
intro t ht

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
t : Set (β × β)
ht : t ∈ 𝓤 β
⊢ ∃ t_1, t_1.Finite ∧ s ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
t : Set (β × β)
ht : t ∈ 𝓤 β
⊢ ∃ t_1, t_1.Finite ∧ s ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}

Tactic:
rcases exists_subset_image_finite_and.1 (hs.exists_subset ht) with ⟨u, -, hfin, h⟩

Result:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : f '' s ⊆ ⋃ y ∈ f '' u, {x | (x, y) ∈ t}
⊢ ∃ t_1, t_1.Finite ∧ s ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}

Proof state:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : f '' s ⊆ ⋃ y ∈ f '' u, {x | (x, y) ∈ t}
⊢ ∃ t_1, t_1.Finite ∧ s ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}

Tactic:
use u, hfin

Result:
case right
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
hs : TotallyBounded (f '' s)
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : f '' s ⊆ ⋃ y ∈ f '' u, {x | (x, y) ∈ t}
⊢ s ⊆ ⋃ y ∈ u, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}