Topic: understanding omega
Johan Commelin (Aug 09 2019 at 10:33):
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
mul_one in the preprocessing step
Last updated: May 07 2021 at 00:30 UTC