chore: update Mathlib dependencies 2024-08-12 (#15728)

kim-em · mathlib-bors[bot] · kim-em · commit a9c4c79d8f2b · 2024-08-12T11:58:20.000Z
Co-authored-by: mathlib-bors &lt;150093616+mathlib-bors@users.noreply.github.com&gt;
diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
+import Batteries.Tactic.Init
 import Mathlib.Logic.Function.Defs
 import Mathlib.Order.Defs
 
diff --git a/Mathlib/Data/Option/NAry.lean b/Mathlib/Data/Option/NAry.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Logic.Function.Defs
+import Batteries.Tactic.Init
 
 /-!
 # Binary map of options
diff --git a/Mathlib/Init/Set.lean b/Mathlib/Init/Set.lean
@@ -3,7 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Parser.Term
 import Batteries.Util.ExtendedBinder
 
 /-!
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import Mathlib.Logic.Nonempty
 import Mathlib.Init.Set
 import Mathlib.Logic.Basic
+import Batteries.Tactic.Init
 
 /-!
 # Miscellaneous function constructions and lemmas
diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard
 -/
+import Batteries.Tactic.Init
 import Mathlib.Tactic.PushNeg
 
 /-!
diff --git a/Mathlib/Tactic/DeprecateMe.lean b/Mathlib/Tactic/DeprecateMe.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-
+import Lean.Meta.Tactic.TryThis
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Tactic.Lemma
 
diff --git a/Mathlib/Tactic/ITauto.lean b/Mathlib/Tactic/ITauto.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Batteries.Logic
 import Batteries.Tactic.Exact
+import Batteries.Tactic.Init
 import Mathlib.Tactic.Hint
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Util.AtomM
diff --git a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Vasily Nesterov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasily Nesterov
 -/
+import Lean.Data.HashMap
 import Batteries.Data.Rat.Basic
 
 /-!
diff --git a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Vasily Nesterov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasily Nesterov
 -/
+import Lean.Meta.Basic
 import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
 
diff --git a/Mathlib/Tactic/Widget/InteractiveUnfold.lean b/Mathlib/Tactic/Widget/InteractiveUnfold.lean
@@ -7,6 +7,7 @@ import Batteries.Lean.Position
 import Mathlib.Tactic.Widget.SelectPanelUtils
 import Mathlib.Lean.GoalsLocation
 import Mathlib.Lean.Meta.KAbstractPositions
+import Lean.Util.FoldConsts
 
 /-!
 
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc167d260ff7ee9849b436037add06bed15104be",
+   "rev": "ad26fe1ebccc9d5b7ca9111d5daf9b4488374415",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0444234b4216e944d5be2ce42a25d7410c67876f",
+   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/scripts/noshake.json b/scripts/noshake.json
@@ -235,7 +235,8 @@
   "Mathlib.Tactic.Linter.UnusedTactic": ["Batteries.Tactic.Unreachable"],
   "Mathlib.Tactic.Lemma": ["Lean.Parser.Command"],
   "Mathlib.Tactic.IrreducibleDef": ["Mathlib.Data.Subtype"],
-  "Mathlib.Tactic.ITauto": ["Batteries.Logic", "Mathlib.Init.Logic"],
+  "Mathlib.Tactic.ITauto":
+  ["Batteries.Logic", "Batteries.Tactic.Init", "Mathlib.Init.Logic"],
   "Mathlib.Tactic.Group": ["Mathlib.Algebra.Group.Commutator"],
   "Mathlib.Tactic.GCongr.Core": ["Mathlib.Order.Defs"],
   "Mathlib.Tactic.GCongr": ["Mathlib.Tactic.Positivity.Core"],
@@ -279,6 +280,7 @@
    "Mathlib.Tactic.CategoryTheory.BicategoricalComp"],
   "Mathlib.Tactic.CC.Addition":
   ["Mathlib.Logic.Basic", "Mathlib.Tactic.CC.Lemmas"],
+  "Mathlib.Tactic.ByContra": ["Batteries.Tactic.Init"],
   "Mathlib.Tactic.Bound.Init": ["Aesop.Frontend.Command"],
   "Mathlib.Tactic.Bound.Attribute":
   ["Mathlib.Algebra.Group.ZeroOne", "Mathlib.Tactic.Bound.Init"],
@@ -312,6 +314,7 @@
   "Mathlib.MeasureTheory.MeasurableSpace.Defs": ["Mathlib.Tactic.FunProp.Attr"],
   "Mathlib.Logic.Nontrivial.Defs": ["Mathlib.Init.Logic"],
   "Mathlib.Logic.Function.Defs": ["Mathlib.Tactic.AdaptationNote"],
+  "Mathlib.Logic.Function.Basic": ["Batteries.Tactic.Init"],
   "Mathlib.Logic.Equiv.Defs": ["Mathlib.Data.Bool.Basic"],
   "Mathlib.Logic.Basic": ["Mathlib.Data.Int.Notation"],
   "Mathlib.LinearAlgebra.Matrix.Transvection": ["Mathlib.Data.Matrix.DMatrix"],
@@ -338,6 +341,7 @@
   "Mathlib.Data.Seq.Parallel": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Data.PEquiv": ["Batteries.Tactic.Congr"],
   "Mathlib.Data.Ordmap.Ordnode": ["Mathlib.Data.Option.Basic"],
+  "Mathlib.Data.Option.NAry": ["Batteries.Tactic.Init"],
   "Mathlib.Data.Nat.Find": ["Batteries.WF"],
   "Mathlib.Data.Multiset.Bind": ["Mathlib.Algebra.GroupWithZero.Action.Defs"],
   "Mathlib.Data.List.TFAE": ["Batteries.Tactic.Classical"],
@@ -352,6 +356,7 @@
   "Mathlib.Data.FunLike.Basic": ["Mathlib.Logic.Function.Basic"],
   "Mathlib.Data.Finset.Basic": ["Mathlib.Data.Finset.Attr"],
   "Mathlib.Data.DFinsupp.Notation": ["Mathlib.Data.Finsupp.Notation"],
+  "Mathlib.Data.Bool.Basic": ["Batteries.Tactic.Init"],
   "Mathlib.Control.Traversable.Instances": ["Mathlib.Control.Applicative"],
   "Mathlib.Control.Monad.Cont": ["Batteries.Tactic.Congr"],
   "Mathlib.Control.Basic": ["Mathlib.Logic.Function.Defs"],
