chore: bump toolchain to v4.27.0-rc1 (#1560)

Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Parth Shastri <31370288+cppio@users.noreply.github.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Sebastian Graf <sgraf1337@gmail.com>
Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
Co-authored-by: Eric Wieser <efw@google.com>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

Author: 23 people

Batteries.lean

@@ -113,4 +113,3 @@ public import Batteries.Util.LibraryNote
 public import Batteries.Util.Panic
 public import Batteries.Util.Pickle
 public import Batteries.Util.ProofWanted
-public import Batteries.WF

Batteries/Control/OptionT.lean

@@ -24,9 +24,6 @@ namespace OptionT
 @[simp] theorem run_mapConst [Monad m] [LawfulMonad m] (x : OptionT m α) (y : β) :
     (Functor.mapConst y x).run = Option.map (Function.const α y) <$> x.run := run_map _ _
 
-@[simp] theorem run_monadMap {n} [MonadFunctorT n m] (f : ∀ {α}, n α → n α) :
-    (monadMap (@f) x : OptionT m α).run = monadMap (@f) x.run := (rfl)
-
 instance [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] :
     LawfulMonadStateOf σ (OptionT m) where
   modifyGet_eq f := by simp [← liftM_modifyGet, ← liftM_get, LawfulMonadStateOf.modifyGet_eq]

Batteries/Data/AssocList.lean

@@ -242,7 +242,7 @@ with key equal to `a` to have key `a` and value `f a' b`.
     | ForInStep.done d  => pure d
     | ForInStep.yield d => es.forIn d f
 
-instance : ForIn m (AssocList α β) (α × β) where
+instance [Monad m] : ForIn m (AssocList α β) (α × β) where
   forIn := AssocList.forIn
 
 @[simp] theorem forIn_eq [Monad m] (l : AssocList α β) (init : δ)

Batteries/Data/BinomialHeap/Basic.lean

@@ -545,7 +545,7 @@ which iterates over the elements in the heap in increasing order.
 protected def forIn [Monad m] (b : BinomialHeap α le) (x : β) (f : α → β → m (ForInStep β)) : m β :=
   ForInStep.run <$> b.1.foldM le (.yield x) fun x a => x.bind (f a)
 
-instance : ForIn m (BinomialHeap α le) α := ⟨BinomialHeap.forIn⟩
+instance [Monad m] : ForIn m (BinomialHeap α le) α := ⟨BinomialHeap.forIn⟩
 
 /-- `O(log n)`. Returns the smallest element in the heap, or `none` if the heap is empty. -/
 @[inline] def head? (b : BinomialHeap α le) : Option α := b.1.head? le

Batteries/Data/ByteSlice.lean

@@ -51,7 +51,7 @@ where
       | ForInStep.done b  => pure b
       | ForInStep.yield b => loop i (Nat.le_of_succ_le h) b
 
-instance : ForIn m ByteSlice UInt8 where
+instance [Monad m] : ForIn m ByteSlice UInt8 where
   forIn := ByteSlice.forIn
 
 instance : Std.Stream ByteSlice UInt8 where
@@ -169,7 +169,7 @@ where
       | ForInStep.done b  => pure b
       | ForInStep.yield b => loop i (Nat.le_of_succ_le h) b
 
-instance : ForIn m ByteSubarray UInt8 where
+instance [Monad m] : ForIn m ByteSubarray UInt8 where
   forIn := ByteSubarray.forIn
 
 instance : Std.Stream ByteSubarray UInt8 where

Batteries/Data/List/Lemmas.lean

@@ -543,7 +543,7 @@ theorem findIdxs_append :
 @[simp, grind =]
 theorem findIdxs_take :
     ((xs : List α).take n).findIdxs p s = (xs.findIdxs p s).take ((xs.take n).countP p) := by
-  induction xs generalizing n s <;> cases n <;> grind
+  induction xs generalizing n s <;> cases n <;> grind [countP_eq_length_filter]
 
 @[simp, grind =>]
 theorem le_getElem_findIdxs (h : i < ((xs : List α).findIdxs p s).length) :

Batteries/Data/MLList/Basic.lean

@@ -115,7 +115,7 @@ private local instance [Monad n] : Inhabited (δ → (α → δ → n (ForInStep
       | ForInStep.done d  => pure d
       | ForInStep.yield d => t.forIn d f
 
-instance [Monad m] [MonadLiftT m n] : ForIn n (MLList m α) α where
+instance [Monad m] [Monad n] [MonadLiftT m n] : ForIn n (MLList m α) α where
   forIn := MLList.forIn
 
 /-- Construct a singleton monadic lazy list from a single monadic value. -/

Batteries/Data/RBMap/Basic.lean

@@ -115,7 +115,7 @@ where
     | nil,          b => return ForInStep.yield b
     | node _ l v r, b => ForInStep.bindM (visit l b) fun b => ForInStep.bindM (f v b) (visit r ·)
 
-instance : ForIn m (RBNode α) α where
+instance [Monad m] : ForIn m (RBNode α) α where
   forIn := RBNode.forIn
 
 /--
@@ -658,7 +658,7 @@ instance (α : Type u) (cmp : α → α → Ordering) : Inhabited (RBSet α cmp)
 /-- `O(n)`. Run monadic function `f` on each element of the tree (in increasing order). -/
 @[inline] def forM [Monad m] (f : α → m PUnit) (t : RBSet α cmp) : m PUnit := t.1.forM f
 
-instance : ForIn m (RBSet α cmp) α where
+instance [Monad m] : ForIn m (RBSet α cmp) α where
   forIn t := t.1.forIn
 
 instance : Std.ToStream (RBSet α cmp) (RBNode.Stream α) := ⟨fun x => x.1.toStream .nil⟩
@@ -944,7 +944,7 @@ variable {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering
 @[inline] def forM [Monad m] (f : α → β → m PUnit) (t : RBMap α β cmp) : m PUnit :=
   t.1.forM (fun (a, b) => f a b)
 
-instance : ForIn m (RBMap α β cmp) (α × β) := inferInstanceAs (ForIn _ (RBSet ..) _)
+instance [Monad m] : ForIn m (RBMap α β cmp) (α × β) := inferInstanceAs (ForIn _ (RBSet ..) _)
 
 instance : Std.ToStream (RBMap α β cmp) (RBNode.Stream (α × β)) :=
   inferInstanceAs (Std.ToStream (RBSet ..) _)
@@ -977,10 +977,10 @@ instance : CoeHead (Keys α β cmp) (Array α) := ⟨keysArray⟩
 
 instance : CoeHead (Keys α β cmp) (List α) := ⟨keysList⟩
 
-instance : ForIn m (Keys α β cmp) α where
+instance [Monad m] : ForIn m (Keys α β cmp) α where
   forIn t init f := t.val.forIn init (f ·.1)
 
-instance : ForM m (Keys α β cmp) α where
+instance [Monad m] : ForM m (Keys α β cmp) α where
   forM t f := t.val.forM (f ·.1)
 
 /-- The result of `toStream` on a `Keys`. -/
@@ -1026,10 +1026,10 @@ instance : CoeHead (Values α β cmp) (Array β) := ⟨valuesArray⟩
 
 instance : CoeHead (Values α β cmp) (List β) := ⟨valuesList⟩
 
-instance : ForIn m (Values α β cmp) β where
+instance [Monad m] : ForIn m (Values α β cmp) β where
   forIn t init f := t.val.forIn init (f ·.2)
 
-instance : ForM m (Values α β cmp) β where
+instance [Monad m] : ForM m (Values α β cmp) β where
   forM t f := t.val.forM (f ·.2)
 
 /-- The result of `toStream` on a `Values`. -/