case intro
α : Type ?u.296964
β : Type ?u.296967
γ : Type ?u.296970
ι : Type ?u.296973
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.297066
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ = c
α : Type ?u.296964
β : Type ?u.296967
γ : Type ?u.296970
ι : Type ?u.296973
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.297066
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
⊢ ∃ x, ‖x‖ = c
rcases exists_ne (0 : E) with ⟨x, hx⟩
case intro
α : Type ?u.296964
β : Type ?u.296967
γ : Type ?u.296970
ι : Type ?u.296973
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.297066
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ x, ‖x‖ = c
case intro
α : Type ?u.296964
β : Type ?u.296967
γ : Type ?u.296970
ι : Type ?u.296973
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.297066
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ = c
rw [← norm_ne_zero_iff] at hx
case intro
α : Type ?u.296964
β : Type ?u.296967
γ : Type ?u.296970
ι : Type ?u.296973
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.297066
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ‖c • ‖x‖⁻¹ • x‖ = c
case intro
α : Type ?u.296964
β : Type ?u.296967
γ : Type ?u.296970
ι : Type ?u.296973
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.297066
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ x, ‖x‖ = c
use c • ‖x‖⁻¹ • x
no goals
case intro
α : Type ?u.296964
β : Type ?u.296967
γ : Type ?u.296970
ι : Type ?u.296973
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.297066
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ‖c • ‖x‖⁻¹ • x‖ = c
simp [norm_smul, Real.norm_of_nonneg hc, abs_of_nonneg hc, inv_mul_cancel hx]