remove redundant imports

server/leanserver/GameServer/Commands.lean

@@ -1,4 +1,3 @@
-import Lean
 import GameServer.EnvExtensions
 
 open Lean Meta Elab Command

server/leanserver/GameServer/EnvExtensions.lean

@@ -1,6 +1,5 @@
-import Lean
-import GameServer.Graph
 import GameServer.AbstractCtx
+import GameServer.Graph
 
 /-! # Environment extensions
 

server/leanserver/GameServer/FileWorker.lean

@@ -1,11 +1,6 @@
 /- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
-
-import Lean
-import GameServer.EnvExtensions
-import GameServer.RpcHandlers
-import GameServer.Game
-
 import Lean.Server.FileWorker
+import GameServer.Game
 
 namespace MyModule
 open Lean

server/leanserver/GameServer/Game.lean

@@ -1,8 +1,5 @@
-import Lean
-import GameServer.EnvExtensions
 import GameServer.RpcHandlers
 
-
 open Lean
 
 structure GameServerState :=

server/leanserver/GameServer/RpcHandlers.lean

@@ -1,4 +1,3 @@
-import Lean
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
 

server/leanserver/GameServer/Watchdog.lean

@@ -1,7 +1,6 @@
 /- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/
-import Lean
-import GameServer.Game
 import Lean.Server.Watchdog
+import GameServer.Game
 
 namespace MyServer.Watchdog
 open Lean

server/leanserver/Main.lean

@@ -1,6 +1,5 @@
-import GameServer.Watchdog
 import GameServer.FileWorker
-
+import GameServer.Watchdog
 
 unsafe def main : List String → IO UInt32 := fun args => do
   let e ← IO.getStderr