Cleanup mathlib imports in Lampe

Lampe/Lampe.lean

@@ -1,3 +1,4 @@
+import Mathlib
 import Lampe.Basic
 open Lampe
 

Lampe/Lampe/Ast.lean

@@ -1,5 +1,3 @@
-import Mathlib
-
 import Lampe.Tp
 import Lampe.Data.HList
 import Lampe.SeparationLogic.ValHeap

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

Lampe/Lampe/Builtin/Helpers.lean

@@ -1,4 +1,4 @@
-import Mathlib
+import Mathlib.Tactic.Linarith
 
 namespace Lampe
 

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]
 

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

Lampe/Lampe/Data/Field.lean

@@ -1,4 +1,4 @@
-import Mathlib
+import Mathlib.Algebra.Algebra.ZMod
 import Lampe.Data.Integers
 
 namespace Lampe

Lampe/Lampe/Data/Integers.lean

@@ -1,5 +1,3 @@
-import Mathlib
-
 namespace Lampe
 
 abbrev U (n : Nat) := BitVec (n)

Lampe/Lampe/Semantics.lean

@@ -1,5 +1,3 @@
-import Mathlib
-
 import Lampe.Ast
 import Lampe.Tp
 import Lampe.Data.Field

Lampe/Lampe/SeparationLogic/LawfulHeap.lean

@@ -1,5 +1,3 @@
-import Lampe.Tp
-
 namespace Lampe
 
 class LawfulHeap (α : Type _) where

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
 

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

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

Lampe/Lampe/Tp.lean

@@ -1,5 +1,3 @@
-import Mathlib
-
 import Lampe.Data.Integers
 import Lampe.Data.Field
 import Lampe.Data.HList