chore(Init): import Tactic.AdaptationNote (leanprover-community#39096)

cf. [#mathlib4 > Where should #adaptation_note be imported?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Where.20should.20.23adaptation_note.20be.20imported.3F/with/593838453)

Author: bryangingechen

Mathlib/Init.lean

@@ -3,6 +3,7 @@ module  -- shake: keep-all, shake: keep-downstream
 public import Lean.Linter.Sets -- for the definition of linter sets
 public import Lean.LibrarySuggestions.Default -- for `+suggestions` modes in tactics
 public import Mathlib.Lean.Linter -- linter utilities; will be transitively imported in #31134
+public import Mathlib.Tactic.AdaptationNote -- make #adaptation_note available everywhere
 public import Mathlib.Tactic.Lemma
 public import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
 public import Mathlib.Tactic.Linter.DirectoryDependency

Mathlib/Logic/Basic.lean

@@ -5,11 +5,10 @@ Authors: Jeremy Avigad, Leonardo de Moura
 -/
 module
 
-public import Mathlib.Tactic.AdaptationNote
 public import Batteries.Logic
 public import Batteries.Util.LibraryNote
 
-import Mathlib.Tactic.Attr.Register
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # Basic logic properties

Mathlib/Tactic/AdaptationNote.lean

@@ -5,7 +5,7 @@ Authors: Kyle Miller
 -/
 module
 
-public import Mathlib.Init
+import Mathlib.Tactic.Linter.Header
 public meta import Lean.Meta.Tactic.TryThis
 
 /-!

MathlibTest/BasicFiles/Init.lean

@@ -40,3 +40,5 @@ run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}"
 theorem test_type_star (α : Type*) : α = α := rfl
 
 lemma test_lemma : True := trivial
+
+#adaptation_note /-- This ensures that adaptation_note is available. -/