chore: import Tactic.Attr.Register privately (leanprover-community#32541)

This is mostly to start a discussion: Should basic tactic files like this one be re-exported by all files out of them being basic, or whether they should be explicitly imported by the few files that actually need it.

Eg in leanprover-community#32245 Andrew and I are adding a new simp attribute, and it's a bit silly that we have to rebuild all of mathlib because that file is re-exported everywhere.

Author: YaelDillies

Mathlib/Algebra/Free.lean

@@ -12,6 +12,8 @@ public import Mathlib.Control.Traversable.Basic
 public import Mathlib.Logic.Equiv.Defs
 public import Mathlib.Tactic.AdaptationNote
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # Free constructions
 

Mathlib/Algebra/Group/Units/Basic.lean

@@ -13,6 +13,8 @@ public import Mathlib.Tactic.Lift
 public import Mathlib.Tactic.Subsingleton
 public import Mathlib.Tactic.Attr.Core
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # Units (i.e., invertible elements) of a monoid
 

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -11,6 +11,8 @@ public import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
 public import Mathlib.CategoryTheory.Monoidal.Discrete
 public import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # The category of monoids in a monoidal category.
 

Mathlib/Control/Applicative.lean

@@ -9,6 +9,8 @@ public import Mathlib.Algebra.Group.Defs
 public import Mathlib.Control.Functor
 public import Mathlib.Control.Basic
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # `applicative` instances
 

Mathlib/Control/Basic.lean

@@ -9,6 +9,8 @@ public import Mathlib.Control.Combinators
 public import Mathlib.Tactic.CasesM
 public import Mathlib.Tactic.Attr.Core
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 Extends the theory on functors, applicatives and monads.
 -/

Mathlib/Control/Functor.lean

@@ -5,10 +5,11 @@ Authors: Simon Hudon
 -/
 module
 
-public import Mathlib.Tactic.Attr.Register
 public import Mathlib.Data.Set.Defs
 public import Mathlib.Tactic.TypeStar
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # Functors
 

Mathlib/Control/Monad/Basic.lean

@@ -8,6 +8,8 @@ module
 public import Mathlib.Logic.Equiv.Defs
 public import Batteries.Lean.Except
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # Monad
 

Mathlib/Control/Traversable/Basic.lean

@@ -10,6 +10,8 @@ public import Mathlib.Control.Functor
 public import Batteries.Data.List.Basic
 public import Mathlib.Control.Basic
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # Traversable type class
 

Mathlib/Control/Traversable/Equiv.lean

@@ -9,6 +9,8 @@ public import Mathlib.Control.Traversable.Lemmas
 public import Mathlib.Logic.Equiv.Defs
 public import Batteries.Tactic.SeqFocus
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # Transferring `Traversable` instances along isomorphisms
 

Mathlib/Control/Traversable/Lemmas.lean

@@ -8,6 +8,8 @@ module
 public import Mathlib.Control.Applicative
 public import Mathlib.Control.Traversable.Basic
 
+import Mathlib.Tactic.Attr.Register
+
 /-!
 # Traversing collections