-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.sum_inner_products_le {s : Finset ι} (hv : Orthonormal 𝕜 v) :
    ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ re (inner x x) -
      (2 * re (∑ i ∈ s, inner x (inner (v i) x • v i)) -
        re (∑ x_1 ∈ s, ∑ i ∈ s, inner (inner (v i) x • v i) (inner (v x_1) x • v x_1))) =
    re (inner x x) - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2

Tactic:
simp only [inner_smul_right, two_mul, inner_smul_left, inner_conj_symm, ← mul_assoc, h₂,
  add_sub_cancel_right, sub_right_inj]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ re (∑ x_1 ∈ s, inner (v x_1) x * inner x (v x_1)) = ∑ i ∈ s, ‖inner (v i) x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
⊢ ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)

Tactic:
exact hv.inner_left_right_finset

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x‖ ^ 2 - (2 * re (inner x (∑ i ∈ s, inner (v i) x • v i)) - ‖∑ i ∈ s, inner (v i) x • v i‖ ^ 2) =
    ‖x‖ ^ 2 - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2

Tactic:
simp only [@InnerProductSpace.norm_sq_eq_inner 𝕜 E, inner_sum, sum_inner]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ re (inner x x) -
      (2 * re (∑ i ∈ s, inner x (inner (v i) x • v i)) -
        re (∑ x_1 ∈ s, ∑ i ∈ s, inner (inner (v i) x • v i) (inner (v x_1) x • v x_1))) =
    re (inner x x) - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ∑ i ∈ s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
suffices hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2 by
  rw [← sub_nonneg, ← hbf]
  simp only [norm_nonneg, pow_nonneg]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x - ∑ i ∈ s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
z : 𝕜
⊢ re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2

Tactic:
simp only [mul_conj, normSq_eq_def']

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
z : 𝕜
⊢ re (↑‖z‖ ^ 2) = ‖z‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i ∈ s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2
⊢ ∑ i ∈ s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
rw [← sub_nonneg, ← hbf]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i ∈ s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2
⊢ 0 ≤ ‖x - ∑ i ∈ s, inner (v i) x • v i‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ re (∑ x_1 ∈ s, inner (v x_1) x * inner x (v x_1)) = ∑ i ∈ s, ‖inner (v i) x‖ ^ 2

Tactic:
simp only [map_sum, ← inner_conj_symm x, ← h₃]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
z : 𝕜
⊢ re (↑‖z‖ ^ 2) = ‖z‖ ^ 2

Tactic:
norm_cast

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x - ∑ i ∈ s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2

Tactic:
rw [@norm_sub_sq 𝕜, sub_add]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k ∈ s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x‖ ^ 2 - (2 * re (inner x (∑ i ∈ s, inner (v i) x • v i)) - ‖∑ i ∈ s, inner (v i) x • v i‖ ^ 2) =
    ‖x‖ ^ 2 - ∑ i ∈ s, ‖inner (v i) x‖ ^ 2