no goals
ι : Type u_3
ι' : Type ?u.859551
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.859580
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.859598
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.859618
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
b : OrthonormalBasis ι 𝕜 { x // x ∈ U }
x : E
⊢ ↑(orthogonalProjection U) x = ∑ i : ι, inner (↑(↑b i)) x • ↑b i
simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
  (b.sum_repr (orthogonalProjection U x)).symm