diff --git a/Mathlib/Computability/QueryComplexity/Basic.lean b/Mathlib/Computability/QueryComplexity/Basic.lean
index 24f05407df700..a5dfc1609da2e 100644
--- a/Mathlib/Computability/QueryComplexity/Basic.lean
+++ b/Mathlib/Computability/QueryComplexity/Basic.lean
@@ -6,6 +6,8 @@ Authors: Geoffrey Irving, Tomaz Mascarenhas
 import Mathlib.Computability.QueryComplexity.Defs
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Nat.Defs
+import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Tactic.Cases
 
 /-!
 ## Basic properties of `Comp` and its Monad instance.