From ff097e952f7cee75608d4097c3e825a1f650ffe7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 6 Mar 2022 12:20:09 +0100
Subject: [PATCH] chore: link orphan file

---
 src/Init.lean                             | 1 +
 src/Lean/Meta/Tactic/LinearArith/Nat.lean | 1 +
 2 files changed, 2 insertions(+)

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