fix: restore #lint via Mathlib.Init (leanprover-community#33827)

This PR is intended as a quick fix to make `#lint` available in Mathlib once again after it was removed with the introduction of the new shake tool in leanprover-community#32731. (See relevant part of the diff [here](https://github.com/leanprover-community/mathlib4/pull/32731/changes#diff-58fcfeaf03590610a5fa5761814c31bca69c4dc9bfb2d97791579919cb880622L8-R10).) Future runs of `shake` should not require `-- shake: keep` after [batteries#1613](leanprover-community/batteries#1613); see also [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23lint.20is.20broken/near/567348613).

Following this, we should likely audit the import hierarchy below Mathlib.Init (and of other meta files) following leanprover-community#32731, and consider whether this is the right hierarchical structure. Possibly we should then add tests to ensure that everything we want to be available remains available at the right points.

Author: thorimur

Mathlib/Init.lean

@@ -12,7 +12,7 @@ public import Mathlib.Tactic.Linter.GlobalAttributeIn
 public import Mathlib.Tactic.Linter.HashCommandLinter
 public import Mathlib.Tactic.Linter.Header
 public import Mathlib.Tactic.Linter.FlexibleLinter
--- This file imports Batteries.Tactic.Lint, where the `env_linter` attribute is defined.
+-- The following module imports `Batteries.Tactic.Lint`, where `#lint` is defined.
 public import Mathlib.Tactic.Linter.Lint
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain

Mathlib/Tactic/Linter/Lint.lean

@@ -5,7 +5,10 @@ Authors: Floris van Doorn
 -/
 module
 
-public import Batteries.Tactic.Lint.Basic
+-- This module imports all of `Batteries.Tactic.Lint`, not just `Batteries.Tactic.Lint.Basic`.
+-- It is responsible for making `#lint` available through `Mathlib.Init`.
+-- TODO: consider removing `-- shake: keep` after batteries#1613
+public import Batteries.Tactic.Lint -- shake: keep
 public import Lean.Linter.Deprecated
 public import Mathlib.Tactic.DeclarationNames