case pos
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : v = 0
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v

case neg
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : ¬v = 0
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
by_cases hv : v = 0
case neg
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
case neg
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : ¬v = 0
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
have hv' : ‖v‖ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv)
case neg
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = ((↑(‖v‖ ^ 2))⁻¹ * inner v w) • v
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
case neg
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
have key :
  (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ((‖v‖ ^ 2 : ℝ) : 𝕜)) • ((orthogonalProjection (𝕜 ∙ v) w) : E) =
    (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ⟪v, w⟫) • v :=
  by simp [mul_smul, smul_orthogonalProjection_singleton 𝕜 w, -ofReal_pow]
no goals
case neg
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = ((↑(‖v‖ ^ 2))⁻¹ * inner v w) • v
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
convert key using 1 <;> field_simp [hv']
case pos
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : v = 0
⊢ ↑(↑(orthogonalProjection ⊥) w) = (inner 0 w / ↑(‖0‖ ^ 2)) • 0
case pos
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : v = 0
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = (inner v w / ↑(‖v‖ ^ 2)) • v
rw [hv, eq_orthogonalProjection_of_eq_submodule (Submodule.span_zero_singleton 𝕜)]
no goals
case pos
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : v = 0
⊢ ↑(↑(orthogonalProjection ⊥) w) = (inner 0 w / ↑(‖0‖ ^ 2)) • 0
simp
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.606270
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
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = ((↑(‖v‖ ^ 2))⁻¹ * inner v w) • v
simp [mul_smul, smul_orthogonalProjection_singleton 𝕜 w, -ofReal_pow]