abel bug?

Stream: mathlib4

[Heather Macbeth]

I think the following may be a bug in abel_nf, perhaps that the normal form is not consistent across different expressions encountered.

import Mathlib.Tactic.Abel

variable {A : Type} [AddCommGroup A]

-- works
example (a b s : A) : -b + (s - a) = s - b - a := by abel

-- fails, leaves goal state `-1 • b + (s + -1 • a) = s + (-1 • b + -1 • a)`
example (a b s : A) : -b + (s - a) = s - b - a := by abel_nf

[Heather Macbeth]

Of course in that example one can just use abel, but there are similar examples where you really want consistent behaviour in abel_nf. I encountered it trying to do something like this:

example (a b s : A) (f : A → A) : f (-b + (s - a)) = f (s - b - a) := by abel_nf

[Mario Carneiro]

#5403

[Heather Macbeth]

Even for @Mario Carneiro, an 11-minute bugfix is pretty fast. Thanks!