refactor: [Lean PR testing] Resolve breakage from leanprover/lean#11163

Aesop/Script/OptimizeSyntax.lean

@@ -27,7 +27,7 @@ partial def optimizeFocusRenameI : Syntax → m Syntax
         | return stx
       match tac with
       | `(tactic| rename_i $[$ns:ident]*) =>
-        `(tactic| next $[$ns:ident]* => $(tacs[1:]):tactic*)
+        `(tactic| next $[$ns:ident]* => $(tacs[1...*].copy):tactic*)
       | _ => return stx
     | _ => return stx
 
@@ -55,13 +55,13 @@ def optimizeInitialRenameI : Syntax → m Syntax
       if dropUntil == 0 then
         return stx
       else if dropUntil == ns.size then
-        tacsToTacticSeq tacs[1:]
+        tacsToTacticSeq tacs[1...*].copy
       else
         let ns : TSyntaxArray `ident := ns[dropUntil:].toArray
         let tac ← `(tactic| rename_i $[$ns:ident]*)
         let mut result : Array (TSyntax `tactic) := Array.mkEmpty tacs.size
         result := result.push tac
-        result := result ++ tacs[1:]
+        result := result ++ tacs[1...*].copy
         tacsToTacticSeq result
     | _ => return stx
   | stx => return stx

Aesop/Script/StructureDynamic.lean

@@ -150,7 +150,7 @@ where
         postGoals := postGoalsWithMVars
         preState, preGoal, postState
       }
-      let postGoals := preGoals[:goalPos] ++ postGoals ++ preGoals[goalPos+1:]
+      let postGoals := preGoals[*...goalPos].copy ++ postGoals ++ preGoals[(goalPos+1)...*].copy
       let postGoals ← postState.runMetaM' do
         postGoals.filterM λ mvarId =>
           return ! (← mvarId.isAssignedOrDelayedAssigned)

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cd62e382d42d8daffeb7786e0ff1626aea5b65ca",
+   "rev": "7f8f80fac7707b4ccb11f28ac9876752437b3c9a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-11-10
+leanprover/lean4-pr-releases:pr-release-11163-68a4aa4