-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem CauchySeq.totallyBounded_range {s : ℕ → α} (hs : CauchySeq s) :
    TotallyBounded (range s)

Proof state:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}

Tactic:
refine ⟨s '' { k | k ≤ n }, (finite_le_nat _).image _, ?_⟩

Result:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ range s ⊆ ⋃ y ∈ s '' {k | k ≤ n}, {x | (x, y) ∈ a}

Proof state:
case intro.inl
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
hm : m ≤ n
⊢ ∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}

case intro.inr
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
hm : n ≤ m
⊢ ∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}

Tactic:
exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
⊢ TotallyBounded (range s)

Tactic:
intro a ha

Result:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}

Proof state:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ s m ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}

Tactic:
rw [mem_iUnion₂]

Result:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ ∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}

Proof state:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}

Tactic:
intro m

Result:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ s m ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}

Proof state:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ ∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}

Tactic:
rcases le_total m n with hm | hm

Result:
case intro.inl
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
hm : m ≤ n
⊢ ∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}

case intro.inr
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
hm : n ≤ m
⊢ ∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}

Proof state:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ range s ⊆ ⋃ y ∈ s '' {k | k ≤ n}, {x | (x, y) ∈ a}

Tactic:
rw [range_subset_iff, biUnion_image]

Result:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}

Tactic:
obtain ⟨n, hn⟩ := cauchySeq_iff.1 hs a ha

Result:
case intro
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}