case pos
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖

case neg
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
by_cases hx : x = 0
case pos.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
case pos
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
obtain ⟨y, hy⟩ := exists_ne (0 : E)
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
case pos.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
obtain ⟨g, hg⟩ : ∃ g : E →L[𝕜] 𝕜, ‖g‖ = 1 ∧ g y = ‖y‖ := exists_dual_vector 𝕜 y hy
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ↑g x = ↑‖x‖
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
refine' ⟨g, hg.left, _⟩
no goals
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ↑g x = ↑‖x‖
simp [hx]
no goals
case neg
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
exact exists_dual_vector 𝕜 x hx