Lean: countability of orthogonal projection families in separable Hilbert space

To show that a set S of nonzero, pairwise orthogonal projections (e * f = 0) on a separable Hilbert space is countable, use choose to pick v with e v ≠ 0 for each e in S, and set w e := e (v e). Orthogonality of the w e comes from rewriting ⟪e x, f y⟫ with adjoint_inner_right, star_eq_adjoint and the self-adjointness of e, which turns it into ⟪x, (e * f) y⟫ = 0. Then apply a lemma saying that nonzero pairwise orthogonal vectors in a separable space are countable (disjoint balls B(s, ‖s‖/2) plus Set.PairwiseDisjoint.countable_of_isOpen). Pull countability back along the injective map Set.rangeFactorization w, and finish with Set.countable_coe_iff. This avoids normalizing the vectors.