diff --git a/Regex/NFA/Compile/Basic.lean b/Regex/NFA/Compile/Basic.lean
index 27a1c77..ecd6275 100644
--- a/Regex/NFA/Compile/Basic.lean
+++ b/Regex/NFA/Compile/Basic.lean
@@ -24,7 +24,7 @@ theorem pushNode_get_lt {nfa : NFA} {node : Node}
   (i : Nat) (h : i < nfa.nodes.size) :
   (nfa.pushNode node).val[i]'(Nat.lt_trans h (nfa.pushNode node).property) = nfa[i] := by
   simp [pushNode, get_eq_nodes_get]
-  rw [Array.get_push_lt]
+  rw [Array.getElem_push_lt]
 
 @[simp]
 theorem pushNode_get_eq {nfa : NFA} {node : Node} :
diff --git a/Regex/NFA/Compile/Lemmas.lean b/Regex/NFA/Compile/Lemmas.lean
index 4d6bdce..8a2ab57 100644
--- a/Regex/NFA/Compile/Lemmas.lean
+++ b/Regex/NFA/Compile/Lemmas.lean
@@ -14,7 +14,7 @@ theorem pushNode_wf {nfa : NFA} {node}
   intro i
   cases Nat.lt_or_ge i.val nfa.nodes.size with
   | inl lt =>
-    have : (nfa.nodes.push node)[i.val] = nfa.nodes[i.val] := nfa.nodes.get_push_lt _ _ lt
+    have : (nfa.nodes.push node)[i.val] = nfa.nodes[i.val] := nfa.nodes.getElem_push_lt _ _ lt
     simp [this]
     apply Node.inBounds_of_inBounds_of_le (wf.inBounds ⟨i.val, lt⟩) (by omega)
   | inr ge =>
diff --git a/Regex/NFA/Compile/ProofData/Basic.lean b/Regex/NFA/Compile/ProofData/Basic.lean
index e96c310..700be26 100644
--- a/Regex/NFA/Compile/ProofData/Basic.lean
+++ b/Regex/NFA/Compile/ProofData/Basic.lean
@@ -104,7 +104,7 @@ theorem get (i : Nat) (h : i < nfa'.nodes.size) :
 end Epsilon
 
 class Char extends ProofData where
-  c : Char
+  c : _root_.Char
   expr_eq : e = .char c
 
 namespace Char
@@ -143,7 +143,7 @@ theorem get (i : Nat) (h : i < nfa'.nodes.size) :
 end Char
 
 class Classes extends ProofData where
-  cs : Classes
+  cs : Data.Classes
   expr_eq : e = .classes cs
 
 namespace Classes
diff --git a/RegexCorrectness/Data/Array.lean b/RegexCorrectness/Data/Array.lean
index 7f919bb..e8cef66 100644
--- a/RegexCorrectness/Data/Array.lean
+++ b/RegexCorrectness/Data/Array.lean
@@ -29,7 +29,7 @@ theorem Array.push_pop_eq (a : Array α) (hemp : ¬ a.isEmpty) :
   . simp [Nat.sub_add_cancel this]
   . simp [Nat.sub_add_cancel this]
     intro i h _
-    rw [Array.get_push]
+    rw [Array.getElem_push]
     split
     case isTrue h' => rw [Array.getElem_pop]
     case isFalse h' =>
diff --git a/lake-manifest.json b/lake-manifest.json
index 0b8e325..dfdc690 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,72 +1,82 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
-   "name": "batteries",
+   "scope": "leanprover",
+   "rev": "0a8cd7afb471bb1fdd335118bf1e253a38a2af53",
+   "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
+   "inputRev": "v4.14.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-parser",
+   "type": "git",
+   "subDir": null,
+   "scope": "fgdorais",
+   "rev": "711662ab6f3c4c0080f6379737b41b1089d3d3f8",
+   "name": "Parser",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "711662ab6f3c4c0080f6379737b41b1089d3d3f8",
+   "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
-   "name": "Qq",
+   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
+   "inputRev": "v4.14.0",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+  {"url": "https://github.com/mhuisi/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
-   "name": "aesop",
+   "scope": "",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
-   "name": "proofwidgets",
+   "scope": "",
+   "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff",
+   "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.44",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/dupuisf/BibtexQuery",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
+   "scope": "",
+   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
+   "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
-   "name": "importGraph",
+   "scope": "",
+   "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
-   "name": "LeanSearchClient",
+   "scope": "",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -75,71 +85,61 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7317655e2826dc1f1de9a0c138db2775c4bb841",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.13.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "c45466d308879f48e06cbb9baa9de48bb7b164e0",
-   "name": "UnicodeBasic",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-parser",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "scope": "fgdorais",
-   "rev": "176dab14ce044b48203d159ef604e04d7e050fa2",
-   "name": "Parser",
+   "scope": "leanprover-community",
+   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "176dab14ce044b48203d159ef604e04d7e050fa2",
-   "inherited": false,
+   "inputRev": "v4.14.0",
+   "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/acmepjz/md4lean",
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
-   "name": "MD4Lean",
+   "scope": "leanprover-community",
+   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
+   "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.47",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
-   "name": "BibtexQuery",
+   "scope": "leanprover-community",
+   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.14.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "c2156beadb1a4d049ff3b19fe396c5403025aac5",
-   "name": "«doc-gen4»",
+   "scope": "leanprover-community",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.13.0",
-   "inherited": false,
+   "inputRev": "master",
+   "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "Regex",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 20f2e5f..fea34a4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,9 +13,9 @@ lean_lib RegexCorrectness where
 -- TODO: make a proper test_driver
 lean_exe Test where
 
-require "leanprover-community" / "mathlib" @ git "v4.13.0"
-require "fgdorais" / "Parser" @ git "176dab14ce044b48203d159ef604e04d7e050fa2"
+require "leanprover-community" / "mathlib" @ git "v4.14.0"
+require "fgdorais" / "Parser" @ git "711662ab6f3c4c0080f6379737b41b1089d3d3f8"
 
 -- TODO: stop using meta if
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
-require "leanprover" / "doc-gen4" @ git "v4.13.0"
+require "leanprover" / "doc-gen4" @ git "v4.14.0"
diff --git a/lean-toolchain b/lean-toolchain
index 4f86f95..401bc14 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0
\ No newline at end of file