-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_singleton {v : E} (w : E) :
    (orthogonalProjection (𝕜 ∙ v) w : E) = (⟪v, w⟫ / ((‖v‖ ^ 2 : ℝ) : 𝕜)) • v

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫_𝕜) • v
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Tactic:
convert key using 1 <;> field_simp [hv']

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Tactic:
have key :
  (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ((‖v‖ ^ 2 : ℝ) : 𝕜)) • ((orthogonalProjection (𝕜 ∙ v) w) : E) =
    (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ⟪v, w⟫) • v := by
  simp [mul_smul, smul_orthogonalProjection_singleton 𝕜 w, -map_pow]

Result:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫_𝕜) • v
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Tactic:
by_cases hv : v = 0

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫_𝕜) • v

Tactic:
simp [mul_smul, smul_orthogonalProjection_singleton 𝕜 w, -map_pow]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Tactic:
have hv' : ‖v‖ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv)

Result:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

Tactic:
rw [hv, eq_orthogonalProjection_of_eq_submodule (Submodule.span_zero_singleton 𝕜)]

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ ↑((orthogonalProjection ⊥) w) = (⟪0, w⟫_𝕜 / ↑(‖0‖ ^ 2)) • 0

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ ↑((orthogonalProjection ⊥) w) = (⟪0, w⟫_𝕜 / ↑(‖0‖ ^ 2)) • 0

Tactic:
simp

Result:
no goals