fix: fixes #2282

src/Lean/Meta/DiscrTree.lean

@@ -436,8 +436,10 @@ def insert [BEq α] (d : DiscrTree α s) (e : Expr) (v : α) : MetaM (DiscrTree
 
 private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array Expr) := do
   let e ← reduceDT e root (simpleReduce := s)
-  if let some v := toNatLit? e then
-    return (.lit v, #[])
+  unless root do
+    -- See pushArgs
+    if let some v := toNatLit? e then
+      return (.lit v, #[])
   match e.getAppFn with
   | .lit v         => return (.lit v, #[])
   | .const c _     =>

tests/lean/run/2282.lean

@@ -0,0 +1,15 @@
+class Zero'.{u} (α : Type u) where
+  zero : α
+
+instance Zero'.toOfNat0 {α} [Zero' α] : OfNat α (nat_lit 0) where
+  ofNat := ‹Zero' α›.1
+
+instance Nat.zero' : Zero' Nat where
+  zero := 0
+
+example :
+    0 = if (b : Bool) then
+      (@OfNat.ofNat.{0} Nat 0 (@Zero'.toOfNat0.{0} Nat (Nat.zero')))
+    else
+      Nat.zero := by
+  simp