chore: bump toolchain to v4.23.0-rc2 (#28454)

Author: kim-em

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -119,13 +119,13 @@ theorem counted_succ_succ (p q : ℕ) :
           Nat.add_sub_cancel]
       · rw [List.count_tail, hl₁, List.head?_eq_head, hlast, if_neg (by decide), Nat.sub_zero]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
-      · rw [← hlast, List.head_cons_tail]
+      · rw [← hlast, List.cons_head_tail]
     · refine Or.inr ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
       · rw [List.count_tail, hl₀, List.head?_eq_head, hlast, if_neg (by decide), Nat.sub_zero]
       · rw [List.count_tail, hl₁, List.head?_eq_head, hlast, beq_self_eq_true, if_pos rfl,
           Nat.add_sub_cancel]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
-      · rw [← hlast, List.head_cons_tail]
+      · rw [← hlast, List.cons_head_tail]
   · rintro (⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩ | ⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩)
     · refine ⟨?_, ?_, ?_⟩
       · rw [List.count_cons, beq_self_eq_true, if_pos rfl, ht₀]

Cache/IO.lean

@@ -325,39 +325,43 @@ def allExist (paths : List (FilePath × Bool)) : IO Bool := do
     if required then if !(← path.pathExists) then return false
   pure true
 
+private structure PackTask where
+  sourceFile : FilePath
+  zip : String
+  task? : Option (Task (Except IO.Error Unit))
+
 /-- Compresses build files into the local cache and returns an array with the compressed files -/
 def packCache (hashMap : ModuleHashMap) (overwrite verbose unpackedOnly : Bool)
     (comment : Option String := none) :
     CacheM <| Array String := do
   IO.FS.createDirAll CACHEDIR
   IO.println "Compressing cache"
   let sp := (← read).srcSearchPath
-  let mut acc := #[]
-  let mut tasks := #[]
+  let mut acc : Array PackTask := #[]
   for (mod, hash) in hashMap.toList do
     let sourceFile ← Lean.findLean sp mod
     let zip := hash.asLTar
     let zipPath := CACHEDIR / zip
     let buildPaths ← mkBuildPaths mod
     if ← allExist buildPaths then
       if overwrite || !(← zipPath.pathExists) then
-        acc := acc.push (sourceFile, zip)
-        tasks := tasks.push <| ← IO.asTask do
+        let task ← IO.asTask do
           -- Note here we require that the `.trace` file is first
           -- in the list generated by `mkBuildPaths`.
           let trace :: args := (← buildPaths.filterM (·.1.pathExists)) |>.map (·.1.toString)
             | unreachable!
-          runCmd (← getLeanTar) <| #[zipPath.toString, trace] ++
+          discard <| runCmd (← getLeanTar) <| #[zipPath.toString, trace] ++
             (if let some c := comment then #["-c", s!"git=mathlib4@{c}"] else #[]) ++ args
+        acc := acc.push {sourceFile, zip, task? := some task}
       else if !unpackedOnly then
-        acc := acc.push (sourceFile, zip)
-  for task in tasks do
-    _ ← IO.ofExcept task.get
-  acc := acc.qsort (·.1.1 < ·.1.1)
-  if verbose then
-    for (path, zip) in acc do
-      println! "packing {path} as {zip}"
-  return acc.map (·.2)
+        acc := acc.push {sourceFile, zip, task? := none}
+  acc := acc.qsort (·.sourceFile.toString < ·.sourceFile.toString)
+  acc.mapM fun {sourceFile, zip, task?} => do
+    if let some task := task? then
+      if verbose then
+        IO.println s!"packing {sourceFile} as {zip}"
+      IO.ofExcept task.get
+    return zip
 
 /-- Gets the set of all cached files -/
 def getLocalCacheSet : IO <| Std.TreeSet String compare := do

Cache/Requests.lean

@@ -240,8 +240,8 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
   IO.println s!"Using cache from {remoteName}: {repo}"
   return {repo := repo, useFirst := false}
 
--- FRO cache is flaky so disable until we work out the kinks: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
-def useFROCache : Bool := false
+-- FRO cache may be flaky: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
+def useFROCache : Bool := true
 
 /-- Public URL for mathlib cache -/
 def URL : String :=
@@ -266,7 +266,7 @@ Given a file name like `"1234.tar.gz"`, makes the URL to that file on the server
 The `f/` prefix means that it's a common file for caching.
 -/
 def mkFileURL (repo URL fileName : String) : String :=
-  let pre := if repo == MATHLIBREPO then "" else s!"{repo}/"
+  let pre := if !useFROCache && repo == MATHLIBREPO then "" else s!"{repo}/"
   s!"{URL}/f/{pre}{fileName}"
 
 section Get

Counterexamples/MapFloor.lean

@@ -46,22 +46,14 @@ open scoped Polynomial
 
 /-- The integers with infinitesimals adjoined. -/
 def IntWithEpsilon :=
-  ℤ[X] deriving Nontrivial
+  ℤ[X] deriving Nontrivial, CommRing, Inhabited
 
 local notation "ℤ[ε]" => IntWithEpsilon
 
 local notation "ε" => (X : ℤ[ε])
 
 namespace IntWithEpsilon
 
-instance nontrivial : Nontrivial IntWithEpsilon := inferInstance
-
--- The `CommRing` and `Inhabited` instances should be constructed by a deriving handler.
--- https://github.com/leanprover-community/mathlib4/issues/380
-instance commRing : CommRing IntWithEpsilon := Polynomial.commRing
-
-instance inhabited : Inhabited IntWithEpsilon := ⟨69⟩
-
 instance linearOrder : LinearOrder ℤ[ε] :=
   LinearOrder.lift' (toLex ∘ coeff) coeff_injective
 

Counterexamples/SorgenfreyLine.lean

@@ -46,23 +46,12 @@ noncomputable section
 It is the real line with the topology space structure generated by
 half-open intervals `Set.Ico a b`. -/
 def SorgenfreyLine : Type := ℝ
--- The `ConditionallyCompleteLinearOrder, LinearOrderedField, Archimedean` instances should be
--- constructed by a deriving handler.
--- https://github.com/leanprover-community/mathlib4/issues/380
+deriving ConditionallyCompleteLinearOrder, Field, IsStrictOrderedRing, Archimedean
 
 @[inherit_doc]
 scoped[SorgenfreyLine] notation "ℝₗ" => Counterexample.SorgenfreyLine
 open scoped SorgenfreyLine
 
-instance : ConditionallyCompleteLinearOrder ℝₗ :=
-  inferInstanceAs (ConditionallyCompleteLinearOrder ℝ)
-
-instance : Field ℝₗ := inferInstanceAs (Field ℝ)
-
-instance : IsStrictOrderedRing ℝₗ := inferInstanceAs (IsStrictOrderedRing ℝ)
-
-instance : Archimedean ℝₗ := inferInstanceAs (Archimedean ℝ)
-
 namespace SorgenfreyLine
 
 /-- Ring homomorphism between the Sorgenfrey line and the standard real line. -/

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -502,7 +502,7 @@ theorem prod_bij_ne_one {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ 
       prod_bij (fun a ha => i a (mem_filter.mp ha).1 <| by simpa using (mem_filter.mp ha).2)
         ?_ ?_ ?_ ?_
     _ = ∏ x ∈ t, g x := prod_filter_ne_one _
-  · grind [mem_filter]
+  · grind
   · solve_by_elim
   · intros b hb
     refine (mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -554,7 +554,7 @@ The natural transformation from identity functor to the composition of restricti
 of scalars.
 -/
 @[simps]
-protected def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙ coextendScalars f where
+protected noncomputable def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙ coextendScalars f where
   app Y := ofHom (app' f Y)
   naturality Y Y' g :=
     hom_ext <| LinearMap.ext fun y : Y => LinearMap.ext fun s : S => by

Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean

@@ -146,12 +146,7 @@ theorem compExactValue_correctness_of_stream_eq_some :
       -- ifp_succ_n.fr ≠ 0
       -- use the IH to show that the following equality suffices
       suffices
-        compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr by
-        #adaptation_note /-- 2025-08-10 replace the following with grind after
-        https://github.com/leanprover/lean4/issues/9825 is fixed -/
-        have : v = compExactValue ppconts pconts ifp_n.fr := IH nth_stream_eq
-        conv_lhs => rw [this]
-        assumption
+        compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr by grind
       -- get the correspondence between ifp_n and ifp_succ_n
       obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_ne_zero, ⟨refl⟩⟩ :
         ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
@@ -196,12 +191,7 @@ theorem compExactValue_correctness_of_stream_eq_some :
       field_simp [compExactValue, contsAux_recurrence s_nth_eq ppconts_eq pconts_eq,
         nextConts, nextNum, nextDen]
       have hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f := rfl
-      #adaptation_note /-- 2025-08-10 replace the following with grind after
-        https://github.com/leanprover/lean4/issues/9825 is fixed -/
-      rw [one_div, if_neg _, ← one_div, hfr]
-      · field_simp [pA, pB, ppA, ppB, pconts, ppconts, hA, hB]
-        ac_rfl
-      · rwa [inv_eq_one_div, hfr]
+      grind
 
 open GenContFract (of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none)
 

Mathlib/Algebra/DirectSum/Basic.lean

@@ -33,21 +33,7 @@ variable (ι : Type v) (β : ι → Type w)
 Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum ι β`. -/
 def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
   Π₀ i, β i
-
--- The `AddCommMonoid, Inhabited` instances should be constructed by a deriving handler.
--- https://github.com/leanprover-community/mathlib4/issues/380
-
-instance [∀ i, AddCommMonoid (β i)] : Inhabited (DirectSum ι β) :=
-  inferInstanceAs (Inhabited (Π₀ i, β i))
-
-instance [∀ i, AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β) :=
-  inferInstanceAs (AddCommMonoid (Π₀ i, β i))
-
-instance [∀ i, AddCommMonoid (β i)] : DFunLike (DirectSum ι β) _ fun i : ι => β i :=
-  inferInstanceAs (DFunLike (Π₀ i, β i) _ _)
-
-instance [∀ i, AddCommMonoid (β i)] : CoeFun (DirectSum ι β) fun _ => ∀ i : ι, β i :=
-  inferInstanceAs (CoeFun (Π₀ i, β i) fun _ => ∀ i : ι, β i)
+deriving AddCommMonoid, Inhabited, DFunLike, CoeFun
 
 /-- `⨁ i, f i` is notation for `DirectSum _ f` and equals the direct sum of `fun i ↦ f i`.
 Taking the direct sum over multiple arguments is possible, e.g. `⨁ (i) (j), f i j`. -/

Mathlib/Algebra/Field/Basic.lean

@@ -158,6 +158,13 @@ variable [Field K]
 
 instance (priority := 100) Field.toGrindField [Field K] : Lean.Grind.Field K :=
   { CommRing.toGrindCommRing K, ‹Field K› with
+    zpow := ⟨fun a n => a^n⟩
+    zpow_zero a := by simp
+    zpow_succ a n := by
+      by_cases h : a = 0
+      · rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
+      · rw [zpow_add_one₀ h]
+    zpow_neg a n := by simp
     zero_ne_one := zero_ne_one' K }
 
 attribute [local simp] mul_assoc mul_comm mul_left_comm