case inl
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ ∃ f, Isometry f

case inr
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : Set.Nonempty univ
⊢ ∃ f, Isometry f
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
⊢ ∃ f, Isometry f
cases' (univ : Set α).eq_empty_or_nonempty with h h
case inl
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ Isometry fun x => 0
case inl
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ ∃ f, Isometry f
use fun _ => 0
case inl
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x✝ : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
x : α
⊢ ∀ (x2 : α), edist ((fun x => 0) x) ((fun x => 0) x2) = edist x x2
case inl
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ Isometry fun x => 0
intro x
no goals
case inl
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x✝ : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
x : α
⊢ ∀ (x2 : α), edist ((fun x => 0) x) ((fun x => 0) x2) = edist x x2
exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
⊢ ∃ f, Isometry f
case inr
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : Set.Nonempty univ
⊢ ∃ f, Isometry f
rcases h with ⟨basepoint⟩
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
⊢ ∃ f, Isometry f
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
⊢ ∃ f, Isometry f
haveI : Inhabited α := ⟨basepoint⟩
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this✝ : Inhabited α
this : ∃ s, Set.Countable s ∧ Dense s
⊢ ∃ f, Isometry f
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
⊢ ∃ f, Isometry f
have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α
case inr.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : Set.Countable S
S_dense : Dense S
⊢ ∃ f, Isometry f
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this✝ : Inhabited α
this : ∃ s, Set.Countable s ∧ Dense s
⊢ ∃ f, Isometry f
rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩
case inr.intro.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x✝ : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : Set.Countable S
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ f, Isometry f
case inr.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : Set.Countable S
S_dense : Dense S
⊢ ∃ f, Isometry f
rcases Set.countable_iff_exists_subset_range.1 S_countable with ⟨x, x_range⟩
no goals
case inr.intro.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x✝ : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : Set.Countable S
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ f, Isometry f
exact ⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩