diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 22a3d6787..b969bf9c2 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -181,26 +181,27 @@ theorem ChurchRosser.normal_eq (cr : ChurchRosser r) (nx : Normal r x) (ny : Nor
 
 /-- A pair of subrelations lifts to transitivity on the relation. -/
 @[implicit_reducible]
-def trans_of_subrelation (s s' r : α → α → Prop) (hr : Transitive r)
+def trans_of_subrelation (s s' r : α → α → Prop) (hr : IsTrans α r)
     (h : Subrelation s r) (h' : Subrelation s' r) : Trans s s' r where
-  trans hab hbc := hr (h hab) (h' hbc)
+  trans hab hbc := hr.trans _ _ _ (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)
+def trans_of_subrelation_left (s r : α → α → Prop) (hr : IsTrans α r)
     (h : Subrelation s r) : Trans s r r where
-  trans hab hbc := hr (h hab) hbc
+  trans hab hbc := hr.trans _ _ _ (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)
+def trans_of_subrelation_right (s r : α → α → Prop) (hr : IsTrans α r)
     (h : Subrelation s r) : Trans r s r where
-  trans hab hbc := hr hab (h hbc)
+  trans hab hbc := hr.trans _ _ _ hab (h hbc)
 
 /-- Confluence implies that multi-step joinability is an equivalence. -/
 theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) :
     Equivalence (Join (ReflTransGen r)) := by
-  grind [equivalence_join, reflexive_reflTransGen, transitive_reflTransGen]
+  apply equivalence_join reflexive_reflTransGen inferInstance
+  grind
 
 /-- A relation is terminating when the inverse of its transitive closure is well-founded.
   Note that this is also called Noetherian or strongly normalizing in the literature. -/
diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean
index ff3a07b29..d2553421b 100644
--- a/Cslib/Languages/CombinatoryLogic/Confluence.lean
+++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean
@@ -92,13 +92,13 @@ theorem reflTransGen_parallelReduction_mRed :
     ReflTransGen ParallelReduction = ReflTransGen Red := by
   ext a b
   constructor
-  · apply Relation.reflTransGen_of_transitive_reflexive
-    · exact fun _ => by rfl
-    · exact Relation.transitive_reflTransGen
+  · apply Relation.reflTransGen_of_isTrans_reflexive
+    · exact Relation.reflexive_reflTransGen
+    · infer_instance
     · exact @mRed_of_parallelReduction
-  · apply Relation.reflTransGen_of_transitive_reflexive
+  · apply Relation.reflTransGen_of_isTrans_reflexive
     · exact Relation.reflexive_reflTransGen
-    · exact Relation.transitive_reflTransGen
+    · infer_instance
     · exact fun a a' h => Relation.ReflTransGen.single (parallelReduction_of_red h)
 
 /-!
diff --git a/lake-manifest.json b/lake-manifest.json
index 753330ea6..6b469356b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "698d2b68b870f1712040ab0c233d34372d4b56df",
+   "rev": "1a37cd3c8e618022c5e78dee604c75c3c946a681",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "22a0afa903bcf65285152eea298a3d319badc78d",
+   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "db22912cdd820b2a2bd84bd25273cb322ff09ead",
+   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "136730b5a40dc633967f5433cb7668df5c3bf9a3",
+   "rev": "00fe208b8e1364736cca3a9b9601c4fe865856af",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.94",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3426969888a264d3f69b6f30ab50aa11f28eb38d",
+   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3a9fde028258300f1cbb003d457d47c8d8e16b1c",
+   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb",
+   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866",
+   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-rc8",
+   "inputRev": "v4.29.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "cslib",
diff --git a/lean-toolchain b/lean-toolchain
index ccec351f4..14791d727 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc8
+leanprover/lean4:v4.29.0