-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem NormedSpace.noncompactSpace : NoncompactSpace E

Proof state:
case neg.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
⊢ IsClosedEmbedding fun x_1 => (Infinite.natEmbedding 𝕜) x_1 • x

Tactic:
refine isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_

Result:
case neg.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (fun x_1 y => ‖x‖ ≤ dist ((Infinite.natEmbedding 𝕜) x_1 • x) ((Infinite.natEmbedding 𝕜) y • x)) k n

Proof state:
case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ¬∃ c, c ≠ 0 ∧ ‖c‖ ≠ 1
⊢ NoncompactSpace E

Tactic:
push_neg at H

Result:
case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
⊢ NoncompactSpace E

Proof state:
case pos
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∃ c, c ≠ 0 ∧ ‖c‖ ≠ 1
⊢ NoncompactSpace E

Tactic:
letI := NontriviallyNormedField.ofNormNeOne H

Result:
case pos
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∃ c, c ≠ 0 ∧ ‖c‖ ≠ 1
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.ofNormNeOne H
⊢ NoncompactSpace E

Proof state:
case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
⊢ NoncompactSpace E

Tactic:
rcases exists_ne (0 : E) with ⟨x, hx⟩

Result:
case neg.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
⊢ NoncompactSpace E

Proof state:
case pos
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∃ c, c ≠ 0 ∧ ‖c‖ ≠ 1
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.ofNormNeOne H
⊢ NoncompactSpace E

Tactic:
exact ⟨fun h ↦ NormedSpace.unbounded_univ 𝕜 E h.isBounded⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
⊢ NoncompactSpace E

Tactic:
by_cases H : ∃ c : 𝕜, c ≠ 0 ∧ ‖c‖ ≠ 1

Result:
case pos
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∃ c, c ≠ 0 ∧ ‖c‖ ≠ 1
⊢ NoncompactSpace E

case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ¬∃ c, c ≠ 0 ∧ ‖c‖ ≠ 1
⊢ NoncompactSpace E

Proof state:
case neg.intro._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0

Tactic:
rwa [sub_ne_zero, (Embedding.injective _).ne_iff]

Result:
no goals

Proof state:
case neg.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (fun x_1 y => ‖x‖ ≤ dist ((Infinite.natEmbedding 𝕜) x_1 • x) ((Infinite.natEmbedding 𝕜) y • x)) k n

Tactic:
simp only [dist_eq_norm, ← sub_smul, norm_smul]

Result:
case neg.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ ‖x‖ ≤ ‖(Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n‖ * ‖x‖

Proof state:
case neg.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ ‖x‖ ≤ ‖(Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n‖ * ‖x‖

Tactic:
rw [H, one_mul]

Result:
case neg.intro._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0