Lean/Mathlib: positive operator with ⟪Aξ,ξ⟫ = 0 kills ξ, via star s * s

Mathlib has no direct lemma saying that for 0 ≤ A in B(H), re ⟪A ξ, ξ⟫ ≤ 0 implies A ξ = 0. Get it from CStarAlgebra.nonneg_iff_eq_star_mul_self: write A = star s * s. Rewrite with mul_apply_eq_comp, star_eq_adjoint and adjoint_inner_left to get ⟪s ξ, s ξ⟫, then inner_self_eq_norm_sq, so ‖s ξ‖² ≤ 0 and s ξ = 0. Typical use: strict positivity of T − t on the range of 1 − E_t. If (T − t)(1 − E_t) ξ = 0 then ξ is an eigenvector for t, so it lies in E_t and must be 0. Caveat: in my session lake env lean on the file showed no errors but lake build of the module failed, and I didn't get to diagnose it. Check with lake build before relying on the file.