fix: issue when matching Int literals (#3504)

src/Lean/Meta/Match/Match.lean

@@ -165,9 +165,21 @@ private def isNatValueTransition (p : Problem) : MetaM Bool := do
   unless (← hasNatValPattern p) do return false
   return hasCtorOrInaccessible p
 
+/--
+Predicate for testing whether we need to expand `Int` value patterns into constructors.
+There are two cases:
+- We have constructor or inaccessible patterns. Example:
+```
+| 0, ...
+| Int.toVal p, ...
+...
+```
+- We don't have the `else`-case (i.e., variable pattern). This can happen
+when the non-value cases are unreachable.
+-/
 private def isIntValueTransition (p : Problem) : MetaM Bool := do
   unless (← hasIntValPattern p) do return false
-  return hasCtorOrInaccessible p
+  return hasCtorOrInaccessible p || !hasVarPattern p
 
 private def processSkipInaccessible (p : Problem) : Problem := Id.run do
   let x :: xs := p.vars | unreachable!

tests/lean/run/match_int_lit_issue.lean

@@ -0,0 +1,12 @@
+theorem Int.eq_zero_of_sign_eq_zero' : ∀ {a : Int}, sign a = 0 → a = 0
+  | 0, _ => rfl
+
+def foo (a : Int) : Bool :=
+  match a with
+  | Int.ofNat 0 => true
+  | Int.ofNat 1 => true
+  | _ => false
+
+example : ∀ {a : Int}, foo a = true → a = 0 ∨ a = 1
+  | 0, _ => Or.inl rfl
+  | 1, _ => Or.inr rfl