mathlib3

d569d634 - refactor(analysis/inner_product_space, geometry/euclidean) range of orthogonal projection (#5408)

refactor(analysis/inner_product_space, geometry/euclidean) range of orthogonal projection (#5408) Previously, the orthogonal projection was defined for all subspaces of an inner product space, with the junk value `id` if the space was not complete; then all nontrivial lemmas required a hypothesis of completeness (and nonemptiness for the affine orthogonal projection). Change this to a definition only for subspaces `K` satisfying `[complete_space K]` (and `[nonempty K]` for the affine orthogonal projection). Previously, the orthogonal projection was a linear map from `E` to `E`. Redefine it to be a linear map from `E` to `K`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Orthogonal.20projection)