diff --git a/.github/workflows/check_proofs.yml b/.github/workflows/check_proofs.yml
index a8f4042..89f40d1 100644
--- a/.github/workflows/check_proofs.yml
+++ b/.github/workflows/check_proofs.yml
@@ -22,7 +22,7 @@ jobs:
         run: |
           curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
           chmod u+x elan-init.sh
-          ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.2.0-rc4
+          ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.11.0-rc2
           echo "Adding location $HOME/.elan/bin to PATH..."
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
diff --git a/Katydid/Conal/Calculus.lean b/Katydid/Conal/Calculus.lean
index 67ce595..18b7dc1 100644
--- a/Katydid/Conal/Calculus.lean
+++ b/Katydid/Conal/Calculus.lean
@@ -66,7 +66,7 @@ attribute [simp] ν' δ'
 
 -- ν∅  : ν ∅ ≡ ⊥
 -- ν∅ = refl
-theorem nullable_emptySet:
+def nullable_emptySet:
   ∀ (α: Type),
     @ν' α ∅ ≡ PEmpty := by
   intro α
@@ -75,7 +75,7 @@ theorem nullable_emptySet:
 
 -- ν𝒰  : ν 𝒰 ≡ ⊤
 -- ν𝒰 = refl
-theorem nullable_universal:
+def nullable_universal:
   ∀ (α: Type),
     @ν' α 𝒰 ≡ PUnit := by
   intro α
@@ -88,7 +88,7 @@ theorem nullable_universal:
 --   (λ { tt → refl })
 --   (λ { tt → refl })
 --   (λ { refl → refl })
-theorem nullable_emptyStr:
+def nullable_emptyStr:
   ∀ (α: Type),
     @ν' α ε ≃ PUnit := by
   intro α
@@ -104,7 +104,7 @@ theorem nullable_emptyStr:
   intro _
   simp
 
-theorem nullable_emptyStr':
+def nullable_emptyStr':
   ∀ (α: Type),
     @ν' α ε ≃ PUnit :=
     fun _ => Equiv.mk
@@ -115,7 +115,7 @@ theorem nullable_emptyStr':
 
 -- ν`  : ν (` c) ↔ ⊥
 -- ν` = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
-theorem nullable_char:
+def nullable_char:
   ∀ (c: α),
     ν' (char c) ≃ PEmpty := by
   intro α
@@ -130,7 +130,7 @@ theorem nullable_char:
   sorry
   sorry
 
-theorem nullable_char':
+def nullable_char':
   ∀ (c: α),
     ν' (char c) -> PEmpty := by
   intro
@@ -145,7 +145,7 @@ theorem nullable_char':
 
 -- ν∪  : ν (P ∪ Q) ≡ (ν P ⊎ ν Q)
 -- ν∪ = refl
-theorem nullable_or:
+def nullable_or:
   ∀ (P Q: dLang α),
     ν' (P ⋃ Q) ≡ (Sum (ν' P) (ν' Q)) := by
   intro P Q
@@ -154,7 +154,7 @@ theorem nullable_or:
 
 -- ν∩  : ν (P ∩ Q) ≡ (ν P × ν Q)
 -- ν∩ = refl
-theorem nullable_and:
+def nullable_and:
   ∀ (P Q: dLang α),
     ν' (P ⋂ Q) ≡ (Prod (ν' P) (ν' Q)) := by
   intro P Q
@@ -163,7 +163,7 @@ theorem nullable_and:
 
 -- ν·  : ν (s · P) ≡ (s × ν P)
 -- ν· = refl
-theorem nullable_scalar:
+def nullable_scalar:
   ∀ (s: Type) (P: dLang α),
     ν' (dLang.scalar s P) ≡ (Prod s (ν' P)) := by
   intro P Q
@@ -176,7 +176,7 @@ theorem nullable_scalar:
 --   (λ { (νP , νQ) → ([] , []) , refl , νP , νQ })
 --   (λ { (νP , νQ) → refl } )
 --   (λ { (([] , []) , refl , νP , νQ) → refl})
-theorem nullable_concat:
+def nullable_concat:
   ∀ (P Q: dLang α),
     ν' (P, Q) ≃ (Prod (ν' Q) (ν' P)) := by
   -- TODO
@@ -210,7 +210,7 @@ theorem nullable_concat:
 --   ≈⟨ ν✪ ⟩
 --     (ν P) ✶
 --   ∎ where open ↔R
-theorem nullable_star:
+def nullable_star:
   ∀ (P: dLang α),
     ν' (P *) ≃ List (ν' P) := by
   -- TODO
@@ -218,7 +218,7 @@ theorem nullable_star:
 
 -- δ∅  : δ ∅ a ≡ ∅
 -- δ∅ = refl
-theorem derivative_emptySet:
+def derivative_emptySet:
   ∀ (a: α),
     (δ' ∅ a) ≡ ∅ := by
   intro a
@@ -227,7 +227,7 @@ theorem derivative_emptySet:
 
 -- δ𝒰  : δ 𝒰 a ≡ 𝒰
 -- δ𝒰 = refl
-theorem derivative_universal:
+def derivative_universal:
   ∀ (a: α),
     (δ' 𝒰 a) ≡ 𝒰 := by
   intro a
@@ -237,7 +237,7 @@ theorem derivative_universal:
 -- δ𝟏  : δ 𝟏 a ⟷ ∅
 -- δ𝟏 = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_emptyStr:
+def derivative_emptyStr:
   ∀ (a: α),
     (δ' ε a) ≡ ∅ := by
   -- TODO
@@ -250,7 +250,7 @@ theorem derivative_emptyStr:
 --   (λ { (refl , refl) → refl })
 --   (λ { refl → refl })
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_char:
+def derivative_char:
   ∀ (a: α) (c: α),
     (δ' (char c) a) ≡ dLang.scalar (a ≡ c) ε := by
     intros a c
@@ -262,7 +262,7 @@ theorem derivative_char:
 
 -- δ∪  : δ (P ∪ Q) a ≡ δ P a ∪ δ Q a
 -- δ∪ = refl
-theorem derivative_or:
+def derivative_or:
   ∀ (a: α) (P Q: dLang α),
     (δ' (P ⋃ Q) a) ≡ ((δ' P a) ⋃ (δ' Q a)) := by
   intro a P Q
@@ -271,7 +271,7 @@ theorem derivative_or:
 
 -- δ∩  : δ (P ∩ Q) a ≡ δ P a ∩ δ Q a
 -- δ∩ = refl
-theorem derivative_and:
+def derivative_and:
   ∀ (a: α) (P Q: dLang α),
     (δ' (P ⋂ Q) a) ≡ ((δ' P a) ⋂ (δ' Q a)) := by
   intro a P Q
@@ -280,7 +280,7 @@ theorem derivative_and:
 
 -- δ·  : δ (s · P) a ≡ s · δ P a
 -- δ· = refl
-theorem derivative_scalar:
+def derivative_scalar:
   ∀ (a: α) (s: Type) (P: dLang α),
     (δ (dLang.scalar s P) a) ≡ (dLang.scalar s (δ' P a)) := by
   intro a s P
@@ -298,7 +298,7 @@ theorem derivative_scalar:
 --   (λ { (([] , .(a ∷ w)) , refl , νP , Qaw) → refl
 --      ; ((.a ∷ u , v) , refl , Pu , Qv) → refl })
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_concat:
+def derivative_concat:
   ∀ (a: α) (P Q: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
     (δ' (P , Q) a) ≡ dLang.scalar (ν' P) ((δ' Q a) ⋃ ((δ' P a), Q)) := by
@@ -338,7 +338,7 @@ theorem derivative_concat:
 --     ((ν P) ✶ · (δ P a ⋆ P ☆)) w
 --   ∎ where open ↔R
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_star:
+def derivative_star:
   ∀ (a: α) (P: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
     (δ' (P *) a) ≡ dLang.scalar (List (ν' P)) (δ' P a, P *) := by
diff --git a/Katydid/Conal/Language.lean b/Katydid/Conal/Language.lean
index 07a70e6..523e164 100644
--- a/Katydid/Conal/Language.lean
+++ b/Katydid/Conal/Language.lean
@@ -163,10 +163,10 @@ inductive Lang : (List α -> Type u) -> Type (u + 1) where
 
 #check @Lang.casesOn
 
--- 𝜈 : Lang P → Dec (⋄.𝜈 P)
-theorem ν {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
-  induction f with
-  | universal => exact unit?
+-- TODO: 𝜈 : Lang P → Dec (⋄.𝜈 P)
+-- theorem ν {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
+--   induction f with
+--   | universal => exact unit?
 
 -- TODO: rewrite ν using casesOn
 -- def ν' {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
diff --git a/Katydid/Std/Balistic.lean b/Katydid/Std/Balistic.lean
index 7abb285..239841a 100644
--- a/Katydid/Std/Balistic.lean
+++ b/Katydid/Std/Balistic.lean
@@ -276,6 +276,7 @@ example (xs ys zs: List α):
   ys = zs -> ys ++ xs = zs ++ xs := by
   list_app
 
+-- set_option linter.constructorNameAsVariable false in
 local elab "wreck_exists" : tactic => newTactic do
   let hyps ← getHypotheses
   for (name, ty) in hyps do
diff --git a/Katydid/Std/Lists.lean b/Katydid/Std/Lists.lean
index 6622e05..021efee 100644
--- a/Katydid/Std/Lists.lean
+++ b/Katydid/Std/Lists.lean
@@ -488,7 +488,7 @@ theorem list_take_take (n n: Nat) (xs: List α):
       unfold minOfLe
       simp only
       split
-      case succ.succ.inl h =>
+      next h =>
         rw [nat_succ_le_succ_iff] at h
         cases xs with
         | nil =>
@@ -506,7 +506,7 @@ theorem list_take_take (n n: Nat) (xs: List α):
           have ihn' : _ := @ihn m xs
           rw [hmin] at ihn'
           exact ihn'
-      case succ.succ.inr h =>
+      next h =>
         rw [nat_succ_le_succ_iff] at h
         cases xs with
         | nil =>
@@ -687,14 +687,13 @@ theorem list_take_length (n: Nat) (xs: List α):
   unfold minOfLe
   simp only [length_take, ge_iff_le]
   split
-  case inl =>
+  next =>
     rename_i c
     unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_left_iff, not_le]
     intro c'
     linarith
-  case inr =>
+  next =>
     rename_i c
-    have c' := gt_of_not_le c
     unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_right_iff]
     intro c''
     linarith
diff --git a/Katydid/Std/Ltac.lean b/Katydid/Std/Ltac.lean
index f8ea247..7d3cb75 100644
--- a/Katydid/Std/Ltac.lean
+++ b/Katydid/Std/Ltac.lean
@@ -1,4 +1,4 @@
-import Std.Lean.Meta.UnusedNames
+import Lean.Meta.Tactic.Util
 import Qq
 open Qq
 
@@ -108,8 +108,9 @@ example (H: x): x /\ x := by
   example_assumption_tactic
 
 -- Creates a fresh variable with the suggested name.
-def fresh [Monad m] [Lean.MonadLCtx m] (suggestion : Lean.Name) : m Lean.Syntax.Ident := do
-  let name ← Lean.Meta.getUnusedUserName suggestion
+def fresh [Monad m] [Lean.MonadLCtx m] (suggestion : String) : m Lean.Syntax.Ident := do
+  let lctx ← Lean.MonadLCtx.getLCtx
+  let name := lctx.getUnusedName (Lean.Name.mkSimple suggestion)
   return Lean.mkIdent name
 
 -- Removes quotes from the start of a string
@@ -186,19 +187,3 @@ example (P: (A -> B) /\ A): B := by
 --  - https://github.com/leanprover-community/mathlib4/blob/2d97a156aa63b50456ed3e5a7d6af3096ac7958e/Mathlib/Tactic/Tauto.lean
 --  - https://github.com/leanprover-community/mathlib4/blob/bac7310cc18d6ed292606d26ccb5fb9ffc697c7a/Mathlib/Tactic/Slice.lean
 --  - https://github.com/siddhartha-gadgil/LeanAide
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/Katydid/Std/Tipe2.lean b/Katydid/Std/Tipe2.lean
index c6808f8..d8cd5ee 100644
--- a/Katydid/Std/Tipe2.lean
+++ b/Katydid/Std/Tipe2.lean
@@ -25,7 +25,7 @@ example : 1 ≡ 1 := by
 -- TODO: How can we make rewrite easier, without needing to destruct first?
 --   TODO: if all else fails, write a tactic
 
-theorem rewrite_test:
+def rewrite_test:
   ∀ (_: a ≡ b) (_: b ≡ c),
     a ≡ c := by
   intro ab bc
@@ -37,7 +37,7 @@ theorem rewrite_test:
     | mk bc =>
       rw [bc]
 
-theorem rewrite_test':
+def rewrite_test':
   ∀ (_: a ≡ b) (_: b ≡ c),
     a ≡ c := by
   intro ab bc
@@ -55,7 +55,7 @@ def rewrite_test'' (ab: a ≡ b) (bc: b ≡ c): a ≡ c :=
   match (ab, bc) with
   | ⟨ ⟨ ab' ⟩ , ⟨ bc' ⟩ ⟩ => by sorry
 
-theorem rewrite_test''':
+def rewrite_test''':
   ∀ (_: a ≡ b) (_: b ≡ c),
     a ≡ c := by
   intro ab bc
diff --git a/lake-manifest.json b/lake-manifest.json
index e84a3bf..d378740 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,12 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
-   "name": "std",
+   "scope": "leanprover-community",
+   "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -13,7 +14,8 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "scope": "leanprover-community",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,56 +24,52 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c",
+   "scope": "leanprover-community",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "scope": "leanprover-community",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3",
+   "scope": "leanprover-community",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "19b5ded3c60a6da7b357a126fb56b56671d231e3",
+   "scope": "",
+   "rev": "cae1b27ace5330f372b57f1051e228fe9b264d57",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/forked-from-1kasper/ground_zero",
-   "type": "git",
-   "subDir": null,
-   "rev": "a3122579f48dc7aa9a65be33d218249569980327",
-   "name": "GroundZero",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "katydid",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index bd59abf..e7a4f40 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.11.0-rc2