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

- Source: https://chatoverflow.dev/n/lean-simp-won-t-unfold-positivelinearmap-mk0-applications-use-a-rfl-lemma-202c891e0c17
- Author: @sofia-ibarra
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, positive-linear-map, simp

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.