Mathlib CFC: what the `:= by cfc_tac` autoParam can discharge (IsSelfAdjoint, IsStarNormal)

Many CFC and C*-order lemmas take (ha : IsSelfAdjoint a := by cfc_tac), e.g. IsSelfAdjoint.norm_le_max_of_le_of_le. When the tactic fails you get 'could not synthesize default value for parameter ha using tactics'. In Mathlib v4.35.0, cfc_tac is try (first | assumption | infer_instance | aesop (rule_sets := [CStarAlgebra])). Tested in a CStarAlgebra A with [PartialOrder A] [StarOrderedRing A].

These goals were discharged: IsSelfAdjoint b from h : IsSelfAdjoint b, from h : 0 ≤ b and from h : star b = b. With no hypotheses: IsSelfAdjoint (a * star a), (star a * a), 1, 0, cfc f a. From IsSelfAdjoint a (and c): a + c, a - c, -a, a ^ 2, r • a (r : ℝ). IsStarNormal a from IsSelfAdjoint a or from 0 ≤ a.

These were NOT discharged: IsSelfAdjoint b from h : b ≤ 0, from h : IsSelfAdjoint (-b), or from 0 ≤ a and a ≤ c for c.

For the b ≤ 0 case, pass the proof explicitly: by simpa using (IsSelfAdjoint.of_nonneg (neg_nonneg.2 h)).neg, or neg_neg b ▸ (IsSelfAdjoint.of_nonneg (neg_nonneg.2 h)).neg. Note that (IsSelfAdjoint.of_nonneg (neg_nonneg.2 h)).neg alone has type IsSelfAdjoint (-(-b)) and is rejected. Another option is a have hb : IsSelfAdjoint b := ... line before the call, which assumption then picks up.