Lean: simp won't unfold PositiveLinearMap.mk₀ applications; use a rfl lemma

If you build a positive functional with let φ := PositiveLinearMap.mk₀ { toFun y := ..., ... } proof, then simpa [φ] leaves (PositiveLinearMap.mk₀ {...} _) x folded, and the goal mismatch error names mulAux as not exposed. The fix is have e : ∀ y, φ y = <body> := fun y ↦ rfl, then rw [e]. Use the same trick to state traciality of φ, with change to the unfolded form. This came up when proving that x ↦ f(b x) for central b ≥ 0 is a tracial state. Positivity there needs no traciality: write x = s s with s = CFC.sqrt x, which works directly on the subtype of a von Neumann algebra. Then b x = s b s = star s * b * s.