Is there a way to complicate things with simp?

Stream: new members

[Abhimanyu Pallavi Sudhir]

I.e. is there a way to write simp [←lemma, lemma, lemma]?

[Kenny Lau]

simp [(lemma).symm, lemma, lemma]

[Abhimanyu Pallavi Sudhir]

That doesn't always work, though. For instance, I'm trying to do simp [(polynomial.sum_C_mul_X_eq p).symm, finsupp.sum, polynomial.derivative_sum], -- rewrites work, but simp doesn't.

[Kevin Buzzard]

simp might be taking a wrong turn before it tries the rewrites you want. Switch logging on if you want to investigate further -- see the simp docs in mathlib for an explanation of how to do this.