𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
let p : Submodule 𝕜 E := 𝕜 ∙ x
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
let f := (‖x‖ : 𝕜) • coord 𝕜 x h
case intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
obtain ⟨g, hg⟩ := exists_extension_norm_eq p f
case intro.refine'_1
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ‖g‖ = 1

case intro.refine'_2
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g x = ↑‖x‖
case intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
refine' ⟨g, _, _⟩
no goals
case intro.refine'_1
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ‖g‖ = 1
rw [hg.2, coord_norm']
no goals
case intro.refine'_2
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g x = ↑‖x‖
calc
  g x = g (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [coe_mk]
  _ = ((‖x‖ : 𝕜) • coord 𝕜 x h) (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [← hg.1]
  _ = ‖x‖ := by simp
no goals
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g x = ↑g ↑{ val := x, property := (_ : x ∈ span 𝕜 {x}) }
rw [coe_mk]
no goals
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g ↑{ val := x, property := (_ : x ∈ span 𝕜 {x}) } =
    ↑(↑‖x‖ • coord 𝕜 x h) { val := x, property := (_ : x ∈ span 𝕜 {x}) }
rw [← hg.1]
no goals
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑(↑‖x‖ • coord 𝕜 x h) { val := x, property := (_ : x ∈ span 𝕜 {x}) } = ↑‖x‖
simp