-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem totallyBounded_of_finite_discretization {s : Set α}
    (H : ∀ ε > (0 : ℝ),
        ∃ (β : Type u) (_ : Fintype β) (F : s → β), ∀ x y, F x = F y → dist (x : α) y < ε) :
    TotallyBounded s

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
this : F x' = F ⟨x, xs⟩
⊢ ∃ i, ∃ (_ : ∃ y, (Subtype.val ∘ Finv) y = i), x ∈ ball i ε

Tactic:
exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε

Tactic:
let x' := Finv (F ⟨x, xs⟩)

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε

Proof state:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
rcases H ε ε0 with ⟨β, fβ, F, hF⟩

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ TotallyBounded s

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs

Result:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded s

case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s.Nonempty
⊢ TotallyBounded s

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
let Finv := Function.invFun F

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Proof state:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
⊢ TotallyBounded s

Tactic:
haveI : Inhabited s := ⟨⟨x0, hx0⟩⟩

Result:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
⊢ TotallyBounded s

Proof state:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded ∅

Tactic:
exact totallyBounded_empty

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s.Nonempty
⊢ TotallyBounded s

Tactic:
rcases hs with ⟨x0, hx0⟩

Result:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
⊢ TotallyBounded s

Proof state:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
⊢ TotallyBounded s

Tactic:
refine totallyBounded_iff.2 fun ε ε0 => ?_

Result:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
refine ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
this : F x' = F ⟨x, xs⟩
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε

Tactic:
simp only [Set.mem_iUnion, Set.mem_range]

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
this : F x' = F ⟨x, xs⟩
⊢ ∃ i, ∃ (_ : ∃ y, (Subtype.val ∘ Finv) y = i), x ∈ ball i ε

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε

Tactic:
have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
this : F x' = F ⟨x, xs⟩
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε