refactor: derive BEq for Option earlier in import chain (#11960)

This PR moves the `deriving instance BEq for Option` from
`Init.Data.Option.Basic` to `Init.Core`, making `BEq (Option α)`
available earlier in the import chain.

This is preparatory work for adding `maxSuggestions : Option Nat` fields
to `Grind.Config` and `Simp.Config`, which need `BEq (Option Nat)` for
the `deriving BEq` clause.

The duplicate derivation in `Init.Data.Option.Basic` is kept because
proofs there need the definition to be exposed.

🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>

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