From e29faaaded73bcdd79637ef1ca833b2de6c346f3 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 9 Dec 2025 22:57:54 +0100
Subject: [PATCH] perf: prune imports in Try.Collect

This PR removed unused imports from Try.Collect
---
 src/Lean/Meta/Tactic/Try/Collect.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Try/Collect.lean b/src/Lean/Meta/Tactic/Try/Collect.lean
index ae83149cd1b6..481e7d998daf 100644
--- a/src/Lean/Meta/Tactic/Try/Collect.lean
+++ b/src/Lean/Meta/Tactic/Try/Collect.lean
@@ -7,8 +7,6 @@ module
 prelude
 public import Init.Try
 public import Lean.Meta.Tactic.LibrarySearch
-public import Lean.Meta.Tactic.Grind.Cases
-public import Lean.Meta.Tactic.Grind.EMatchTheorem
 public import Lean.Meta.Tactic.FunIndCollect
 import Lean.Meta.Eqns
 public section