Fix imports on basic.lean

leanprover-community · Jan 18, 2025 · bcd773c · bcd773c
1 parent 9ebea56
commit bcd773c
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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.