chore: bump toolchain to v4.30.0-rc1 (#37564)

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Robin Arnez <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Joscha <joscha@plugh.de>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>

Author: 5 people

Archive/Imo/Imo2024Q5.lean

@@ -778,9 +778,9 @@ lemma path1_firstMonster_of_not_edge (hN : 2 ≤ N) {m : MonsterData N} (hc₁0
     (hc₁N : (m (row1 hN) : ℕ) ≠ N) :
     (path1 hN (m (row1 hN))).firstMonster m = none ∨
       (path1 hN (m (row1 hN))).firstMonster m =
-        some (⟨2, by lia⟩, ⟨(m (row1 hN) : ℕ) - 1, by lia⟩) := by
+        some (⟨2, by lia⟩, ⟨(m (row1 hN) : ℕ) - 1, by omega⟩) := by
   suffices h : ∀ c ∈ (path1 hN (m (row1 hN))).cells, c ∉ m.monsterCells ∨
-      c = (⟨2, by lia⟩, ⟨(m (row1 hN) : ℕ) - 1, by lia⟩) by
+      c = (⟨2, by lia⟩, ⟨(m (row1 hN) : ℕ) - 1, by omega⟩) by
     simp only [Path.firstMonster]
     by_cases hn : List.find? (fun x ↦ decide (x ∈ m.monsterCells))
                              (path1 hN (m (row1 hN))).cells = none

Cache/IO.lean

@@ -79,24 +79,24 @@ def CURLBIN :=
   -- change file name if we ever need a more recent version to trigger re-download
   IO.CACHEDIR / s!"curl-{CURLVERSION}"
 
-/-- leantar version at https://github.com/digama0/leangz -/
-def LEANTARVERSION :=
-  "0.1.17"
-
 def EXE := if System.Platform.isWindows then ".exe" else ""
 
-def LEANTARBIN :=
-  -- change file name if we ever need a more recent version to trigger re-download
-  IO.CACHEDIR / s!"leantar-{LEANTARVERSION}{EXE}"
-
 def LAKEPACKAGESDIR : FilePath :=
   ".lake" / "packages"
 
 def getCurl : IO String := do
   return if (← CURLBIN.pathExists) then CURLBIN.toString else "curl"
 
-def getLeanTar : IO String := do
-  return if (← LEANTARBIN.pathExists) then LEANTARBIN.toString else "leantar"
+/-- Path to the `leantar` binary bundled with the Lean toolchain.
+    This has been bundled since `nightly-2026-03-09` (lean4#12822). -/
+private initialize leantarSysrootBin : String ← do
+  let out ← IO.Process.output { cmd := "lean", args := #["--print-prefix"] }
+  if out.exitCode == 0 then
+    let path : FilePath := out.stdout.trimAscii.toString / "bin" / s!"leantar{EXE}"
+    if ← path.pathExists then return path.toString
+  throw <| IO.userError "leantar not found in Lean sysroot. This toolchain may predate nightly-2026-03-09."
+
+def getLeanTar : IO String := return leantarSysrootBin
 
 /-- Spawn a `leantar` process for decompression, writing the given JSON config to its stdin.
     Returns the process exit code. -/
@@ -208,7 +208,9 @@ def validateCurl : IO Bool := do
   match (← runCmd "curl" #["--version"]).splitOn " " with
   | "curl" :: v :: _ => match v.splitOn "." with
     | maj :: min :: _ =>
-      let version := (maj.toNat!, min.toNat!)
+      let some majN := String.toNat? maj | throw <| IO.userError "Invalidly formatted version of `curl`"
+      let some minN := String.toNat? min | throw <| IO.userError "Invalidly formatted version of `curl`"
+      let version := (majN, minN)
       let _ := @lexOrd
       let _ := @leOfOrd
       if version >= (7, 81) then return true
@@ -232,45 +234,6 @@ def validateCurl : IO Bool := do
     | _ => throw <| IO.userError "Invalidly formatted version of `curl`"
   | _ => throw <| IO.userError "Invalidly formatted response from `curl --version`"
 
-def Version := Nat × Nat × Nat
-  deriving Inhabited, DecidableEq
-
-instance : Ord Version := let _ := @lexOrd; lexOrd
-instance : LE Version := leOfOrd
-
-def parseVersion (s : String) : Option Version := do
-  let [maj, min, patch] := s.splitOn "." | none
-  some (maj.toNat!, min.toNat!, patch.toNat!)
-
-def validateLeanTar : IO Unit := do
-  if (← LEANTARBIN.pathExists) then return
-  if let some version ← some <$> runCmd "leantar" #["--version"] <|> pure none then
-    let "leantar" :: v :: _ := version.splitOn " "
-      | throw <| IO.userError "Invalidly formatted response from `leantar --version`"
-    let some v := parseVersion v | throw <| IO.userError "Invalidly formatted version of `leantar`"
-    -- currently we need exactly one version of leantar, change this to reflect compatibility
-    if v = (parseVersion LEANTARVERSION).get! then return
-  let win := System.Platform.getIsWindows ()
-  let target ← if win then
-    pure "x86_64-pc-windows-msvc"
-  else
-    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}"
-    pure <|
-      if System.Platform.getIsOSX () then s!"{arch}-apple-darwin"
-      else s!"{arch}-unknown-linux-musl"
-  IO.println s!"installing leantar {LEANTARVERSION}"
-  IO.FS.createDirAll IO.CACHEDIR
-  let ext := if win then "zip" else "tar.gz"
-  let _ ← runCmd "curl" (stderrAsErr := false) #[
-    s!"https://github.com/digama0/leangz/releases/download/v{LEANTARVERSION}/leantar-v{LEANTARVERSION}-{target}.{ext}",
-    "-L", "-o", s!"{LEANTARBIN}.{ext}"]
-  let _ ← runCmd "tar" #["-xf", s!"{LEANTARBIN}.{ext}",
-    "-C", IO.CACHEDIR.toString, "--strip-components=1"]
-  IO.FS.rename (IO.CACHEDIR / s!"leantar{EXE}").toString LEANTARBIN.toString
-
 /-- Recursively gets all files from a directory with a certain extension -/
 partial def getFilesWithExtension
   (fp : FilePath) (extension : String) (acc : Array FilePath := #[]) :

Cache/Main.lean

@@ -113,7 +113,6 @@ def main (args : List String) : IO Unit := do
   let hashMemo ← getHashMemo roots
   let hashMap := hashMemo.hashMap
   let goodCurl ← pure !curlArgs.contains (args.headD "") <||> validateCurl
-  if leanTarArgs.contains (args.headD "") then validateLeanTar
   let get (args : List String) (force := false) (decompress := true) := do
     let hashMap ← if args.isEmpty then pure hashMap else hashMemo.filterByRootModules roots.keys
     getFiles repo? hashMap force force goodCurl decompress

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -824,7 +824,6 @@ theorem mem_adjoin_iff {s : Set A} {x : A} :
 
 variable (R)
 
-set_option backward.isDefEq.respectTransparency false in
 open scoped IsMulCommutative in
 /-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a commutative
 ring. -/

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

@@ -258,7 +258,7 @@ lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
   | [], ys => by simp
   | xs, [] => by simp
   | x :: xs, y :: ys => by
-    simp only [drop, length, zipWith_cons_cons, prod_cons]
+    simp only [drop, zipWith_cons_cons, prod_cons]
     conv =>
       lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
       rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -366,7 +366,7 @@ theorem map'_comp {M₁ M₂ M₃ : ModuleCat.{v} R} (l₁₂ : M₁ ⟶ M₂) (
   induction x using TensorProduct.induction_on with
   | zero => rfl
   | tmul => rfl
-  | add _ _ ihx ihy => grind
+  | add _ _ ihx ihy => erw [LinearMap.map_add, LinearMap.map_add]; grind
 
 end ExtendScalars
 

Mathlib/Algebra/FiniteSupport/Basic.lean

@@ -167,7 +167,7 @@ variable {β : Type*} {f : β → M} {g : α → β}
 lemma HasFiniteMulSupport.comp_of_injective (hg : Injective g) (hf : f.HasFiniteMulSupport) :
     (f ∘ g).HasFiniteMulSupport := by
   refine Set.Finite.of_injOn ?_ (Set.injOn_of_injective hg) hf
-  grind [Set.mapsTo_iff_subset_preimage]
+  grind [Set.mapsTo_iff_subset_preimage, Function.mulSupport]
 
 @[to_additive (attr := fun_prop)]
 lemma HasFiniteMulSupport.fun_comp_of_injective (hg : Injective g) (hf : f.HasFiniteMulSupport) :

Mathlib/Algebra/Group/Ext.lean

@@ -109,7 +109,11 @@ theorem CancelMonoid.toRightCancelMonoid_injective {M : Type u} :
 theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} :
     Function.Injective (@CancelCommMonoid.toCommMonoid M) := by
   rintro @⟨@⟨@⟨⟩⟩⟩ @⟨@⟨@⟨⟩⟩⟩ h
-  grind
+  #adaptation_note /-- Before leanprover/lean4#13166, the last line was `grind`.
+  The new type-directed canonicalizer tries to synthesize `Monoid M` / `CommMonoid M` to normalize
+  sub-expressions, but fails because after `rintro` the instances exist only as destructured fields
+  in the local context, not as registered typeclass instances. -/
+  cases h; rfl
 
 @[to_additive (attr := ext)]
 theorem CancelCommMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelCommMonoid M⦄

Mathlib/Algebra/Homology/HomotopyCategory/MappingCocone.lean

@@ -153,7 +153,11 @@ lemma δ_descCochain (n' : ℤ) (hn' : n + 1 = n') :
     Cochain.comp_v (n₁ := 1) _ _ _ (p + -1) p _ (by lia) hpq,
     Cochain.comp_v (n₂ := m + 2) _ _ _ p (p + -1) q rfl (by lia),
     smul_smul, Int.negOnePow_add, Int.negOnePow_even 2 ⟨1, rfl⟩]
-  grind
+  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
+  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
+  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
+  canonicalizer; a minimization would help. The original proof was: `grind` -/
+  abel
 
 end
 
@@ -245,7 +249,11 @@ lemma δ_liftCochain (n' : ℤ) (hn' : n + 1 = n') :
     Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (q + -1)),
     Cochain.comp_v _ _ _ p q _ hpq rfl,
     Cochain.comp_v (n₁ := n) (n₂ := 1) _ _ _ p (q + -1) q (by lia) (by lia)]
-  grind
+  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
+  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
+  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
+  canonicalizer; a minimization would help. The original proof was: `grind` -/
+  abel
 
 end
 

Mathlib/Algebra/Lie/CartanExists.lean

@@ -282,7 +282,7 @@ lemma engel_isBot_of_isMin (hLK : finrank K L ≤ #K) (U : LieSubalgebra K L)
     use s \ t
     refine ⟨?_, ?_⟩
     · refine le_trans ?_ (Finset.le_card_sdiff _ _)
-      lia
+      omega
     · intro α hα
       simp only [Finset.mem_sdiff, Multiset.mem_toFinset, mem_roots', IsRoot.def, not_and, t] at hα
       exact hα.2 hψ
@@ -293,7 +293,7 @@ lemma engel_isBot_of_isMin (hLK : finrank K L ≤ #K) (U : LieSubalgebra K L)
     -- Which follows from our assumptions `i < r` and `r ≤ s.card`
     -- and the fact that the degree of `coeff χ i` is less than or equal to `r - i`.
     apply lt_of_le_of_lt (lieCharpoly_coeff_natDegree _ _ _ _ i (r - i) _)
-    · lia
+    · omega
     · dsimp only [r] at hi ⊢
       rw [Nat.add_sub_cancel' hi.le]
   -- We need to show that for all `α ∈ s`, the polynomial `coeff χ i` evaluates to zero at `α`.