Quesiton on equality and omega

Stream: lean4

[Emmanuel Anaya Gonzalez]

Why does the following snippet works, whereas using the commented line fails?

theorem lemma_small
    (a b : Nat)
    -- (sum : a + b == 2)
    (sum : a + b = 2)
  : (a = 0 ∧ b = 2) ∨ (a = 1 ∧ b = 1) ∨ (a = 2 ∧ b = 0)
  := by omega

[Kim Morrison]

omega knows nothing about ==.

[Kim Morrison]

by simp_all; omega works.

[Emmanuel Anaya Gonzalez]

you are right! thanks :)