diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 5789c80a06..6103dc6e6d 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -13,6 +13,10 @@ public import Init.SizeOf
 public section
 set_option linter.missingDocs true -- keep it documented
 
+-- BEq instance for Option defined here so it's available early in the import chain
+-- (before Init.Grind.Config and Init.MetaTypes which need BEq (Option Nat))
+deriving instance BEq for Option
+
 @[expose] section
 
 universe u v w