## Stream: general

### Topic: understanding omega

#### Johan Commelin (Aug 09 2019 at 10:33):

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 (Aug 09 2019 at 10:42):

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

#### Seul Baek (Aug 17 2019 at 20:03):

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

Last updated: May 07 2021 at 00:30 UTC