shake update

leanprover-community · Oct 19, 2024 · 407a445 · 407a445
1 parent 4f6fe87
commit 407a445
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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"],