diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index 196420fe1f..0bc82b64fc 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -36,6 +36,12 @@ builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × Reducib
     statsFn         := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size
     -- attribute is set by `addPreDefinitions`
     asyncMode       := .async .asyncEnv
+    replay? := some <| fun _oldState newState newItems otherState =>
+      newItems.foldl (init := otherState) fun otherState k =>
+        if let some v := newState.find? k then
+          otherState.insert k v
+        else
+          otherState
   }
 
 builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ←