diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index e9946c31da4f..2757caac37b5 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -311,7 +311,7 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
   | nil =>
     cases h rfl
   | cons y l ih =>
-    simp only [drop]
+    simp only [length, drop_succ_cons]
     by_cases h₁ : l = []
     · simp [h₁]
     rw [getLast_cons h₁]
diff --git a/src/Init/Data/Range/Polymorphic/IntLemmas.lean b/src/Init/Data/Range/Polymorphic/IntLemmas.lean
index cb763c6b5ced..6cb8196d4c1e 100644
--- a/src/Init/Data/Range/Polymorphic/IntLemmas.lean
+++ b/src/Init/Data/Range/Polymorphic/IntLemmas.lean
@@ -16,6 +16,9 @@ import Init.Data.Option.Lemmas
 import Init.Data.Range.Polymorphic.Lemmas
 import Init.Omega
 
+-- TODO: remove after stage0 update
+set_option linter.unusedSimpArgs false
+
 public section
 
 set_option doc.verso true
@@ -72,7 +75,7 @@ theorem size_toArray_rco {a b : Int} :
 @[simp]
 theorem size_roc {a b : Int} :
     (a<...=b).size = (b - a).toNat := by
-  simp only [Roc.size, Rxc.HasSize.size]
+  simp only [Roc.size, Rxc.HasSize.size, UpwardEnumerable.succ?]
   omega
 
 @[simp]
@@ -88,7 +91,7 @@ theorem size_toArray_roc {a b : Int} :
 @[simp]
 theorem size_roo {a b : Int} :
     (a<...b).size = (b - a - 1).toNat := by
-  simp only [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size, Int.pred_toNat]
+  simp only [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size, UpwardEnumerable.succ?, Int.pred_toNat]
   omega
 
 @[simp]
diff --git a/src/Init/Data/Range/Polymorphic/NatLemmas.lean b/src/Init/Data/Range/Polymorphic/NatLemmas.lean
index 523f0e84f3a2..fdaa3fc2a999 100644
--- a/src/Init/Data/Range/Polymorphic/NatLemmas.lean
+++ b/src/Init/Data/Range/Polymorphic/NatLemmas.lean
@@ -18,6 +18,9 @@ import Init.Data.Option.Lemmas
 import Init.Data.Range.Polymorphic.Lemmas
 import Init.Omega
 
+-- TODO: remove after stage0 update
+set_option linter.unusedSimpArgs false
+
 set_option doc.verso true
 
 public section
@@ -133,7 +136,7 @@ theorem size_toArray_roo {a b : Nat} :
 @[simp]
 theorem size_ric {b : Nat} :
     (*...=b).size = b + 1 := by
-  simp [Ric.size, Rxc.HasSize.size]
+  simp [Ric.size, Rxc.HasSize.size, Least?.least?]
 
 @[deprecated size_ric (since := "2025-10-30")]
 def _root_.Std.PRange.Nat.size_Ric := @_root_.Nat.size_ric
@@ -154,7 +157,7 @@ theorem size_toArray_ric {b : Nat} :
 @[simp]
 theorem size_rio {b : Nat} :
     (*...b).size = b := by
-  simp [Rio.size, Rxo.HasSize.size, Rxc.HasSize.size]
+  simp [Rio.size, Rxo.HasSize.size, Rxc.HasSize.size, Least?.least?]
 
 @[deprecated size_rio (since := "2025-10-30")]
 def _root_.Std.PRange.Nat.size_Rio := @_root_.Nat.size_rio
@@ -1852,7 +1855,7 @@ theorem induct_roc_right (motive : Nat → Nat → Prop)
 
 theorem toList_rio_eq_toList_rco {n : Nat} :
     (*...n).toList = (0...n).toList := by
-  simp [Rio.toList_eq_match_rco]
+  simp [Rio.toList_eq_match_rco, Least?.least?]
 
 @[simp]
 theorem toList_toArray_rio {n : Nat} :
@@ -2014,7 +2017,7 @@ theorem getD_toList_rio_eq_fallback {n i fallback : Nat} (h : n ≤ i) :
 
 theorem toArray_rio_eq_toArray_rco {n : Nat} :
     (*...n).toArray = (0...n).toArray := by
-  simp [Rio.toArray_eq_match_rco]
+  simp [Rio.toArray_eq_match_rco, Least?.least?]
 
 theorem toArray_rio_eq_if {n : Nat} :
     (*...n).toArray = if 0 < n then (*...(n - 1)).toArray.push (n - 1) else #[] := by
@@ -2166,7 +2169,8 @@ theorem getD_toArray_rio_eq_fallback {n i fallback : Nat} (h : n ≤ i) :
 
 theorem toList_ric_eq_toList_rio {n : Nat} :
     (*...=n).toList = (*...(n + 1)).toList := by
-  simp [Ric.toList_eq_match_rcc, toList_rio_succ_eq_append, toList_rio_eq_toList_rco]
+  simp [Ric.toList_eq_match_rcc, toList_rio_succ_eq_append, toList_rio_eq_toList_rco,
+    Least?.least?]
 
 theorem toList_ric_eq_toList_rcc {n : Nat} :
     (*...=n).toList = (0...=n).toList := by
diff --git a/src/Init/LawfulBEqTactics.lean b/src/Init/LawfulBEqTactics.lean
index fe8267431927..40b20c4afc6a 100644
--- a/src/Init/LawfulBEqTactics.lean
+++ b/src/Init/LawfulBEqTactics.lean
@@ -19,7 +19,7 @@ macro "deriving_ReflEq_tactic" : tactic => `(tactic|(
   intro x
   induction x
   all_goals
-    simp only [ BEq.refl, ↓reduceDIte, Bool.and_true, *, reduceBEq ,reduceCtorIdx]
+    simp only [BEq.refl, ↓reduceDIte, Bool.and_true, *, reduceBEq ,reduceCtorIdx]
 ))
 
 theorem and_true_curry {a b : Bool} {P : Prop}
diff --git a/src/Lean/Meta/GetUnfoldableConst.lean b/src/Lean/Meta/GetUnfoldableConst.lean
index 8ac2b5ea6ec9..2c8f8c42b106 100644
--- a/src/Lean/Meta/GetUnfoldableConst.lean
+++ b/src/Lean/Meta/GetUnfoldableConst.lean
@@ -13,7 +13,7 @@ namespace Lean.Meta
 Implements the `TransparencyMode` hierarchy for unfolding decisions.
 See `TransparencyMode` and `ReducibilityStatus` for the design rationale.
 -/
-private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
+def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
   | .none => return false
   | .all  => return true
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 0ce0dcac2261..29b920bac7c1 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -496,40 +496,37 @@ Auxiliary predicate for `whnfMatcher`.
 See comment above.
 -/
 def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
-  match cfg.transparency with
-  | .all     => return true
-  | .default => return !(← isIrreducible info.name)
-  | _ =>
-    let status ← getReducibilityStatus info.name
-    if status matches .reducible | .implicitReducible then
-      return true
-    else if hasMatchPatternAttribute (← getEnv) info.name then
-      return true
-    else
-      return info.name == ``decEq
-       || info.name == ``Nat.decEq
-       || info.name == ``Char.ofNat   || info.name == ``Char.ofNatAux
-       || info.name == ``String.decEq || info.name == ``List.hasDecEq
-       || info.name == ``Fin.ofNat
-       || info.name == ``Fin.ofNat -- It is used to define `BitVec` literals
-       || info.name == ``UInt8.ofNat  || info.name == ``UInt8.decEq
-       || info.name == ``UInt16.ofNat || info.name == ``UInt16.decEq
-       || info.name == ``UInt32.ofNat || info.name == ``UInt32.decEq
-       || info.name == ``UInt64.ofNat || info.name == ``UInt64.decEq
-       /- Remark: we need to unfold the following two definitions because they are used for `Fin`, and
-          lazy unfolding at `isDefEq` does not unfold projections.  -/
-       || info.name == ``HMod.hMod || info.name == ``Mod.mod
+  if (← canUnfoldDefault cfg info) then
+    return true
+  /- Beyond what the normal transparency allows, we additionally unfold
+     certain definitions to expose constructors in match discriminants. -/
+  if hasMatchPatternAttribute (← getEnv) info.name then
+    return true
+  return info.name == ``OfNat.ofNat -- needed to reduce numeric literals in match discriminants
+   || info.name == ``NatCast.natCast -- needed for `↑m` in match discriminants (pervasive in Int proofs)
+   || info.name == ``Zero.zero || info.name == ``One.one -- needed for `0`/`1` in match discriminants
+   || info.name == ``decEq
+   || info.name == ``Nat.decEq
+   || info.name == ``Char.ofNat   || info.name == ``Char.ofNatAux
+   || info.name == ``String.decEq || info.name == ``List.hasDecEq
+   || info.name == ``Fin.ofNat -- needed for Fin literal reduction in match discriminants
+   || info.name == ``UInt8.ofNat  || info.name == ``UInt8.decEq
+   || info.name == ``UInt16.ofNat || info.name == ``UInt16.decEq
+   || info.name == ``UInt32.ofNat || info.name == ``UInt32.decEq
+   || info.name == ``UInt64.ofNat || info.name == ``UInt64.decEq
+   /- `Fin.ofNat` reduces to `⟨a % n, _⟩`, so we also need to unfold `%` (i.e., `HMod.hMod`
+      and `Mod.mod`) to expose the `Fin.mk` constructor in match discriminants. -/
+   || info.name == ``HMod.hMod || info.name == ``Mod.mod
 
 private def whnfMatcher (e : Expr) : MetaM Expr := do
-  /- When reducing `match` expressions, if the reducibility setting is at `TransparencyMode.reducible`,
-     we increase it to `TransparencyMode.instances`. 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` occurring in the target.
-
-     TODO: consider other solutions; investigate whether the solution above produces counterintuitive behavior.  -/
+  /- When reducing `match` expressions at `.reducible` or `.instances` transparency,
+     we use a custom `canUnfoldAtMatcher` predicate that additionally allows unfolding
+     class projections (e.g., `OfNat.ofNat`, `NatCast.natCast`) and a few other specific
+     definitions. This ensures match discriminants like `OfNat.ofNat α n inst` can be
+     reduced to expose constructors, without bumping the overall transparency level.  -/
   if (← getTransparency) matches .instances | .reducible then
     -- Also unfold some default-reducible constants; see `canUnfoldAtMatcher`
-    withTransparency .instances <| withCanUnfoldPred canUnfoldAtMatcher do
+    withCanUnfoldPred canUnfoldAtMatcher do
       whnf e
   else
     -- Do NOT use `canUnfoldAtMatcher` here as it does not affect all/default reducibility and inhibits caching (#2564).
@@ -537,6 +534,7 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do
     whnf e
 
 def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
+  let e := e.consumeMData
   let .const declName declLevels := e.getAppFn
     | return .notMatcher
   let some info ← getMatcherInfo? declName
@@ -984,6 +982,7 @@ partial def whnfCoreUnfoldingAnnotations (e : Expr) : MetaM Expr :=
 
 /-- Try to reduce matcher/recursor/quot applications. We say they are all "morally" recursor applications. -/
 def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
+  let e := e.consumeMData
   if !e.isApp then
     return none
   else match (← reduceMatcher? e) with
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index 17d1a874a59c..4c8f6673d1f3 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -3873,7 +3873,7 @@ theorem getValue_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l
   suffices some (getValue k (insertList l toInsert) contains) = some (getValue k toInsert (contains_of_contains_insertList_of_contains_eq_false_left contains not_contains)) from by
     injection this
   simp only [← getValue?_eq_some_getValue]
-  simp only [ getValue?_eq_getEntry? ]
+  simp only [getValue?_eq_getEntry? ]
   congr 1
   exact getEntry?_insertList_of_contains_left_eq_false distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) not_contains
 
@@ -3885,7 +3885,7 @@ theorem getValue_insertList_of_contains_right [BEq α] [EquivBEq α] {l toInsert
   suffices some (getValue k (insertList l toInsert) h) = some (getValue k toInsert contains) from by
     injection this
   simp only [← getValue?_eq_some_getValue]
-  simp only [ getValue?_eq_getEntry? ]
+  simp only [getValue?_eq_getEntry? ]
   congr 1
   apply getEntry?_insertList_of_contains_eq_true
   . exact distinct_l
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index ec7de2ec9f9e..2eb33c594c33 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -15,6 +15,9 @@ import Init.Data.Int.OfNat
 import Init.Data.Nat.Linear
 import Init.Data.Nat.Simproc
 
+-- TODO: remove after stage0 update
+set_option linter.unusedSimpArgs false
+
 @[expose] public section
 
 /-!
@@ -477,7 +480,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
     next idx_eq_j =>
       apply Or.inl
       constructor
-      · simp only [clearUnit, idx_eq_j, Array.getInternal_eq_getElem, ih1]
+      · simp only [Fin.getElem_fin, clearUnit, idx_eq_j, Array.getInternal_eq_getElem, ih1]
         rw [Array.getElem_modify_self, ih2, remove_add_cancel]
         exact ih3
       · intro k k_ge_idx_add_one
@@ -511,7 +514,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
         · simp only [Fin.getElem_fin]
           exact ih2
         · constructor
-          · simp only [clearUnit, idx_eq_j1, Array.getInternal_eq_getElem, ih1]
+          · simp only [Fin.getElem_fin, clearUnit, idx_eq_j1, Array.getInternal_eq_getElem, ih1]
             rw [Array.getElem_modify_self, ih3, ih4]
             decide
           · constructor
@@ -543,7 +546,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
           · simp only [Fin.getElem_fin]
             exact ih1
           · constructor
-            · simp only [clearUnit, idx_eq_j2, Array.getInternal_eq_getElem, ih2]
+            · simp only [Fin.getElem_fin, clearUnit, idx_eq_j2, Array.getInternal_eq_getElem, ih2]
               rw [Array.getElem_modify_self, ih3, ih4]
               decide
             · constructor
diff --git a/tests/elab/mvcgenTutorial.lean b/tests/elab/mvcgenTutorial.lean
index b229e23169ed..a5d767efc573 100644
--- a/tests/elab/mvcgenTutorial.lean
+++ b/tests/elab/mvcgenTutorial.lean
@@ -212,8 +212,8 @@ instance : Monad Result where
 instance : LawfulMonad Result :=
   LawfulMonad.mk' _
     (by dsimp only [Functor.map]; grind)
-    (by dsimp only [bind]; grind)
-    (by dsimp only [bind]; grind)
+    (by dsimp only [bind, pure]; grind)
+    (by dsimp only [bind, pure]; grind)
 
 instance Result.instWP : WP Result (.except Error .pure) where
   wp
diff --git a/tests/elab/unfold1.lean.out.expected b/tests/elab/unfold1.lean.out.expected
index e0de7543d3be..a279b75b11d0 100644
--- a/tests/elab/unfold1.lean.out.expected
+++ b/tests/elab/unfold1.lean.out.expected
@@ -1,8 +1,17 @@
 case succ
 x : Nat
 ih : isEven (2 * x) = true
-⊢ isOdd (Nat.mul 2 x + 1) = true
+⊢ (match 2 * (x + 1) with
+    | 0 => true
+    | n.succ => isOdd n) =
+    true
 case succ
 x : Nat
 ih : isEven (2 * x) = true
-⊢ isEven (Nat.mul 2 x) = true
+⊢ (match 2 * (x + 1) with
+    | 0 => true
+    | n.succ =>
+      match n with
+      | 0 => false
+      | n.succ => isEven n) =
+    true