diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
index e114914..52f43a4 100644
--- a/Lampe/Lampe.lean
+++ b/Lampe/Lampe.lean
@@ -1,3 +1,4 @@
+import Mathlib
 import Lampe.Basic
 open Lampe
 
diff --git a/Lampe/Lampe/Ast.lean b/Lampe/Lampe/Ast.lean
index a620020..8618c1b 100644
--- a/Lampe/Lampe/Ast.lean
+++ b/Lampe/Lampe/Ast.lean
@@ -1,5 +1,3 @@
-import Mathlib
-
 import Lampe.Tp
 import Lampe.Data.HList
 import Lampe.SeparationLogic.ValHeap
diff --git a/Lampe/Lampe/Builtin/Basic.lean b/Lampe/Lampe/Builtin/Basic.lean
index 973e3eb..d6a42c5 100644
--- a/Lampe/Lampe/Builtin/Basic.lean
+++ b/Lampe/Lampe/Builtin/Basic.lean
@@ -2,7 +2,7 @@ import Lampe.SeparationLogic.ValHeap
 import Lampe.Data.Field
 import Lampe.Data.HList
 import Lampe.Builtin.Helpers
-import Mathlib
+import Mathlib.Tactic.Lemma
 
 lemma List.replicate_head (hl : x :: xs = List.replicate n a) : x = a := by
   unfold List.replicate at hl
diff --git a/Lampe/Lampe/Builtin/Helpers.lean b/Lampe/Lampe/Builtin/Helpers.lean
index b83f126..5f0a110 100644
--- a/Lampe/Lampe/Builtin/Helpers.lean
+++ b/Lampe/Lampe/Builtin/Helpers.lean
@@ -1,4 +1,4 @@
-import Mathlib
+import Mathlib.Tactic.Linarith
 
 namespace Lampe
 
diff --git a/Lampe/Lampe/Builtin/Slice.lean b/Lampe/Lampe/Builtin/Slice.lean
index f18d8ba..90b736f 100644
--- a/Lampe/Lampe/Builtin/Slice.lean
+++ b/Lampe/Lampe/Builtin/Slice.lean
@@ -7,7 +7,7 @@ def replaceSlice' (s : Tp.denote p $ .slice tp) (i : Fin s.length) (v : Tp.denot
   List.modifyNth (fun _ => v) i s
 
 @[simp]
-lemma replaceSlice_length_eq_length :
+theorem replaceSlice_length_eq_length :
     (replaceSlice' s i v).length = s.length := by
   simp_all [List.length_modifyNth]
 
diff --git a/Lampe/Lampe/Builtin/Struct.lean b/Lampe/Lampe/Builtin/Struct.lean
index 21879e2..bad4c69 100644
--- a/Lampe/Lampe/Builtin/Struct.lean
+++ b/Lampe/Lampe/Builtin/Struct.lean
@@ -1,3 +1,5 @@
+import Mathlib.Algebra.PUnitInstances.Algebra -- TODO: This import is necessary for the
+                                              -- `CommRing Unit` instance, but shouldn't be needed
 import Lampe.Builtin.Basic
 
 namespace Lampe.Builtin
diff --git a/Lampe/Lampe/Data/Field.lean b/Lampe/Lampe/Data/Field.lean
index 70ad203..0097989 100644
--- a/Lampe/Lampe/Data/Field.lean
+++ b/Lampe/Lampe/Data/Field.lean
@@ -1,4 +1,4 @@
-import Mathlib
+import Mathlib.Algebra.Algebra.ZMod
 import Lampe.Data.Integers
 
 namespace Lampe
diff --git a/Lampe/Lampe/Data/Integers.lean b/Lampe/Lampe/Data/Integers.lean
index 8c3a11c..0e2e246 100644
--- a/Lampe/Lampe/Data/Integers.lean
+++ b/Lampe/Lampe/Data/Integers.lean
@@ -1,5 +1,3 @@
-import Mathlib
-
 namespace Lampe
 
 abbrev U (n : Nat) := BitVec (n)
diff --git a/Lampe/Lampe/Semantics.lean b/Lampe/Lampe/Semantics.lean
index 25b2e33..69586bb 100644
--- a/Lampe/Lampe/Semantics.lean
+++ b/Lampe/Lampe/Semantics.lean
@@ -1,5 +1,3 @@
-import Mathlib
-
 import Lampe.Ast
 import Lampe.Tp
 import Lampe.Data.Field
diff --git a/Lampe/Lampe/SeparationLogic/LawfulHeap.lean b/Lampe/Lampe/SeparationLogic/LawfulHeap.lean
index a1f2ff1..43e3820 100644
--- a/Lampe/Lampe/SeparationLogic/LawfulHeap.lean
+++ b/Lampe/Lampe/SeparationLogic/LawfulHeap.lean
@@ -1,5 +1,3 @@
-import Lampe.Tp
-
 namespace Lampe
 
 class LawfulHeap (α : Type _) where
diff --git a/Lampe/Lampe/SeparationLogic/SLP.lean b/Lampe/Lampe/SeparationLogic/SLP.lean
index 041f9c6..dd92851 100644
--- a/Lampe/Lampe/SeparationLogic/SLP.lean
+++ b/Lampe/Lampe/SeparationLogic/SLP.lean
@@ -1,3 +1,6 @@
+import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.Use
+import Lampe.Data.Field
 import Lampe.Tactic.IntroCases
 import Lampe.SeparationLogic.LawfulHeap
 
diff --git a/Lampe/Lampe/SeparationLogic/ValHeap.lean b/Lampe/Lampe/SeparationLogic/ValHeap.lean
index 3ffe117..2e0b3e2 100644
--- a/Lampe/Lampe/SeparationLogic/ValHeap.lean
+++ b/Lampe/Lampe/SeparationLogic/ValHeap.lean
@@ -1,5 +1,7 @@
+import Mathlib.Data.Finmap
 import Lampe.SeparationLogic.LawfulHeap
 import Lampe.SeparationLogic.SLP
+import Lampe.Tp
 
 lemma Finmap.insert_eq_singleton_union [DecidableEq α] {ref : α}:
     m.insert ref v = Finmap.singleton ref v ∪ m := by rfl
diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
index bd2f887..3d0e04d 100644
--- a/Lampe/Lampe/Syntax.lean
+++ b/Lampe/Lampe/Syntax.lean
@@ -1,8 +1,7 @@
-import Mathlib
 import Lean
-import Lampe.Ast
 import Qq
 
+import Lampe.Ast
 import Lampe.Builtin.Arith
 import Lampe.Builtin.Array
 import Lampe.Builtin.BigInt
diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean
index f9bf922..81a9f57 100644
--- a/Lampe/Lampe/Tp.lean
+++ b/Lampe/Lampe/Tp.lean
@@ -1,5 +1,3 @@
-import Mathlib
-
 import Lampe.Data.Integers
 import Lampe.Data.Field
 import Lampe.Data.HList