Update lean-toolchain for leanprover/lean4#8883

Author: leanprover-community-mathlib4-bot

.github/workflows/nightly_detect_failure.yml

@@ -22,7 +22,7 @@ jobs:
         type: 'stream'
         topic: 'Batteries status updates'
         content: |
-          ❌ The latest CI for Batteries' branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
+          ❌ The latest CI for Batteries' [nightly-testing branch](https://github.com/${{ github.repository }}/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
           You can `git fetch; git checkout nightly-testing` and push a fix.
 
   handle_success:
@@ -84,13 +84,13 @@ jobs:
         }
         response = client.get_messages(request)
         messages = response['messages']
-        if not messages or messages[0]['content'] != f"✅ The latest CI for Batteries' branch#nightly-testing has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))":
+        if not messages or messages[0]['content'] != f"✅ The latest CI for Batteries' [nightly-testing branch](https://github.com/${{ github.repository }}/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))":
             # Post the success message
             request = {
                 'type': 'stream',
                 'to': 'nightly-testing',
                 'topic': 'Batteries status updates',
-                'content': f"✅ The latest CI for Batteries' branch#nightly-testing has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
+                'content': f"✅ The latest CI for Batteries' [nightly-testing branch](https://github.com/${{ github.repository }}/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
             }
             result = client.send_message(request)
             print(result)

.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.lean

@@ -1,16 +1,19 @@
 import Batteries.Classes.Cast
+import Batteries.Classes.Deprecated
 import Batteries.Classes.Order
 import Batteries.Classes.RatCast
 import Batteries.Classes.SatisfiesM
 import Batteries.CodeAction
 import Batteries.CodeAction.Attr
 import Batteries.CodeAction.Basic
 import Batteries.CodeAction.Deprecated
+import Batteries.CodeAction.Match
 import Batteries.CodeAction.Misc
 import Batteries.Control.AlternativeMonad
 import Batteries.Control.ForInStep
 import Batteries.Control.ForInStep.Basic
 import Batteries.Control.ForInStep.Lemmas
+import Batteries.Control.LawfulMonadState
 import Batteries.Control.Lemmas
 import Batteries.Control.Monad
 import Batteries.Control.Nondet.Basic

Batteries/Classes/Deprecated.lean

@@ -3,7 +3,6 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro, Gabriel Ebner
 -/
-import Batteries.Data.Rat.Basic
 
 /-- Type class for the canonical homomorphism `Rat → K`. -/
 class RatCast (K : Type u) where

Batteries/Classes/Order.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Kim Morrison
 -/
 import Batteries.Lean.EStateM
 import Batteries.Lean.Except
-import Batteries.Tactic.Lint
 
 /-!
 ## SatisfiesM
@@ -50,7 +49,7 @@ namespace SatisfiesM
 /-- If `p` is always true, then every `x` satisfies it. -/
 theorem of_true [Functor m] [LawfulFunctor m] {x : m α}
     (h : ∀ a, p a) : SatisfiesM p x :=
-  ⟨(fun a => ⟨a, h a⟩) <$> x, by simp [← comp_map, Function.comp_def]⟩
+  ⟨(fun a => ⟨a, h a⟩) <$> x, by simp⟩
 
 /--
 If `p` is always true, then every `x` satisfies it.
@@ -69,7 +68,7 @@ protected theorem map [Functor m] [LawfulFunctor m] {x : m α}
     (hx : SatisfiesM p x) (hf : ∀ {a}, p a → q (f a)) : SatisfiesM q (f <$> x) := by
   let ⟨x', hx⟩ := hx
   refine ⟨(fun ⟨a, h⟩ => ⟨f a, hf h⟩) <$> x', ?_⟩
-  rw [← hx]; simp [← comp_map, Function.comp_def]
+  rw [← hx]; simp
 
 /--
 `SatisfiesM` distributes over `<$>`, strongest postcondition version.
@@ -102,7 +101,7 @@ protected theorem seq [Applicative m] [LawfulApplicative m] {x : m α}
     (H : ∀ {f a}, p₁ f → p₂ a → q (f a)) : SatisfiesM q (f <*> x) := by
   match f, x, hf, hx with | _, _, ⟨f, rfl⟩, ⟨x, rfl⟩ => ?_
   refine ⟨(fun ⟨a, h₁⟩ ⟨b, h₂⟩ => ⟨a b, H h₁ h₂⟩) <$> f <*> x, ?_⟩
-  simp only [← pure_seq]; simp [SatisfiesM, seq_assoc]
+  simp only [← pure_seq]; simp [seq_assoc]
   simp only [← pure_seq]; simp [seq_assoc, Function.comp_def]
 
 /-- `SatisfiesM` distributes over `<*>`, strongest postcondition version. -/
@@ -210,7 +209,7 @@ theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
   · exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, nofun⟩) <$> f
     show _ = _ >>= _; rw [← comp_map, map_eq_pure_bind]; congr; funext a; cases a <;> rfl
   · exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)
-    show _ >>= _ = _; simp [← comp_map, ← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl
+    show _ >>= _ = _; simp [← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl
 
 /--
 If a monad has `MonadSatisfying m`, then we can lift a `h : SatisfiesM (m := m) p x` predicate
@@ -289,7 +288,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/Classes/RatCast.lean

@@ -1,3 +1,4 @@
 import Batteries.CodeAction.Attr
 import Batteries.CodeAction.Basic
 import Batteries.CodeAction.Misc
+import Batteries.CodeAction.Match

Batteries/Classes/SatisfiesM.lean

@@ -63,7 +63,7 @@ def TacticCodeActions.insert (self : TacticCodeActions)
     { self with onAnyTactic := self.onAnyTactic.push action }
   else
     { self with onTactic := tacticKinds.foldl (init := self.onTactic) fun m a =>
-        m.insert a ((m.findD a #[]).push action) }
+        m.insert a ((m.getD a #[]).push action) }
 
 /-- An extension which collects all the tactic code actions. -/
 initialize tacticSeqCodeActionExt :

Batteries/CodeAction.lean

@@ -3,8 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Server.CodeActions
-import Batteries.CodeAction.Basic
+import Lean.Server.CodeActions.Provider
 
 /-!
 # Code action for @[deprecated] replacements