-- Mathlib/Topology/MetricSpace/Kuratowski.lean
theorem exists_isometric_embedding (α : Type u) [MetricSpace α] [SeparableSpace α] :
    ∃ f : α → ℓ^∞(ℕ), Isometry f

Proof state:
case inr.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
⊢ ∃ f, Isometry f

Tactic:
haveI : Inhabited α := ⟨basepoint⟩

Result:
case inr.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
⊢ ∃ f, Isometry f

Proof state:
case inr.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
⊢ ∃ f, Isometry f

Tactic:
rcases Set.countable_iff_exists_subset_range.1 S_countable with ⟨x, x_range⟩

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ f, Isometry f

Proof state:
case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ Isometry fun x => 0

Tactic:
intro x

Result:
case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
x : α
⊢ ∀ (x2 : α), edist ((fun x => 0) x) ((fun x => 0) x2) = edist x x2

Proof state:
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
⊢ ∃ f, Isometry f

Tactic:
rcases (univ : Set α).eq_empty_or_nonempty with h | h

Result:
case inl
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ ∃ f, Isometry f

case inr
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ.Nonempty
⊢ ∃ f, Isometry f

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ f, Isometry f

Tactic:
exact ⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩

Result:
no goals

Proof state:
case inr.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
⊢ ∃ f, Isometry f

Tactic:
have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α

Result:
case inr.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this✝ : Inhabited α
this : ∃ s, s.Countable ∧ Dense s
⊢ ∃ f, Isometry f

Proof state:
case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
x : α
⊢ ∀ (x2 : α), edist ((fun x => 0) x) ((fun x => 0) x2) = edist x x2

Tactic:
exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)

Result:
no goals

Proof state:
case inr
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ.Nonempty
⊢ ∃ f, Isometry f

Tactic:
rcases h with ⟨basepoint⟩

Result:
case inr.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
⊢ ∃ f, Isometry f

Proof state:
case inr.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this✝ : Inhabited α
this : ∃ s, s.Countable ∧ Dense s
⊢ ∃ f, Isometry f

Tactic:
rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩

Result:
case inr.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
⊢ ∃ f, Isometry f

Proof state:
case inl
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ ∃ f, Isometry f

Tactic:
use fun _ => 0

Result:
case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ Isometry fun x => 0