GroupTheory.GroupAction.ConjAct !4#1871

Stream: mathlib4

[Johan Commelin]

@Gabriel Ebner Jireh reports that there were some very slow simps in this file. I guess you might be interested in seeing those in action?

[Jireh Loreaux]

I sped them up with simp only. Look at the diff to see the original simp. Note that it was necessary also to separate out simp [units_smul_def, other lemmas] into simp only [units_smul_def]; simp [other lemmas], otherwise simp didn't close the goal.

[Jireh Loreaux]

I assume that latter has something to do with the order in which simp lemmas are applied being different in Lean 3 versus 4.

[Kevin Buzzard]

My understanding of this issue is that there's no way of controlling which order simp applies lemmas but if the order matters then the simp set is not "confluent" and one might want to add or remove lemmas to try and make it confluent. Easier said than done sometimes

[Yaël Dillies]

priority precisely lets us control which order simp applies lemmas in. But we haven't decided on the kind of priorities we want to have

[Chris Hughes]

I slightly sped it up by deleting the line smul := (. \bub .)