diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index edc73333..6491b468 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -107,9 +107,9 @@ lemma step_abs_close {x : Var} : (M ⭢βᶠ M') → (M⟦0 ↜ x⟧.abs ⭢β
 lemma redex_abs_close {x : Var} : (M ↠βᶠ M') → (M⟦0 ↜ x⟧.abs ↠βᶠ M'⟦0 ↜ x⟧.abs) :=  by
   intros step
   induction step using Relation.ReflTransGen.trans_induction_on
-  case ih₁ => rfl
-  case ih₂ ih => exact Relation.ReflTransGen.single (step_abs_close ih)
-  case ih₃ l r => exact .trans l r
+  case refl => rfl
+  case single ih => exact Relation.ReflTransGen.single (step_abs_close ih)
+  case trans l r => exact .trans l r
 
 /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
 theorem redex_abs_cong (xs : Finset Var) : 
diff --git a/Cslib/Semantics/ReductionSystem/Basic.lean b/Cslib/Semantics/ReductionSystem/Basic.lean
index c06a290e..a3742eeb 100644
--- a/Cslib/Semantics/ReductionSystem/Basic.lean
+++ b/Cslib/Semantics/ReductionSystem/Basic.lean
@@ -43,13 +43,6 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b)
 
 open Relation Relation.ReflTransGen
 
--- these instances allow us to switch between single and multistep reductions in a `calc` block
-instance {α} (R : α → α → Prop) : Trans R (ReflTransGen R) (ReflTransGen R) where
-  trans := head
-
-instance {α} (R : α → α → Prop) : Trans (ReflTransGen R) R (ReflTransGen R) where
-  trans := tail
-
 instance (rs : ReductionSystem Term) : Trans rs.Red rs.MRed rs.MRed := by infer_instance
 instance (rs : ReductionSystem Term) : Trans rs.MRed rs.Red rs.MRed := by infer_instance
 
diff --git a/docs/lake-manifest.json b/docs/lake-manifest.json
index 2921873c..55d12c99 100644
--- a/docs/lake-manifest.json
+++ b/docs/lake-manifest.json
@@ -22,27 +22,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "928758ac3743dc7f171fc66f450506723896f1c5",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc4",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c37191eba2da78393070da8c4367689d8c4276e4",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,50 +52,50 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.67",
+   "inputRev": "v0.0.68",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef3dac0f872ca6aaa7d02e015427e06dd0b6195",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/docs/lean-toolchain b/docs/lean-toolchain
index 8ce10238..1f2f20aa 100644
--- a/docs/lean-toolchain
+++ b/docs/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc4
\ No newline at end of file
+leanprover/lean4:v4.22.0
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
index 8cc16931..41d60bcf 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "928758ac3743dc7f171fc66f450506723896f1c5",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc4",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c37191eba2da78393070da8c4367689d8c4276e4",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,50 +35,50 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.67",
+   "inputRev": "v0.0.68",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef3dac0f872ca6aaa7d02e015427e06dd0b6195",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.toml b/lakefile.toml
index e693bf44..225d1be1 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,7 +9,7 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.22.0-rc4"
+rev = "v4.22.0"
 
 [[lean_lib]]
 name = "Cslib"
diff --git a/lean-toolchain b/lean-toolchain
index 8ce10238..1f2f20aa 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc4
\ No newline at end of file
+leanprover/lean4:v4.22.0
\ No newline at end of file