𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) (↑(‖v‖ ^ 2) • w)) = inner v w • v
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ ↑(‖v‖ ^ 2) • ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = inner v w • v
suffices ((orthogonalProjection (𝕜 ∙ v) (((‖v‖ ^ 2 : ℝ) : 𝕜) • w)) : E) = ⟪v, w⟫ • v by
  simpa using this
case hvm
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ inner v w • v ∈ Submodule.span 𝕜 {v}

case hvo
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ ∀ (w_1 : E), w_1 ∈ Submodule.span 𝕜 {v} → inner (↑(‖v‖ ^ 2) • w - inner v w • v) w_1 = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) (↑(‖v‖ ^ 2) • w)) = inner v w • v
apply eq_orthogonalProjection_of_mem_of_inner_eq_zero
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
this : ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) (↑(‖v‖ ^ 2) • w)) = inner v w • v
⊢ ↑(‖v‖ ^ 2) • ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = inner v w • v
simpa using this
case hvm
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ ∃ a, a • v = inner v w • v
case hvm
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ inner v w • v ∈ Submodule.span 𝕜 {v}
rw [Submodule.mem_span_singleton]
no goals
case hvm
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ ∃ a, a • v = inner v w • v
use ⟪v, w⟫
case hvo
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w x : E
hx : x ∈ Submodule.span 𝕜 {v}
⊢ inner (↑(‖v‖ ^ 2) • w - inner v w • v) x = 0
case hvo
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
⊢ ∀ (w_1 : E), w_1 ∈ Submodule.span 𝕜 {v} → inner (↑(‖v‖ ^ 2) • w - inner v w • v) w_1 = 0
intro x hx
case hvo.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
c : 𝕜
hx : c • v ∈ Submodule.span 𝕜 {v}
⊢ inner (↑(‖v‖ ^ 2) • w - inner v w • v) (c • v) = 0
case hvo
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w x : E
hx : x ∈ Submodule.span 𝕜 {v}
⊢ inner (↑(‖v‖ ^ 2) • w - inner v w • v) x = 0
obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.mp hx
case hvo.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
c : 𝕜
hx : c • v ∈ Submodule.span 𝕜 {v}
hv : ↑(‖v‖ ^ 2) = inner v v
⊢ inner (↑(‖v‖ ^ 2) • w - inner v w • v) (c • v) = 0
case hvo.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
c : 𝕜
hx : c • v ∈ Submodule.span 𝕜 {v}
⊢ inner (↑(‖v‖ ^ 2) • w - inner v w • v) (c • v) = 0
have hv : ((‖v‖ ^ 2 : ℝ) : 𝕜) = ⟪v, v⟫ := by
  norm_cast
  simp [@norm_sq_eq_inner 𝕜]
no goals
case hvo.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
c : 𝕜
hx : c • v ∈ Submodule.span 𝕜 {v}
hv : ↑(‖v‖ ^ 2) = inner v v
⊢ inner (↑(‖v‖ ^ 2) • w - inner v w • v) (c • v) = 0
simp [inner_sub_left, inner_smul_left, inner_smul_right, map_div₀, mul_comm, hv,
  InnerProductSpace.conj_symm, hv, -ofReal_pow]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
c : 𝕜
hx : c • v ∈ Submodule.span 𝕜 {v}
⊢ ↑(‖v‖ ^ 2) = inner v v
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
c : 𝕜
hx : c • v ∈ Submodule.span 𝕜 {v}
⊢ ↑(‖v‖ ^ 2) = inner v v
norm_cast
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.567907
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
c : 𝕜
hx : c • v ∈ Submodule.span 𝕜 {v}
⊢ ↑(‖v‖ ^ 2) = inner v v
simp [@norm_sq_eq_inner 𝕜]