diff --git a/Mathport/Syntax/Translate/Tactic/Mathlib/Misc2.lean b/Mathport/Syntax/Translate/Tactic/Mathlib/Misc2.lean
index 69f50ae0..9c9b761b 100644
--- a/Mathport/Syntax/Translate/Tactic/Mathlib/Misc2.lean
+++ b/Mathport/Syntax/Translate/Tactic/Mathlib/Misc2.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathport.Syntax.Translate.Tactic.Basic
 import Mathport.Syntax.Translate.Tactic.Lean3
 import Mathport.Syntax.Translate.Tactic.Mathlib.Cache
+import Mathlib.Tactic.MoveAdd
 
 -- Misc. special-purpose tactics
 
@@ -195,15 +196,21 @@ def trSubtypeInstance : TacM Syntax.Tactic := `(tactic| subtype_instance)
 -- # tactic.move_add
 
 @[tr_tactic move_add] def trMoveAdd : TacM Syntax.Tactic := do
-  `(tactic| move_add $(← liftM $ (← parse rwRules).mapM trRwRule),* $(← trLoc (← parse location))?)
+  let rules ← liftM $ (← parse rwRules).mapM trRwRule
+  let .targets #[] true ← parse location | warn! "unsupported: move_add at"
+  `(tactic| move_add [$rules,*])
 
 @[tr_tactic move_mul] def trMoveMul : TacM Syntax.Tactic := do
-  `(tactic| move_mul $(← liftM $ (← parse rwRules).mapM trRwRule),* $(← trLoc (← parse location))?)
+  let rules ← liftM $ (← parse rwRules).mapM trRwRule
+  let .targets #[] true ← parse location | warn! "unsupported: move_mul at"
+  `(tactic| move_mul [$rules,*])
 
 @[tr_tactic move_oper] def trMoveOper : TacM Syntax.Tactic := do
   let #[e] ← parse pExprList | warn! "unsupported: move_oper with multiple ops"
-  `(tactic| move_op $(← trExpr e)
-    $(← liftM $ (← parse rwRules).mapM trRwRule),* $(← trLoc (← parse location))?)
+  let .ident n := e.kind | warn! "unsupported: move_oper with non-ident"
+  let rules ← liftM $ (← parse rwRules).mapM trRwRule
+  let .targets #[] true ← parse location | warn! "unsupported: move_oper at"
+  `(tactic| move_oper $(← withSpanS e.meta (mkIdentI n)) [$rules,*])
 
 -- # tactic.print_sorry
 @[tr_user_cmd «#print_sorry_in»] def trPrintSorryIn : Parse1 Syntax.Command :=
diff --git a/lake-manifest.json b/lake-manifest.json
index d72905fa..f93a6067 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bba0af6e930ebcbabfacf021b21dd881d58aaa9d",
+   "rev": "dc4a6b1ac3cd502988e283d5c9c5fdf261125a07",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
+   "rev": "26b4e42e8e9c45c3ded44a4d161161bef430d446",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "17a95d6c8cfe5a6dec779187375268505245c934",
+   "rev": "ee4303e0103ba28f9106bd96ca5a66054fda6acc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",