chore: bump toolchain to v4.27.0-rc1 (leanprover-community#32874)

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: leanprover-community-bot-assistant <97194829+leanprover-community-bot-assistant@users.noreply.github.com>

Author: 6 people

Archive/Imo/Imo2015Q6.lean

@@ -85,7 +85,7 @@ lemma pool_subset_Icc : ∀ {t}, pool a t ⊆ Icc 0 2014
   | t + 1 => by
     intro x hx
     simp_rw [pool, mem_map, Equiv.coe_toEmbedding, Equiv.subRight_apply] at hx
-    obtain ⟨y, my, ey⟩ := hx
+    obtain ⟨y, my, rfl⟩ := hx
     suffices y ∈ Icc 1 2015 by rw [mem_Icc] at this ⊢; lia
     rw [mem_insert, mem_erase] at my; rcases my with h | ⟨h₁, h₂⟩
     · exact h ▸ ha.1 t

Cache/IO.lean

@@ -142,7 +142,7 @@ private def CacheM.mathlibDepPath (sp : SearchPath) : IO FilePath := do
 def _root_.Lean.SearchPath.relativize (sp : SearchPath) : IO SearchPath := do
   let pwd ← IO.FS.realPath "."
   let pwd' := pwd.toString ++ System.FilePath.pathSeparator.toString
-  return sp.map fun x => ⟨if x = pwd then "." else x.toString.stripPrefix pwd'⟩
+  return sp.map fun x => ⟨if x = pwd then "." else x.toString.dropPrefix pwd' |>.copy⟩
 
 private def CacheM.getContext : IO CacheM.Context := do
   let sp ← (← getSrcSearchPath).relativize
@@ -208,8 +208,8 @@ def validateCurl : IO Bool := do
       let _ := @leOfOrd
       if version >= (7, 81) then return true
       -- TODO: support more platforms if the need arises
-      let arch ← (·.trim) <$> runCmd "uname" #["-m"] false
-      let kernel ← (·.trim) <$> runCmd "uname" #["-s"] false
+      let arch ← (·.trimAscii.copy) <$> runCmd "uname" #["-m"] false
+      let kernel ← (·.trimAscii.copy) <$> runCmd "uname" #["-s"] false
       if kernel == "Linux" && arch ∈ ["x86_64", "aarch64"] then
         IO.println s!"curl is too old; downloading more recent version"
         IO.FS.createDirAll IO.CACHEDIR
@@ -249,7 +249,7 @@ def validateLeanTar : IO Unit := do
   let target ← if win then
     pure "x86_64-pc-windows-msvc"
   else
-    let mut arch ← (·.trim) <$> runCmd "uname" #["-m"] false
+    let mut arch ← (·.trimAscii.copy) <$> runCmd "uname" #["-m"] false
     if arch = "arm64" then arch := "aarch64"
     unless arch ∈ ["x86_64", "aarch64"] do
       throw <| IO.userError s!"unsupported architecture {arch}"

Cache/Requests.lean

@@ -28,10 +28,10 @@ structure RepoInfo where
 Helper function to extract repository name from a git remote URL
 -/
 def extractRepoFromUrl (url : String) : Option String := do
-  let url := url.stripSuffix ".git"
-  let pos ← url.revFind (· == '/')
-  let pos ← url.revFindAux (fun c => c == '/'  || c == ':') pos
-  return (String.Pos.Raw.extract url) (String.Pos.Raw.next url pos) url.rawEndPos
+  let url := url.dropSuffix ".git"
+  let pos ← url.revFind? (· == '/')
+  let pos ← (url.sliceTo pos).revFind? (fun c => c == '/' || c == ':')
+  return url.sliceFrom (String.Slice.Pos.ofSliceTo pos).next! |>.copy
 
 /-- Spot check if a URL is valid for a git remote -/
 def isRemoteURL (url : String) : Bool :=
@@ -50,14 +50,14 @@ def getRepoFromRemote (mathlibDepPath : FilePath) (remoteName : String) (errorCo
   let out ← IO.Process.output
     {cmd := "git", args := #["remote", "get-url", remoteName], cwd := mathlibDepPath}
   -- If `git remote get-url` fails then bail out with an error to help debug
-  let output := out.stdout.trim
+  let output := out.stdout.trimAscii
   unless out.exitCode == 0 do
     throw <| IO.userError s!"\
       Failed to run Git to determine Mathlib's repository from {remoteName} remote (exit code: {out.exitCode}).\n\
       {errorContext}\n\
-      Stdout:\n{output}\nStderr:\n{out.stderr.trim}\n"
+      Stdout:\n{output}\nStderr:\n{out.stderr.trimAscii}\n"
   -- Finally attempt to extract the repository from the remote URL returned by `git remote get-url`
-  repoFromURL output
+  repoFromURL output.copy
 where repoFromURL (url : String) : IO String := do
     if let some repo := extractRepoFromUrl url then
       return repo
@@ -79,17 +79,17 @@ def findMathlibRemote (mathlibDepPath : FilePath) : IO String := do
     throw <| IO.userError s!"\
       Failed to run Git to list remotes (exit code: {remotesInfo.exitCode}).\n\
       Ensure Git is installed.\n\
-      Stdout:\n{remotesInfo.stdout.trim}\nStderr:\n{remotesInfo.stderr.trim}\n"
+      Stdout:\n{remotesInfo.stdout.trimAscii}\nStderr:\n{remotesInfo.stderr.trimAscii}\n"
 
   let remoteLines := remotesInfo.stdout.splitToList (· == '\n')
   let mut mathlibRemote : Option String := none
   let mut originPointsToMathlib : Bool := false
 
   for line in remoteLines do
-    let parts := line.trim.splitToList (· == '\t')
+    let parts := line.trimAscii.copy.splitToList (· == '\t')
     if parts.length >= 2 then
       let remoteName := parts[0]!
-      let remoteUrl := parts[1]!.takeWhile (· != ' ') -- Remove (fetch) or (push) suffix
+      let remoteUrl := parts[1]!.takeWhile (· != ' ') |>.copy -- Remove (fetch) or (push) suffix
 
       -- Check if this remote points to leanprover-community/mathlib4
       let isMathlibRepo := remoteUrl.containsSubstr "leanprover-community/mathlib4"
@@ -128,11 +128,11 @@ def isDetachedAtNightlyTesting (mathlibDepPath : FilePath) : IO Bool := do
   let currentCommit ← IO.Process.output
     {cmd := "git", args := #["rev-parse", "HEAD"], cwd := mathlibDepPath}
   if currentCommit.exitCode == 0 then
-    let commitHash := currentCommit.stdout.trim
+    let commitHash := currentCommit.stdout.trimAscii.copy
     let tagInfo ← IO.Process.output
       {cmd := "git", args := #["name-rev", "--tags", commitHash], cwd := mathlibDepPath}
     if tagInfo.exitCode == 0 then
-      let parts := tagInfo.stdout.trim.splitOn " "
+      let parts := tagInfo.stdout.trimAscii.copy.splitOn " "
       -- git name-rev returns "commit_hash tags/tag_name" or just "commit_hash undefined" if no tag
       if parts.length >= 2 && parts[1]!.startsWith "tags/" then
         let tagName := parts[1]!.drop 5  -- Remove "tags/" prefix
@@ -159,17 +159,17 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
     {cmd := "git", args := #["rev-parse", "--abbrev-ref", "HEAD"], cwd := mathlibDepPath}
 
   if currentBranch.exitCode == 0 then
-    let branchName := currentBranch.stdout.trim.stripPrefix "heads/"
+    let branchName := currentBranch.stdout.trimAscii.dropPrefix "heads/"
     IO.println s!"Current branch: {branchName}"
 
     -- Check if we're in a detached HEAD state at a nightly-testing tag
-    let isDetachedAtNightlyTesting ← if branchName == "HEAD" then
+    let isDetachedAtNightlyTesting ← if branchName == "HEAD".toSlice then
       isDetachedAtNightlyTesting mathlibDepPath
     else
       pure false
 
     -- Check if we're on a branch that should use nightly-testing remote
-    let shouldUseNightlyTesting := branchName == "nightly-testing" ||
+    let shouldUseNightlyTesting := branchName == "nightly-testing".toSlice ||
                                   branchName.startsWith "lean-pr-testing-" ||
                                   branchName.startsWith "batteries-pr-testing-" ||
                                   branchName.startsWith "bump/" ||
@@ -229,10 +229,10 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
 
   -- Fall back to using the remote that the current branch is tracking
   let trackingRemote ← IO.Process.output
-    {cmd := "git", args := #["config", "--get", s!"branch.{currentBranch.stdout.trim}.remote"], cwd := mathlibDepPath}
+    {cmd := "git", args := #["config", "--get", s!"branch.{currentBranch.stdout.trimAscii}.remote"], cwd := mathlibDepPath}
 
   let remoteName := if trackingRemote.exitCode == 0 then
-    trackingRemote.stdout.trim
+    trackingRemote.stdout.trimAscii.copy
   else
     -- If no tracking remote is configured, fall back to origin
     "origin"
@@ -329,15 +329,15 @@ def monitorCurl (args : Array String) (size : Nat)
   let s@{success, failed, done, speed, ..} ← IO.runCurlStreaming args init fun a line => do
     let mut {last, success, failed, done, speed} := a
     -- output errors other than 404 and remove corresponding partial downloads
-    let line := line.trim
+    let line := line.trimAscii
     if !line.isEmpty then
-      match Lean.Json.parse line with
+      match Lean.Json.parse line.copy with
       | .ok result =>
         match result.getObjValAs? Nat "http_code" with
         | .ok 200 =>
           if let .ok fn := result.getObjValAs? String "filename_effective" then
             if (← System.FilePath.pathExists fn) && fn.endsWith ".part" then
-              IO.FS.rename fn (fn.dropRight 5)
+              IO.FS.rename fn (fn.dropEnd 5).copy
           success := success + 1
         | .ok 404 => pure ()
         | code? =>
@@ -415,10 +415,10 @@ def checkForToolchainMismatch : IO.CacheM Unit := do
   let mathlibToolchainFile := (← read).mathlibDepPath / "lean-toolchain"
   let downstreamToolchain ← IO.FS.readFile "lean-toolchain"
   let mathlibToolchain ← IO.FS.readFile mathlibToolchainFile
-  if !(mathlibToolchain.trim = downstreamToolchain.trim) then
+  if !(mathlibToolchain.trimAscii == downstreamToolchain.trimAscii) then
     IO.println "Dependency Mathlib uses a different lean-toolchain"
-    IO.println s!"  Project uses {downstreamToolchain.trim}"
-    IO.println s!"  Mathlib uses {mathlibToolchain.trim}"
+    IO.println s!"  Project uses {downstreamToolchain.trimAscii}"
+    IO.println s!"  Mathlib uses {mathlibToolchain.trimAscii}"
     IO.println "\nThe cache will not work unless your project's toolchain matches Mathlib's toolchain"
     IO.println s!"This can be achieved by copying the contents of the file `{mathlibToolchainFile}`
 into the `lean-toolchain` file at the root directory of your project"
@@ -554,7 +554,8 @@ section Commit
 def isGitStatusClean : IO Bool :=
   return (← IO.runCmd "git" #["status", "--porcelain"]).isEmpty
 
-def getGitCommitHash : IO String := return (← IO.runCmd "git" #["rev-parse", "HEAD"]).trimRight
+def getGitCommitHash : IO String :=
+  return (← IO.runCmd "git" #["rev-parse", "HEAD"]).trimAsciiEnd.copy
 
 /--
 Sends a commit file to the server, containing the hashes of the respective committed files.

Mathlib/Algebra/GroupWithZero/Torsion.lean

@@ -27,7 +27,7 @@ theorem IsMulTorsionFree.mk' (ih : ∀ x ≠ 0, ∀ y ≠ 0, ∀ n ≠ 0, (x ^ n
   refine ⟨fun n hn x y hxy ↦ ?_⟩
   by_cases h : x ≠ 0 ∧ y ≠ 0
   · exact ih x h.1 y h.2 n hn hxy
-  grind [pow_eq_zero, zero_pow]
+  grind [eq_zero_of_pow_eq_zero, zero_pow]
 
 variable [UniqueFactorizationMonoid M] [NormalizationMonoid M] [IsMulTorsionFree Mˣ]
 

Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

@@ -431,7 +431,7 @@ noncomputable def extFunctor (n : ℕ) : Cᵒᵖ ⥤ C ⥤ AddCommGrpCat.{w} whe
         dsimp
         symm
         apply Ext.comp_assoc
-        all_goals omega }
+        all_goals lia }
   map_comp {X₁ X₂ X₃} f f' := by
     ext Y α
     simp

Mathlib/Algebra/Homology/ExactSequence.lean

@@ -106,7 +106,7 @@ lemma isComplex₀ (S : ComposableArrows C 0) : S.IsComplex where
   zero i hi := by simp at hi
 
 lemma isComplex₁ (S : ComposableArrows C 1) : S.IsComplex where
-  zero i hi := by omega
+  zero i hi := by lia
 
 variable (S)
 
@@ -193,7 +193,7 @@ lemma exact₀ (S : ComposableArrows C 0) : S.Exact where
 
 lemma exact₁ (S : ComposableArrows C 1) : S.Exact where
   toIsComplex := S.isComplex₁
-  exact i hi := by exfalso; omega
+  exact i hi := by exfalso; lia
 
 lemma isComplex₂_iff (S : ComposableArrows C 2) :
     S.IsComplex ↔ S.map' 0 1 ≫ S.map' 1 2 = 0 := by

Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

@@ -547,7 +547,7 @@ lemma liftCochain_descCochain :
 lemma liftCochain_v_descCochain_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + n' = p₃)
     (q : ℤ) (hq : p₁ + m = q) :
     (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (descCochain φ α' β' h').v p₂ p₃ h₂₃ =
-      α.v p₁ q hq ≫ α'.v q p₃ (by lia) + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃ := by
+      α.v p₁ q hq ≫ α'.v q p₃ (by omega) + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃ := by
   have eq := Cochain.congr_v (liftCochain_descCochain φ α β α' β' h h' p hp) p₁ p₃ (by lia)
   simpa only [Cochain.comp_v _ _ hp p₁ p₂ p₃ h₁₂ h₂₃, Cochain.add_v,
     Cochain.comp_v _ _ _ _ _ _ hq (show q + m' = p₃ by lia)] using eq

Mathlib/Algebra/Module/ZLattice/Summable.lean

@@ -124,9 +124,9 @@ lemma sum_piFinset_Icc_rpow_le {ι : Type*} [Fintype ι] [DecidableEq ι]
       norm_num at this
       zify
       convert this using 3
-      · rw [abs_eq_self.mpr (sub_nonneg.mpr (by gcongr; omega)), Nat.cast_sub (by gcongr; omega)]
+      · rw [abs_eq_self.mpr (sub_nonneg.mpr (by gcongr; lia)), Nat.cast_sub (by gcongr; lia)]
         simp
-      · rw [max_eq_left (by gcongr; omega), abs_eq_self.mpr (by positivity)]
+      · rw [max_eq_left (by gcongr; lia), abs_eq_self.mpr (by positivity)]
   let ε := normBound b
   have hε : 0 < ε := normBound_pos b
   calc ∑ p ∈ s n, ‖∑ i, p i • b i‖ ^ r
@@ -147,7 +147,7 @@ lemma sum_piFinset_Icc_rpow_le {ι : Type*} [Fintype ι] [DecidableEq ι]
         gcongr with k hk
         refine (this _).trans ?_
         gcongr
-        omega
+        lia
     _ = 2 * d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, (k + 1) ^ (d - 1) * (k + 1 : ℝ) ^ r := by
         simp_rw [Finset.mul_sum]
         congr with k

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -225,7 +225,10 @@ end Fewnomials
 theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
     coeff (p * Polynomial.X ^ n) (d + n) = coeff p d := by
   rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-  all_goals grind [mem_antidiagonal, mul_zero]
+  · rintro ⟨i, j⟩ h1 h2
+    rw [coeff_X_pow, if_neg, mul_zero]
+    grind [mem_antidiagonal]
+  · grind [mem_antidiagonal]
 
 @[simp]
 theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) :

Mathlib/Algebra/Polynomial/RuleOfSigns.lean

@@ -313,7 +313,7 @@ theorem succ_signVariations_le_X_sub_C_mul (hη : 0 < η) (hP : P ≠ 0) :
   · --P is zero degree, therefore a constant.
     have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
     have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
-      grind [coeff_X_sub_C_mul, mul_zero, coeff_eq_zero_of_natDegree_lt]
+      simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]
     dsimp [signVariations, coeffList]
     rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]
     simp [h_deg_mul, hxcQ, hη, hcQ, hd, List.range_succ]