feat: import Lean.LibrarySuggestions.Default in Mathlib.Init

This enables the `+suggestions` modes in tactics (like `grind +suggestions`)
to work throughout Mathlib without requiring explicit imports.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: kim-em

Mathlib/Init.lean

@@ -1,6 +1,7 @@
 module
 
 public import Lean.Linter.Sets -- for the definition of linter sets
+public import Lean.LibrarySuggestions.Default -- for `+suggestions` modes in tactics
 public import Mathlib.Tactic.Linter.CommandStart
 public import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
 public import Mathlib.Tactic.Linter.DirectoryDependency