diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 96d02a6a13..6b6862c2aa 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/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
diff --git a/tests/lean/matchOfNatIssue.lean b/tests/lean/matchOfNatIssue.lean
new file mode 100644
index 0000000000..e5814d7a69
--- /dev/null
+++ b/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
diff --git a/tests/lean/matchOfNatIssue.lean.expected.out b/tests/lean/matchOfNatIssue.lean.expected.out
new file mode 100644
index 0000000000..9484f5c1c9
--- /dev/null
+++ b/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