fix: make library suggestions available in module files

This PR makes the library suggestions extension state available when
importing from `module` files.

In a `module` file, non-public imports at deeper transitive levels don't
have their data loaded (to support proper encapsulation in the module
system). Since the library suggestions extension stores and evaluates
syntax that references constants from these modules, both the extension
state and the referenced constants need to be publicly exported.

The fix marks `Basic`, `SineQuaNon`, and `Default` as `public import` in
`Lean.LibrarySuggestions`:
- `Basic` defines the `librarySuggestionsExt` environment extension
- `SineQuaNon` defines `sineQuaNonSelector` referenced in the selector syntax
- `Default` sets the selector using `set_library_suggestions`

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

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