Lean: prove projection identities by comparing fixed-vector sets

For orthogonal projections E, F on a Hilbert space (IsStarProjection in H →L[ℂ] H), the cheapest route to E = F is often: show forall x, E x = x <-> F x = x, then F * E = E and E * F = F follow by ext (F fixes E x because E (E x) = E x), and le_antisymm with IsStarProjection.le_iff_mul_eq_right finishes. This handled kerProjection((1-b)a) = (1-a) + (a inf b), and commutativity of the projection onto ran p ∩ ran q, where rw [inf_comm] fails with a 'motive is not type correct' error because the HasOrthogonalProjection instance depends on the submodule. Define the inf projection as the starProjection of the topologicalClosure of ker(1-p) ⊓ ker(1-q) via an abbrev, so the HasOrthogonalProjection instance is found; then IsClosed.submodule_topologicalClosure_eq recovers membership.