Non-terminal simps in `GroupTheory.Coxeter.Inversion`

Stream: mathlib4

[Kim Morrison]

Similarly, a non-terminal simp in theorem getD_rightInvSeq_mul_self in Mathlib.GroupTheory.Coxeter.Inversion just got in my way!

@Mitchell Lee or anyone else, would you be able to fix these up?

[Kim Morrison]

I can switch to a different branch and simp? and replace myself, of course, but I would like to note these things as they occur as a reminder that getting these things right really does make a difference to maintenance!

[Mitchell Lee]

Yes, I will do it tomorrow

[Mitchell Lee]

I did it: #13787

Thanks for telling me about this.

[Kim Morrison]

And thanks very much for fixing it! :-)

[Michael Rothgang]

And there was even a tiny speed-up as a result: http://speed.lean-lang.org/mathlib4/run-detail/1dc401b2-67ba-4c95-94cb-9b0626d5b8f2