diff --git a/src/Init.lean b/src/Init.lean
index 122d982a55..0fd45ba040 100644
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -20,3 +20,4 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
+import Init.SizeOfLemmas
diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat.lean b/src/Lean/Meta/Tactic/LinearArith/Nat.lean
index db47abddd1..a31bdc1732 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Nat.lean
+++ b/src/Lean/Meta/Tactic/LinearArith/Nat.lean
@@ -5,3 +5,4 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.LinearArith.Nat.Basic
 import Lean.Meta.Tactic.LinearArith.Nat.Simp
+import Lean.Meta.Tactic.LinearArith.Nat.Solver