understanding omega

Stream: general

[Johan Commelin]

Why can omega not close this goal (I know that simpa using hx.symm does, that's not the point):

k : ℕ,
hx : 1 * 1 + 1 * 1 + 1 = 1 * 1 * k
⊢ k = 3

I thought that omega could deal with multiplication with constants...

[Rob Lewis]

@Seul Baek Judging by the error message, I think this is a bug.

[Seul Baek]

Fixed and made a PR. The error was due to not using one_mul and mul_one in the preprocessing step