-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma totallyBounded_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
    TotallyBounded (interUnionBalls xs u U)

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Tactic:
have h_subset : interUnionBalls xs u U
    ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
  fun x hx ↦ Set.mem_iInter.1 hx i

Result:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ x ∈ ⋃ y, ⋃ (_ : y ≤ u i), {x | (x, xs y) ∈ U i}

Tactic:
exact h_subset hx

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Tactic:
refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩

Result:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ x ∈ ⋃ y ∈ ↑(Finset.image xs (Finset.range (u i + 1))), {x | (x, y) ∈ U i}

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
rw [Filter.HasBasis.totallyBounded_iff H]

Result:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ ∀ (i : ℕ), p i → ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ ∀ (i : ℕ), p i → ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Tactic:
intro i _

Result:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Tactic:
classical
refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
  iUnion_iUnion_eq_right, Nat.lt_succ_iff]
exact h_subset hx

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ x ∈ ⋃ y ∈ ↑(Finset.image xs (Finset.range (u i + 1))), {x | (x, y) ∈ U i}

Tactic:
simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
  iUnion_iUnion_eq_right, Nat.lt_succ_iff]

Result:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → Set (α × α)
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ x ∈ ⋃ y, ⋃ (_ : y ≤ u i), {x | (x, xs y) ∈ U i}