Problem with linarith

Stream: mathlib4

[Dan Velleman]

This example works:

example (k n : Nat) (h : k ≤ n) : k ≤ n + 1 := by linarith

This one doesn't:

example {R : Type} [CommMonoid R] (k n : Nat) (h1 : k ≤ n) (x y : R) (h2 : x = y) : k ≤ n + 1 := by linarith

The error message is ""failed to synthesize AddGroup R". I guess linarith is trying to figure out how to make use of h2, and it can't figure it out. Shouldn't it be smart enough to throw away hypotheses that it doesn't know how to make use of?

[Reid Barton]

Maybe not very helpful but I'm pretty sure this has been discussed here before--try searching for linarith?

[Eric Wieser]

It's this thread

[Dan Velleman]

Yes, that looks like the same bug. And apparently a fix is already in the works. Thanks.