diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index 7e8aece65..702824717 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -1,5 +1,5 @@
-import Lean
-import Mathlib.Tactic.Linarith -- Introduces a lot of useful lemmas
+import Mathlib.Algebra.Order.Ring.Int
+import Mathlib.Data.Nat.Cast.Order.Ring
 
 namespace Arith
 
diff --git a/backends/lean/Base/Arith/Init.lean b/backends/lean/Base/Arith/Init.lean
index dcf9924de..b0afd3049 100644
--- a/backends/lean/Base/Arith/Init.lean
+++ b/backends/lean/Base/Arith/Init.lean
@@ -1,5 +1,4 @@
 import Base.Extensions
-import Aesop
 open Lean
 
 /-!
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index b041c3fb9..4b785d895 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -1,13 +1,8 @@
 /- This file contains tactics to solve arithmetic goals -/
 
-import Lean
-import Lean.Meta.Tactic.Simp
-import Init.Data.List.Basic
-import Mathlib.Tactic.Ring.RingNF
-import Base.Utils
-import Base.Arith.Base
 import Base.Arith.Init
-import Base.Saturate
+import Base.Saturate.Tactic
+import Mathlib.Util.CountHeartbeats
 
 namespace Arith
 
diff --git a/backends/lean/Base/Arith/ScalarNF.lean b/backends/lean/Base/Arith/ScalarNF.lean
index 59f264958..3fe5e62bb 100644
--- a/backends/lean/Base/Arith/ScalarNF.lean
+++ b/backends/lean/Base/Arith/ScalarNF.lean
@@ -1,4 +1,5 @@
 import Base.Arith.Scalar
+import Mathlib.Tactic.Ring.RingNF
 
 namespace Arith
 
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 8803f3d8e..f69dc36a5 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -1,5 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
+import Mathlib.Tactic.Zify
 import Init.Data.List.Basic
 import Base.Primitives.Base
 import Base.Arith.Base
diff --git a/backends/lean/Base/Extensions.lean b/backends/lean/Base/Extensions.lean
index 8093ff183..792c29aa0 100644
--- a/backends/lean/Base/Extensions.lean
+++ b/backends/lean/Base/Extensions.lean
@@ -1,9 +1,5 @@
-import Lean
 import Base.Utils
-import Base.Primitives.Base
-
-import Lean.Meta.DiscrTree
-import Lean.Meta.Tactic.Simp
+import Lean.Elab.Tactic.Rewrites
 
 /-! Various state extensions used in the library -/
 namespace Extensions