-- 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
⊢ ∑ i ∈ s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
have h₂ :
  (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) = (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫ : 𝕜) := by
  classical exact hv.inner_left_right_finset

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)
⊢ ∑ i ∈ s, ‖inner (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
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

Tactic:
simp only [norm_nonneg, pow_nonneg]

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 * (starRingEnd 𝕜) z) = ‖z‖ ^ 2

Tactic:
intro z

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 * (starRingEnd 𝕜) z) = ‖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
⊢ ∑ 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:
classical 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)
⊢ ∑ i ∈ s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
have h₃ : ∀ z : 𝕜, re (z * conj z) = ‖z‖ ^ 2 := by
  intro z
  simp only [mul_conj, normSq_eq_def']
  norm_cast

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
⊢ ∑ i ∈ s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2