From a5ff8efe5b5e314e0aa759318e5fb194e066f612 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Tue, 14 Apr 2026 16:04:44 +0200
Subject: update lean

---
 Algebra/Derivations.lean             | 10 +++++-----
 Graded/GradedMonad.lean              | 20 ++++++++++++++------
 Nominal/Equivariance.lean            |  9 ++++++---
 Nominal/Helpers/CountableString.lean |  6 +++---
 Nominal/Instances/Abstraction.lean   | 12 ++++--------
 Nominal/Instances/Basic.lean         | 10 ++++++----
 Nominal/LambdaCalculus/Terms.lean    | 22 +++++++++-------------
 Nominal/Permutations.lean            |  6 +++---
 Nominal/Support.lean                 |  2 +-
 flake.lock                           |  6 +++---
 lake-manifest.json                   | 26 +++++++++++++-------------
 lakefile.toml                        |  4 ++--
 lean-toolchain                       |  2 +-
 13 files changed, 70 insertions(+), 65 deletions(-)

diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean
index 717ffe1..b6e5cb5 100644
--- a/Algebra/Derivations.lean
+++ b/Algebra/Derivations.lean
@@ -118,11 +118,11 @@ lemma Derivable.of_eq
     Derivable T eq := by
   intro hderiv
   have heq : (eq.val.vars ⊢ t ≣ u) = eq := by
-    apply Subtype.eq; ext
+    apply Subtype.ext; ext
     · rfl
     · rfl
-    · rw [heq_eq_eq]; exact ht
-    · rw [heq_eq_eq]; exact hu
+    · exact heq_of_eq ht
+    · exact heq_of_eq hu
   rw [← heq]; exact hderiv
 
 lemma Derivable.equivariant_substitution
@@ -180,7 +180,7 @@ lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} :
   · rw [rename_eq]
     apply Derivable.trans (by apply Derivable.symm; apply equivariant_substitution; exact h_1) _
     apply Derivable.trans _ (by apply equivariant_substitution; exact h_1)
-    rw [← MulAction.mul_smul, ← MulAction.mul_smul]
+    rw [← SemigroupAction.mul_smul, ← SemigroupAction.mul_smul]
     apply Derivable.ax
     · exact h
     · exact h_1
@@ -195,7 +195,7 @@ lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} :
       exact h_1 x
     · intro x
       show Derivable T (X_1 ⊢ π • ts x ≣ ⸨π a, π b⸩ • π • us x)
-      rw [← MulAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, MulAction.mul_smul]
+      rw [← SemigroupAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, SemigroupAction.mul_smul]
       exact a_ih x
 
 instance DerivableEq.instEquivariant : Rel.Equivariant 𝔸 (DerivableEq T X n) := by
diff --git a/Graded/GradedMonad.lean b/Graded/GradedMonad.lean
index d0af5f4..39d543c 100644
--- a/Graded/GradedMonad.lean
+++ b/Graded/GradedMonad.lean
@@ -54,17 +54,23 @@ def ofMonad (M : Monad C) : GradedMonad C where
   toFunctor _ := M.toFunctor
   η := M.η
   μ _ _ := M.μ
-  assoc X _ _ _ := by simp [M.assoc X]
-  left_unit X _ := by simp [M.left_unit]
-  right_unit X _ := by simp [M.right_unit]
+  assoc X _ _ _ := by simp only [Functor.comp_obj, eqToHom_refl, Category.comp_id]; exact M.assoc X
+  left_unit X _ := by simp only [eqToHom_refl, Category.comp_id]; exact M.left_unit X
+  right_unit X _ := by exact M.right_unit X
 
 def toMonad (M : GradedMonad C) : Monad C :=
   { M 0 with
     η := M.η
     μ := M.μ 0 0
-    assoc X := by simp [M.assoc X 0 0 0]
-    left_unit X := by simp [M.left_unit X 0]
-    right_unit X := by simp [M.right_unit X 0] }
+    assoc X := by
+      have h := M.assoc X 0 0 0
+      simp only [Functor.comp_obj, Nat.add_zero, eqToHom_refl, Category.comp_id] at h
+      exact h
+    left_unit X := by
+      have h := M.left_unit X 0
+      simp only [Functor.id_obj, Nat.add_zero, eqToHom_refl, Category.comp_id] at h
+      exact h
+    right_unit X := M.right_unit X 0 }
 
 lemma toMonad_ofMonad {M : Monad C} : (ofMonad M).toMonad = M := rfl
 
@@ -83,6 +89,8 @@ def ofComp (F : C ⥤ C) : GradedMonad C where
   η := NatTrans.id (𝟭 C)
   μ n k := NatTrans.id (compFunctor F k ⋙ compFunctor F n) ≫ eqToHom (compFunctor_comp _ n k)
   assoc X n k m := by simp [eqToHom_map]
+  left_unit X n := by simp [compFunctor]
+  right_unit X n := by simp [compFunctor]
 
 end GradedMonad
 
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 2682a55..e9bd850 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -25,7 +25,7 @@ class inductive Function.Equivariant (f : X → Y) : Prop
 
 lemma Function.equivariant (f : X → Y) [Equivariant 𝔸 f] :
     ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x := by
-  cases (inferInstanceAs (Equivariant 𝔸 f)); assumption
+  cases (inferInstance : Equivariant 𝔸 f); assumption
 
 /-- A set is equivariant if it is closed under permutations. -/
 class inductive Set.Equivariant (S : Set X) : Prop
@@ -34,7 +34,7 @@ class inductive Set.Equivariant (S : Set X) : Prop
 /-- For equivariant sets, we even have "if and only if". -/
 lemma Set.equivariant (S : Set X) [Equivariant 𝔸 S] :
     ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by
-  cases (inferInstanceAs (Equivariant 𝔸 S)); rename_i h
+  cases (inferInstance : Equivariant 𝔸 S); rename_i h
   intro x π; constructor
   · intro hx; exact h x π hx
   · intro hx
@@ -49,7 +49,7 @@ class inductive Rel.Equivariant (R : Rel X Y) : Prop
 /-- For equivariant relations, we even have "if and only if". -/
 lemma Rel.equivariant (R : Rel X Y) [Rel.Equivariant 𝔸 R] :
     ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y ↔ R (π • x) (π • y) := by
-  cases (inferInstanceAs (Equivariant 𝔸 R)); rename_i h
+  cases (inferInstance : Equivariant 𝔸 R); rename_i h
   intro x y π; constructor
   · intro hxy; exact h x y π hxy
   · intro hxy
@@ -83,6 +83,7 @@ instance Function.Equivariant.comp
     _             = π • (f (g x)) := by rw [← Function.equivariant 𝔸 f]
 
 /-- If a function is equivariant, its inverse is also equivariant. -/
+@[reducible]
 def Function.Equivariant.inv
     {f : X → Y} [Function.Equivariant 𝔸 f] {inv : Y → X}
     (hleft : Function.LeftInverse inv f)
@@ -191,6 +192,7 @@ lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] :
 end Function.Equivariant
 
 /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/
+@[reducible]
 def NominalSet.ofEquivariantSurjective
     {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y]
     (f : X → Y) [Function.Equivariant 𝔸 f] (hsurj : Function.Surjective f) :
@@ -385,6 +387,7 @@ instance EquivariantEquiv.invFunEquivariant
   equiv.invFun_equivariant
 
 /-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/
+@[reducible]
 def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X :=
   NominalSet.ofEquivariantSurjective 𝔸 equiv.invFun equiv.symm.surjective
 
diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
index b6f59f8..c887f96 100644
--- a/Nominal/Helpers/CountableString.lean
+++ b/Nominal/Helpers/CountableString.lean
@@ -5,10 +5,10 @@ instance : Countable Char where
     use Char.toNat
     intro c₁ c₂ hc
     rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
-    exact Char.eq_of_val_eq hc
+    exact Char.ext hc
 
 instance : Countable String := Countable.of_equiv (List Char)
-  { toFun := String.mk
-    invFun := String.data
+  { toFun := String.ofList
+    invFun := String.toList
     left_inv x := by simp
     right_inv x := by simp }
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index e03d67a..f1a711b 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -225,16 +225,12 @@ instance NameAbstraction.setoid_equivariant : Rel.Equivariant 𝔸 (setoid 𝔸
   instAlphaEqEquivariant
 
 /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
-def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
+abbrev NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
 
 namespace NameAbstraction
 
-/-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/
-abbrev mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
-  Quotient.mk (setoid 𝔸 X) (.mk a x)
-
 /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/
-notation "⟪" a "⟫ " x:60 => mk a x
+notation "⟪" a "⟫ " x:60 => (⟦⟨a, x⟩⟧ : NameAbstraction _ _)
 
 instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸
 
@@ -390,13 +386,13 @@ private lemma map_id : map 𝔸 (EquivariantMap.id 𝔸 : X →ₑ[𝔸] X) = Eq
   suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.id 𝔸) x = x by ext x; exact this x
   apply Quotient.ind
   intro x
-  simp [map', NameAbstraction.mk]
+  simp [map']
 
 private lemma map_comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : map 𝔸 (EquivariantMap.comp 𝔸 f g) = EquivariantMap.comp 𝔸 (map 𝔸 f) (map 𝔸 g) := by
   suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.comp 𝔸 f g) x = (map' 𝔸 f) ((map' 𝔸 g) x) by ext x; exact this x
   apply Quotient.ind
   intro x
-  simp [map', NameAbstraction.mk]
+  simp [map']
 
 /-- Name abstractions form a functor `Nom ⥤ Nom`. -/
 def Functor : Nom 𝔸 ⥤ Nom 𝔸 :=
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index b627c1b..7a88eeb 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -59,6 +59,7 @@ Every set can be made into a discrete nominal set, where supp x = ∅.
 -/
 section Discrete
 
+@[reducible]
 def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where
   smul π x := x
   one_smul := by intro; rfl
@@ -330,6 +331,7 @@ instance : PermSet 𝔸 (Quotient setoid) where
 instance instMkEquivariant : Function.Equivariant 𝔸 (Quotient.mk setoid) := by
   constructor; simp
 
+@[reducible]
 def lift_equivariant
     {Y : Type} [PermSet 𝔸 Y] (f : X → Y) [Function.Equivariant 𝔸 f]
     (h : ∀ (a b : X), a ≈ b → f a = f b) :
@@ -392,11 +394,11 @@ instance : PermSet 𝔸 S where
     rw [← Set.equivariant 𝔸 S]
     exact x.prop⟩
   one_smul x := by
-    apply Subtype.eq
+    apply Subtype.ext
     exact MulAction.one_smul x.val
   mul_smul π τ x := by
-    apply Subtype.eq
-    exact MulAction.mul_smul π τ x.val
+    apply Subtype.ext
+    exact SemigroupAction.mul_smul π τ x.val
 
 @[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl
 
@@ -410,7 +412,7 @@ instance : NominalSet 𝔸 S where
     use NominalSet.supp 𝔸 x.val
     constructor
     · intro π hπ
-      apply Subtype.eq
+      apply Subtype.ext
       exact NominalSet.supp_is_support 𝔸 hπ
     · exact NominalSet.supp_finite 𝔸
 
diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean
index 91f4fb8..7af82cd 100644
--- a/Nominal/LambdaCalculus/Terms.lean
+++ b/Nominal/LambdaCalculus/Terms.lean
@@ -53,40 +53,37 @@ instance Preterm.instSetoidEquivariant : Rel.Equivariant Var setoid.r := by
     exact h
 
 /-- Define λ-terms as the quotient Preterm/≈. -/
-def Term := Quotient Preterm.setoid
+abbrev Term := Quotient Preterm.setoid
 
 namespace Term
 
-/-- The equivalence class of a λ-preterm. -/
-abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid
-
 instance : NominalSet Var Term := Quotient.instNominalSet Var
 
 @[simp]
-lemma smul {π : FPerm Var} {t : Preterm} : π • Term.mk t = Term.mk (π • t) := by congr
+lemma smul {π : FPerm Var} {t : Preterm} : π • (⟦t⟧ : Term) = ⟦π • t⟧ := by congr
 
 private lemma alpha_eq {t u : Preterm} : t ≈ u ↔ AlphaEq t u := by rfl
 
-lemma eq_iff_alpha_eq {t u : Preterm} : mk t = mk u ↔ t ≈ u := by
+lemma eq_iff_alpha_eq {t u : Preterm} : (⟦t⟧ : Term) = (⟦u⟧ : Term) ↔ t ≈ u := by
   rw [Quotient.eq_iff_equiv]
 
-def var : Var → Term := fun x => mk (.var x)
+def var : Var → Term := fun x => ⟦.var x⟧
 
 def abs : Var → Term → Term := fun x =>
   Quotient.lift
-    (fun t => mk (.abs x t))
+    (fun t => ⟦.abs x t⟧)
     (by intro t t'; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_abs)
 
 def app : Term → Term → Term :=
   Quotient.lift₂
-    (fun t u => mk (.app t u))
+    (fun t u => ⟦.app t u⟧)
     (by intro t₁ t₂ u₁ u₂; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_app)
 
 @[simp]
-lemma abs_preterm {x : Var} {t : Preterm} : abs x (mk t) = mk (.abs x t) := rfl
+lemma abs_preterm {x : Var} {t : Preterm} : abs x ⟦t⟧ = ⟦.abs x t⟧ := rfl
 
 @[simp]
-lemma app_preterm {t u : Preterm} : app (mk t) (mk u) = mk (.app t u) := rfl
+lemma app_preterm {t u : Preterm} : app ⟦t⟧ ⟦u⟧ = ⟦.app t u⟧ := rfl
 
 /-- Alternative characterization of α-equivalence for each preterm constructor. -/
 inductive AlphaEq' : Preterm → Preterm → Prop where
@@ -242,7 +239,6 @@ lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫
   obtain ⟨u', hu'⟩ := u.exists_rep
   simp only [abs, ← ht', Quotient.lift_mk, ← hu']
   rw [Quotient.eq_iff_equiv, alpha_eq_abs]
-  rfl
 
 /-- Alternative characterization of α-equivalence for application preterms. -/
 lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by
@@ -295,7 +291,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term
       (by
         intro t u htu
         rw [alpha_eq, alpha_eq_iff] at htu
-        cases htu <;> simp only [Sum.inr.injEq, Sum.inl.injEq, *]; assumption)
+        cases htu <;> simp [*])
     invFun
       | .inl x => .var x
       | .inr (.inl x) => Quotient.liftOn x
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 0a4974a..f1115d3 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -42,7 +42,7 @@ lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by
 
 /-- The support of the inverse function is the same as the function's support. -/
 lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by
-  simp [supp, set_support_inv_eq]
+  simp [supp, set_support_symm_eq]
 
 /-- The support of two concatenated permutations is a subset of the individual supports as a union. -/
 lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by
@@ -199,10 +199,10 @@ instance : PermSet 𝔸 𝔸 where
 
 instance : OrbitFinite 𝔸 𝔸 where
   fin_orbits := Finite.of_equiv Unit
-    { toFun _ := Quotient.mk _ (inferInstanceAs (Nonempty 𝔸)).some
+    { toFun _ := Quotient.mk _ (inferInstance : Nonempty 𝔸).some
       invFun _ := ()
       right_inv := by
-        let chosen := (inferInstanceAs (Nonempty 𝔸)).some
+        let chosen := (inferInstance : Nonempty 𝔸).some
         apply Quotient.ind; intro a
         rw [Quotient.eq]
         show chosen ∈ MulAction.orbit (FPerm 𝔸) a
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 7888a68..fde20c7 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -79,7 +79,7 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite
       simp)
   let m' := (S \ T).restrict m
   rw [Set.injOn_iff_injective, show (S \ T).restrict m = m' by rfl] at h_m_injective
-  obtain h_m_inv := Function.partialInv_of_injective h_m_injective
+  obtain h_m_inv := h_m_injective.isPartialInv
   have h_m_image : m '' (S \ T) ⊆ (π'.supp ∪ S ∪ T)ᶜ :=
     Set.image_subset_iff.mpr h_m_preimage
 
diff --git a/flake.lock b/flake.lock
index 99d3a8f..d1e7f8c 100644
--- a/flake.lock
+++ b/flake.lock
@@ -20,11 +20,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1764167966,
-        "narHash": "sha256-nXv6xb7cq+XpjBYIjWEGTLCqQetxJu6zvVlrqHMsCOA=",
+        "lastModified": 1775888245,
+        "narHash": "sha256-nwASzrRDD1JBEu/o8ekKYEXm/oJW6EMCzCRdrwcLe90=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "5c46f3bd98147c8d82366df95bbef2cab3a967ea",
+        "rev": "13043924aaa7375ce482ebe2494338e058282925",
         "type": "github"
       },
       "original": {
diff --git a/lake-manifest.json b/lake-manifest.json
index 6dce1af..707a535 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ccd71f89cbbd82ae7d097723ce1722ca7b01c33",
+   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0",
+   "inputRev": "v4.29.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3",
+   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb",
+   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d",
+   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.79",
+   "inputRev": "v0.0.95",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349",
+   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f",
+   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5c78955e8375f872c085514cb521216bac1bda17",
+   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,11 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0",
+   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0",
+   "inputRev": "v4.29.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
- "name": "CoalgebraicAutomata",
+ "name": "Nominal",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 21e9fc9..513bf8e 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -5,7 +5,7 @@ defaultTargets = ["Nominal"]
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.25.0"
+rev = "v4.29.0"
 
 [[lean_lib]]
 name = "Nominal"
@@ -15,4 +15,4 @@ name = "Graded"
 
 [[lean_lib]]
 name = "Algebra"
-needs = ["Nominal", "Graded"]
\ No newline at end of file
+needs = ["Nominal", "Graded"]
diff --git a/lean-toolchain b/lean-toolchain
index e5ab73a..d324cad 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.25.0
+leanprover/lean4:v4.29.0
\ No newline at end of file
-- 
cgit v1.3.1