fix: match + OfNat issue

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20match.20question

src/Lean/Meta/WHNF.lean

@@ -279,7 +279,16 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
       let auxAppType ← inferType auxApp
       forallBoundedTelescope auxAppType info.numAlts fun hs _ => do
         let auxApp := mkAppN auxApp hs
-        let auxApp ← whnf auxApp
+        /- When reducing `match` expressions, if the reducibility setting is at `TransparencyMode.reducible`,
+           we increase it to `TransparencyMode.instance`. We use the `TransparencyMode.reducible` in many places (e.g., `simp`),
+           and this setting prevents us from reducing `match` expressions where the discriminants are terms such as `OfNat.ofNat α n inst`.
+           For example, `simp [Int.div]` will not unfold the application `Int.div 2 1` occuring in the target.
+
+           TODO: consider other solutions; investigate whether the solution above produces counterintuitive behavior.  -/
+        let mut transparency ← getTransparency
+        if transparency == TransparencyMode.reducible then
+          transparency := TransparencyMode.instances
+        let auxApp ← withTransparency transparency <| whnf auxApp
         let auxAppFn := auxApp.getAppFn
         let mut i := prefixSz
         for h in hs do

tests/lean/matchOfNatIssue.lean

@@ -0,0 +1,18 @@
+example (x : Int) (h : x = 2) : Int.div 2 1 = x := by
+  simp [Int.div]
+  traceState
+  simp [h]
+
+example (n : Nat) : Int.div (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n / 0) := by
+  simp [Int.div]
+
+example (n : Nat) : Int.div (Int.ofNat n) 0 = Int.ofNat (n / 0) := by
+  simp [Int.div]
+
+example (n : Nat) : Int.mul (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n * 0) := by
+  simp [Int.mul]
+
+example (n : Nat) : Int.mul (Int.ofNat n) 0 = Int.ofNat (n * 0) := by
+  simp [Int.mul]
+  traceState
+  rfl

tests/lean/matchOfNatIssue.lean.expected.out

@@ -0,0 +1,5 @@
+x : Int
+h : x = 2
+⊢ Int.ofNat (2 / 1) = x
+n : Nat
+⊢ n * 0 = 0