diff --git a/Mathlib/Algebra/BigOperators/Group/List.lean b/Mathlib/Algebra/BigOperators/Group/List.lean
index 08b3745443eb9..7944a074da49e 100644
--- a/Mathlib/Algebra/BigOperators/Group/List.lean
+++ b/Mathlib/Algebra/BigOperators/Group/List.lean
@@ -13,6 +13,7 @@ import Mathlib.Data.List.Range
 import Mathlib.Data.List.Rotate
 import Mathlib.Data.List.Pairwise
 import Mathlib.Data.List.Join
+import Mathlib.Data.List.ProdSigma
 
 /-!
 # Sums and products from lists
diff --git a/Mathlib/Order/Defs.lean b/Mathlib/Order/Defs.lean
index 14a3cebd9de8f..75d603ee2c080 100644
--- a/Mathlib/Order/Defs.lean
+++ b/Mathlib/Order/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Batteries.Classes.Order
+import Batteries.Tactic.Trans
 import Mathlib.Data.Ordering.Basic
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.SplitIfs
diff --git a/scripts/noshake.json b/scripts/noshake.json
index b0c52f7471209..97b19e40ac899 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -325,6 +325,7 @@
   "Mathlib.Order.RelClasses": ["Batteries.WF"],
   "Mathlib.Order.Filter.ListTraverse":
   ["Mathlib.Control.Traversable.Instances"],
+  "Mathlib.Order.Defs": ["Batteries.Tactic.Trans"],
   "Mathlib.NumberTheory.Harmonic.Defs":
   ["Mathlib.Algebra.Order.BigOperators.Ring.Finset",
    "Mathlib.Algebra.Order.Field.Basic"],
@@ -427,6 +428,7 @@
   ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"],
   "Mathlib.Algebra.Category.MonCat.Basic":
   ["Mathlib.Algebra.Ring.Action.Group"],
+  "Mathlib.Algebra.BigOperators.Group.List": ["Mathlib.Data.List.ProdSigma"],
   "Mathlib.Algebra.Algebra.Subalgebra.Order":
   ["Mathlib.Algebra.Module.Submodule.Order"],
   "Batteries.Tactic.OpenPrivate": ["Lean.Parser.Module"],