diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 55db7b40d4..e3eb695a76 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -831,10 +831,12 @@ mutual
           else
             unfoldDefault ()
     | .const declName lvls => do
+      let some cinfo ← getUnfoldableConstNoEx? declName | pure none
+      -- check smart unfolding only after `getUnfoldableConstNoEx?` because smart unfoldings have a
+      -- significant chance of not existing and `Environment.contains` misses are more costly
       if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
         return none
       else
-        let some cinfo ← getUnfoldableConstNoEx? declName | pure none
         unless cinfo.hasValue do return none
         deltaDefinition cinfo lvls
           (fun _ => pure none)