Update lean-toolchain for leanprover/lean4#8664

Author: leanprover-community-mathlib4-bot

.github/workflows/test_mathlib.yml

@@ -35,6 +35,12 @@ jobs:
           ref: master
           fetch-depth: 0
 
+      - name: Add nightly-testing remote
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
+        run: |
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing
+
       - name: Install elan
         if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
         run: |
@@ -85,4 +91,4 @@ jobs:
         env:
           PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
         run: |
-          git push origin batteries-pr-testing-$PR_NUMBER
+          git push nightly-testing batteries-pr-testing-$PR_NUMBER

Batteries/Classes/SatisfiesM.lean

@@ -289,7 +289,6 @@ instance : MonadSatisfying (EStateM ε σ) where
   val_eq {α p x} h := by
     ext s
     rw [EStateM.run_map, EStateM.run]
-    simp only
     split <;> simp_all
 
 end MonadSatisfying

Batteries/Data/Array/Basic.lean

@@ -163,9 +163,9 @@ def popHead? (as : Subarray α) : Option (α × Subarray α) :=
     then
       let head := as.array[as.start]'(Nat.lt_of_lt_of_le h as.stop_le_array_size)
       let tail :=
-        { as with
-          start := as.start + 1
-          start_le_stop := Nat.le_of_lt_succ $ Nat.succ_lt_succ h }
+        ⟨{ as.internalRepresentation with
+           start := as.start + 1
+           start_le_stop := Nat.le_of_lt_succ $ Nat.succ_lt_succ h }⟩
       some (head, tail)
     else
       none

Batteries/Data/Array/Lemmas.lean

@@ -26,22 +26,6 @@ theorem idxOf?_toList [BEq α] {a : α} {l : Array α} :
   rcases l with ⟨l⟩
   simp
 
-/-! ### finIdxOf? -/
-
--- forward-port of https://github.com/leanprover/lean4/pull/8678
-@[simp]
-theorem isSome_finIdxOf?_eq [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
-    (xs.finIdxOf? a).isSome = xs.contains a := by
-  rcases xs with ⟨xs⟩
-  simp [Array.size]
-
--- forward-port of https://github.com/leanprover/lean4/pull/8678
-@[simp]
-theorem isNone_finIdxOf?_eq [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
-    (xs.finIdxOf? a).isNone = !xs.contains a := by
-  rcases xs with ⟨xs⟩
-  simp [Array.size]
-
 /-! ### erase -/
 
 @[deprecated (since := "2025-02-06")] alias eraseP_toArray := List.eraseP_toArray

Batteries/Data/BitVec/Lemmas.lean

@@ -52,16 +52,20 @@ theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
 @[simp] theorem getElem_ofFnLE (f : Fin n → Bool) (i) (h : i < n) : (ofFnLE f)[i] = f ⟨i, h⟩ :=
   getElem_ofFnLEAux ..
 
-theorem getLsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getLsb' i = f i := by simp
+theorem getLsb_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getLsb i = f i := by simp
+
+@[deprecated (since := "2025-06-17")] alias getLsb'_ofFnLE := getLsb_ofFnLE
 
 theorem getLsbD_ofFnLE (f : Fin n → Bool) (i) :
     (ofFnLE f).getLsbD i = if h : i < n then f ⟨i, h⟩ else false := by
   split
   · next h => rw [getLsbD_eq_getElem h, getElem_ofFnLE]
   · next h => rw [getLsbD_of_ge _ _ (Nat.ge_of_not_lt h)]
 
-@[simp] theorem getMsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getMsb' i = f i.rev := by
-  simp [getMsb'_eq_getLsb', Fin.rev]; congr 2; omega
+@[simp] theorem getMsb_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getMsb i = f i.rev := by
+  simp [getMsb_eq_getLsb, Fin.rev]; congr 2; omega
+
+@[deprecated (since := "2025-06-17")] alias getMsb'_ofFnLE := getMsb_ofFnLE
 
 theorem getMsbD_ofFnLE (f : Fin n → Bool) (i) :
     (ofFnLE f).getMsbD i = if h : i < n then f (Fin.rev ⟨i, h⟩) else false := by
@@ -88,16 +92,20 @@ theorem msb_ofFnLE (f : Fin n → Bool) :
 @[simp] theorem getElem_ofFnBE (f : Fin n → Bool) (i) (h : i < n) :
     (ofFnBE f)[i] = f (Fin.rev ⟨i, h⟩) := by simp [ofFnBE]
 
-theorem getLsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getLsb' i = f i.rev := by
+theorem getLsb_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getLsb i = f i.rev := by
   simp
 
+@[deprecated (since := "2025-06-17")] alias getLsb'_ofFnBE := getLsb_ofFnBE
+
 theorem getLsbD_ofFnBE (f : Fin n → Bool) (i) :
     (ofFnBE f).getLsbD i = if h : i < n then f (Fin.rev ⟨i, h⟩) else false := by
   simp [ofFnBE, getLsbD_ofFnLE]
 
-@[simp] theorem getMsb'_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getMsb' i = f i := by
+@[simp] theorem getMsb_ofFnBE (f : Fin n → Bool) (i) : (ofFnBE f).getMsb i = f i := by
   simp [ofFnBE]
 
+@[deprecated (since := "2025-06-17")] alias getMsb'_ofFnBE := getMsb_ofFnBE
+
 theorem getMsbD_ofFnBE (f : Fin n → Bool) (i) :
     (ofFnBE f).getMsbD i = if h : i < n then f ⟨i, h⟩ else false := by
   simp [ofFnBE, getMsbD_ofFnLE]

Batteries/Data/List/Lemmas.lean

@@ -26,7 +26,7 @@ theorem dropLast_eq_eraseIdx {xs : List α} {i : Nat} (last_idx : i + 1 = xs.len
     xs.dropLast = List.eraseIdx xs i := by
   induction i generalizing xs with
   | zero =>
-    let [x] := xs
+    let ([x]) := xs
     rfl
   | succ n ih =>
     let x::xs := xs

Batteries/Lean/Meta/Simp.lean

@@ -57,22 +57,8 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
   let congrTheorems ← Meta.getSimpCongrTheorems
   let ctx ← Simp.mkContext (← elabSimpConfig stx[1] (kind := kind)) #[simpTheorems] congrTheorems
   let r ← elabSimpArgs stx[4] (simprocs := #[simprocs]) ctx eraseLocal kind
-  if !r.starArg || ignoreStarArg then
-    return { r with dischargeWrapper }
-  else
-    let ctx := r.ctx
-    let mut simpTheorems := ctx.simpTheorems
-    let simprocs := r.simprocs
-    /-
-    When using `zeta := false`, we do not expand let-declarations when using `[*]`.
-    Users must explicitly include it in the list.
-    -/
-    let hs ← getPropHyps
-    for h in hs do
-      unless simpTheorems.isErased (.fvar h) do
-        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    let ctx := ctx.setSimpTheorems simpTheorems
-    return { ctx, simprocs, dischargeWrapper }
+    (ignoreStarArg := ignoreStarArg)
+  return { r with dischargeWrapper }
 
 
 end Simp

Batteries/Tactic/Alias.lean

@@ -87,7 +87,9 @@ elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident :
     let declMods ← elabModifiers mods
     let (attrs, machineApplicable) := setDeprecatedTarget name declMods.attrs
     let declMods := { declMods with
-      isNoncomputable := declMods.isNoncomputable || isNoncomputable (← getEnv) name
+      computeKind :=
+        if isNoncomputable (← getEnv) name then .noncomputable
+        else declMods.computeKind
       isUnsafe := declMods.isUnsafe || cinfo.isUnsafe
       attrs
     }

Batteries/Tactic/Lint/Basic.lean

@@ -43,9 +43,8 @@ def isAutoDecl (decl : Name) : CoreM Bool := do
     if env.isConstructor n && ["injEq", "inj", "sizeOf_spec"].any (· == s) then
       return true
     if let ConstantInfo.inductInfo _ := (← getEnv).find? n then
-      if s.startsWith "brecOn_" || s.startsWith "below_" || s.startsWith "binductionOn_"
-        || s.startsWith "ibelow_" then return true
-      if [casesOnSuffix, recOnSuffix, brecOnSuffix, binductionOnSuffix, belowSuffix, "ibelow",
+      if s.startsWith "brecOn_" || s.startsWith "below_" then return true
+      if [casesOnSuffix, recOnSuffix, brecOnSuffix, belowSuffix,
           "ndrec", "ndrecOn", "noConfusionType", "noConfusion", "ofNat", "toCtorIdx"
         ].any (· == s) then
         return true

Batteries/Tactic/Lint/Frontend.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
 -/
-import Lean.Util.Paths
 import Lean.Elab.Command
 import Batteries.Tactic.Lint.Basic
 import Batteries.Tactic.OpenPrivate