diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 1d652df..a39e5d9 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -54,17 +54,11 @@ jobs:
         if: github.ref_type == 'tag'
         uses: softprops/action-gh-release@v1
 
-      # TODO: replace with just `lake upload $RELEASE_TAG` when lean4#2713 is fixed
-      # References:
-      # https://docs.github.com/en/actions/learn-github-actions/contexts#runner-context
-      # https://stackoverflow.com/questions/8766730/tar-command-in-mac-os-x-adding-hidden-files-why
       - name: Upload release archive
         if: github.ref_type == 'tag'
         # All our runners are 64-bit ¯\_(ツ)_/¯
         run: |
-          export COPYFILE_DISABLE=true
-          tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./build .
-          gh release upload ${RELEASE_TAG} ./${LEAN_OS}-64.tar.gz
+          lake upload ${RELEASE_TAG}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           RELEASE_TAG: ${{ github.ref_name }}
diff --git a/.gitignore b/.gitignore
index b3a637d..80024d7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
+.lake
+DuperOnMathlib/.lake
 /build
 /lake-packages
 /lean_packages
diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean
index feb27d1..067b286 100644
--- a/Duper/Tests/test_regression.lean
+++ b/Duper/Tests/test_regression.lean
@@ -682,4 +682,4 @@ theorem proj_test (h1 : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0) (h2 : 3 >
 def sk (a b : Nat) (c : Nat × Nat) (h1 : c = (a, b)) : c.1 = a := by
   duper [h1]
 
-#print sk.proof_1
+#print sk
diff --git a/DuperOnMathlib/DuperOnMathlib.lean b/DuperOnMathlib/DuperOnMathlib.lean
index 32a84a6..a4eb99f 100644
--- a/DuperOnMathlib/DuperOnMathlib.lean
+++ b/DuperOnMathlib/DuperOnMathlib.lean
@@ -1,3 +1,2 @@
 import DuperOnMathlib.Prime
 import DuperOnMathlib.Cantor
-import DuperOnMathlib.PrimesModFour
diff --git a/DuperOnMathlib/lake-manifest.json b/DuperOnMathlib/lake-manifest.json
index c572c53..fc82926 100644
--- a/DuperOnMathlib/lake-manifest.json
+++ b/DuperOnMathlib/lake-manifest.json
@@ -1,61 +1,74 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
-    "subDir?": null,
-    "rev": "4e5518cafc0efd7c7b7d287fa960fce5201908db",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": "4e5518cafc0efd7c7b7d287fa960fce5201908db",
-    "inherited": false}},
-  {"path": {"opts": {}, "name": "Duper", "inherited": false, "dir": "./../"}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/quote4",
-    "subDir?": null,
-    "rev": "396201245bf244f9d78e9007a02dd1c388193d27",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/lean4-cli",
-    "subDir?": null,
-    "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/ProofWidgets4",
-    "subDir?": null,
-    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.21",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/lean-auto.git",
-    "subDir?": null,
-    "rev": "c42a69000568fbadd8bc5664ed22b64b7ff96a62",
-    "opts": {},
-    "name": "auto",
-    "inputRev?": "v0.0.2",
-    "inherited": true}}],
- "name": "duperOnMathlib"}
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.23",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "rev": "75641abe702d35c946b6e59b8dc672c7e6d80b13",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.4.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "b61345f6d42675298f8fa2b0cc5c471c264a6b40",
+   "name": "auto",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.4",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "Duper",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../",
+   "configFile": "lakefile.lean"}],
+ "name": "duperOnMathlib",
+ "lakeDir": ".lake"}
diff --git a/DuperOnMathlib/lakefile.lean b/DuperOnMathlib/lakefile.lean
index ed2efc4..2479881 100644
--- a/DuperOnMathlib/lakefile.lean
+++ b/DuperOnMathlib/lakefile.lean
@@ -5,7 +5,7 @@ package «duperOnMathlib» {
   -- add any package configuration options here
 }
 
-require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "4e5518cafc0efd7c7b7d287fa960fce5201908db"
+require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "v4.4.0-rc1"
 
 require «Duper» from "../"
 
diff --git a/DuperOnMathlib/lean-toolchain b/DuperOnMathlib/lean-toolchain
index e856017..91ccf6a 100644
--- a/DuperOnMathlib/lean-toolchain
+++ b/DuperOnMathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.4.0-rc1
diff --git a/lake-manifest.json b/lake-manifest.json
index ddde9b0..48d34f7 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,20 +1,23 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/lean-auto.git",
-    "subDir?": null,
-    "rev": "c42a69000568fbadd8bc5664ed22b64b7ff96a62",
-    "opts": {},
-    "name": "auto",
-    "inputRev?": "v0.0.2",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4.git",
-    "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}}],
- "name": "Duper"}
+ [{"url": "https://github.com/leanprover/std4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "b61345f6d42675298f8fa2b0cc5c471c264a6b40",
+   "name": "auto",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.4",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Duper",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 280a3bd..60ce173 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v0.0.2"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v0.0.4"
 
 package Duper {
   precompileModules := true
diff --git a/lean-toolchain b/lean-toolchain
index e856017..91ccf6a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.4.0-rc1