aesop simp for ifs

Stream: mathlib4

[Violeta Hernández]

In the CGT repo, I've had a lot of success adding the following line:

attribute [local aesop simp] Function.update Polynomial.coeff_one Polynomial.coeff_C Polynomial.coeff_X

These lemmas all rewrite an expression in terms of an if, e.g. coeff_one : coeff 1 n = if n = 0 then 1 else 0. They make pretty terrible simp lemmas, but I think they make great aesop simp lemmas, since aesop is then able to split the resulting if statements, and it's often able to prove both cases of whatever remains separately.

Would it be desirable to upstream these attributes (and similar attributes for similar lemmas) to Mathlib?

[Eric Wieser]

Does aesop apply these lemmas even if it can't make progress?

[Violeta Hernández]

aesop first applies any lemmas tagged simp or aesop simp, then continues onto its other stages.

[Kim Morrison]

I'm curious if you've tried using grind here. We tend to happily (indeed encourage) tag @[grind =] lemmas that create an if on the RHS, as grind is happy to case split.

[Violeta Hernández]

I haven't! I'll have to learn that tactic sooner than later.