chore: Revert "chore: deprecate Traversable deriving handler (leanprover-community#29573)" (leanprover-community#29931)

This reverts commit f4506f7.

Author: kim-em

Mathlib.lean

@@ -3744,7 +3744,6 @@ import Mathlib.Deprecated.Estimator
 import Mathlib.Deprecated.MLList.BestFirst
 import Mathlib.Deprecated.Order
 import Mathlib.Deprecated.RingHom
-import Mathlib.Deprecated.Tactic.DeriveTraversable
 import Mathlib.Dynamics.BirkhoffSum.Average
 import Mathlib.Dynamics.BirkhoffSum.Basic
 import Mathlib.Dynamics.BirkhoffSum.NormedSpace
@@ -6093,6 +6092,7 @@ import Mathlib.Tactic.DeprecateTo
 import Mathlib.Tactic.DeriveCountable
 import Mathlib.Tactic.DeriveEncodable
 import Mathlib.Tactic.DeriveFintype
+import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.ENatToNat
 import Mathlib.Tactic.Eqns
 import Mathlib.Tactic.ErwQuestion

Mathlib/Tactic.lean

@@ -72,6 +72,7 @@ import Mathlib.Tactic.DeprecateTo
 import Mathlib.Tactic.DeriveCountable
 import Mathlib.Tactic.DeriveEncodable
 import Mathlib.Tactic.DeriveFintype
+import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.ENatToNat
 import Mathlib.Tactic.Eqns
 import Mathlib.Tactic.ErwQuestion

…Deprecated/Tactic/DeriveTraversable.lean Mathlib/Tactic/DeriveTraversable.leanMathlib/Deprecated/Tactic/DeriveTraversable.lean renamed to Mathlib/Tactic/DeriveTraversable.lean Mathlib/Deprecated/Tactic/DeriveTraversable.lean renamed to Mathlib/Tactic/DeriveTraversable.lean

@@ -11,8 +11,6 @@ import Lean.Elab.PreDefinition.Main
 /-!
 # Deriving handler for `Traversable` instances
 
-Note: this module was deprecated on 2025-09-11.
-
 This module gives deriving handlers for `Functor`, `LawfulFunctor`, `Traversable`, and
 `LawfulTraversable`. These deriving handlers automatically derive their dependencies, for
 example `deriving LawfulTraversable` all by itself gives all four.
@@ -495,13 +493,10 @@ def deriveLawfulTraversable (m : MVarId) : TermElabM Unit := do
     m.refl
 
 /-- The deriving handler for `LawfulTraversable`. -/
-@[deprecated "This has not been used in Mathlib for some time, and broke on nightly-2025-09-11. \
-  Without an active maintainer, it has been deprecated." (since := "2025-09-11")]
 def lawfulTraversableDeriveHandler : DerivingHandler :=
   higherOrderDeriveHandler ``LawfulTraversable deriveLawfulTraversable
     [traversableDeriveHandler, lawfulFunctorDeriveHandler] (fun n arg => mkAppOptM n #[arg, none])
 
-set_option linter.deprecated false in
 initialize registerDerivingHandler ``LawfulTraversable lawfulTraversableDeriveHandler
 
 end Mathlib.Deriving.Traversable

MathlibTest/Traversable.lean

@@ -1,4 +1,4 @@
-import Mathlib.Deprecated.Tactic.DeriveTraversable
+import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Control.Traversable.Instances
 
 set_option linter.style.commandStart false