From bcd773cc4835f5f6f2cc56ad8c19b9a931e8ac6b Mon Sep 17 00:00:00 2001
From: tomaz1502 <tomgm1502@gmail.com>
Date: Sat, 18 Jan 2025 17:53:24 -0300
Subject: [PATCH] Fix imports on basic.lean

---
 Mathlib/Computability/QueryComplexity/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

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.