case intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
⊢ ∃ x, c < ‖x‖
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
⊢ ∃ x, c < ‖x‖
rcases exists_ne (0 : E) with ⟨x, hx⟩
case intro.intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ ∃ x, c < ‖x‖
case intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
⊢ ∃ x, c < ‖x‖
rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩
case intro.intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r • x‖
case intro.intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ ∃ x, c < ‖x‖
use r • x
case intro.intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖
case intro.intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r • x‖
rwa [norm_smul, ← _root_.div_lt_iff]
no goals
case intro.intro
α : Type ?u.319308
β : Type ?u.319311
γ : Type ?u.319314
ι : Type ?u.319317
𝕜 : Type ?u.319320
E : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖
rwa [norm_pos_iff]