mathlib

568435cb - chore(analysis/inner_product_space/projection): typeclass inference for completeness (#10357)

chore(analysis/inner_product_space/projection): typeclass inference for completeness (#10357) As of #5408, most lemmas about orthogonal projection onto a subspace `K` / reflection through a subspace `K` / orthogonal complement of `K` which require `K` to be complete phrase this in terms of `complete_space K` rather than `is_complete K`, so that it can be found by typeclass inference. A few still used the old way; this PR completes the switch.