chore: bump toolchain to v4.29.0-rc6 (leanprover#412)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -29,6 +29,7 @@ following two conditions hold:
 (1) `u` can move `na` from `s` to `t` iff `v` can move `na` from `s` to `t`;
 (2) `u` can move `na` from `s` to `t` via an acceptingg states iff `v` can move `na`
 from `s` to `t` via an acceptingg states. -/
+@[implicit_reducible]
 def BuchiCongruence (na : Buchi State Symbol) : RightCongruence Symbol where
   eq.r u v :=
     ∀ {s t}, (u ∈ na.pairLang s t ↔ v ∈ na.pairLang s t) ∧

Cslib/Foundations/Data/BiTape.lean

@@ -7,7 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Foundations.Data.StackTape
-public import Mathlib.Computability.Tape
+public import Mathlib.Computability.TuringMachine.Tape
 public import Mathlib.Data.Finset.Attr
 public import Mathlib.Tactic.SetLike
 public import Mathlib.Algebra.Order.Group.Nat

Cslib/Foundations/Data/HasFresh.lean

@@ -146,12 +146,14 @@ noncomputable instance HasFresh.of_infinite (α : Type u) [Infinite α] : HasFre
 
 open Finset in
 /-- Construct a fresh element from an embedding of `ℕ` using `Nat.find`. -/
+@[implicit_reducible]
 def HasFresh.ofNatEmbed {α : Type u} [DecidableEq α] (e : ℕ ↪ α) : HasFresh α where
   fresh s := e (Nat.find (p := fun n ↦ e n ∉ s) ⟨(s.preimage e e.2.injOn).max.succ,
     fun h ↦ not_lt_of_ge (le_max <| mem_preimage.2 h) (WithBot.lt_succ _)⟩)
   fresh_notMem s := Nat.find_spec (p := fun n ↦ e n ∉ s) _
 
 /-- Construct a fresh element given a function `f` with `x < f x`. -/
+@[implicit_reducible]
 def HasFresh.ofSucc {α : Type u} [Inhabited α] [SemilatticeSup α] (f : α → α) (hf : ∀ x, x < f x) :
     HasFresh α where
   fresh s := if hs : s.Nonempty then f (s.sup' hs id) else default

Cslib/Foundations/Data/Relation.lean

@@ -176,16 +176,19 @@ theorem ChurchRosser.normal_eq (cr : ChurchRosser r) (nx : Normal r x) (ny : Nor
   grind
 
 /-- A pair of subrelations lifts to transitivity on the relation. -/
+@[implicit_reducible]
 def trans_of_subrelation (s s' r : α → α → Prop) (hr : Transitive r)
     (h : Subrelation s r) (h' : Subrelation s' r) : Trans s s' r where
   trans hab hbc := hr (h hab) (h' hbc)
 
 /-- A subrelation lifts to transitivity on the left of the relation. -/
+@[implicit_reducible]
 def trans_of_subrelation_left (s r : α → α → Prop) (hr : Transitive r)
     (h : Subrelation s r) : Trans s r r where
   trans hab hbc := hr (h hab) hbc
 
 /-- A subrelation lifts to transitivity on the right of the relation. -/
+@[implicit_reducible]
 def trans_of_subrelation_right (s r : α → α → Prop) (hr : Transitive r)
     (h : Subrelation s r) : Trans r s r where
   trans hab hbc := hr hab (h hbc)

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "891dd961017425184bf9499bdcf6c88a68076667",
+   "rev": "5c8398df528176d9c87ccd9226ba8f7c8852d59c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8629a535d10cd7edfbf1a2c5cdfbaeee135a62cd",
+   "rev": "e84e3e16aea6b72cc5d311ca1bb25caad417e162",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f7f57d837a219a8e298798faba94bc7082111a7d",
+   "rev": "f207d9fcf0cef00ba79962a33ef156061914d9c7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5a4234b81b903726764307df9cb23ec3cc3e5758",
+   "rev": "2e58165a9dcdca9837b666528f974299ee1a51cc",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.91",
+   "inputRev": "v0.0.92",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d5ec850924e710ea67881e3ca9d1e920c929dbe",
+   "rev": "c3361708f266893de5d1769192b60d4b1831f2bb",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bc486babc10837d7f43351f12b53879581924163",
+   "rev": "221e8088e3a066b8676dc471ff10638cf1c10835",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ac3fb7297326c5429ce2844712fb54ba9dd20198",
+   "rev": "bd58e3506632241b59e406902d5e42b73cdeccce",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "06c8b4d690d9b7ef98d594672bbdaa618156215a",
+   "rev": "3de531c1135f5e3a01f3ac04830996fda476b28e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-rc4",
+   "inputRev": "v4.29.0-rc6",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "cslib",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc4
+leanprover/lean4:v4.29.0-rc6