diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean
index 631d00e9aa..a7c2f889f1 100644
--- a/Lake/Util/Name.lean
+++ b/Lake/Util/Name.lean
@@ -23,7 +23,7 @@ namespace Name
 open Lean.Name
 
 @[simp] protected theorem beq_false (m n : Name) : (m == n) = false ↔ ¬ (m = n) := by
-  rw [← beq_iff_eq m n]; cases m == n <;> simp
+  rw [← beq_iff_eq m n]; cases m == n <;> simp (config := { decide := true })
 
 @[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n := by
   cases n <;> simp [isPrefixOf]