From 54ec946209c1b3aae82001e31e39b2fc1abda31c Mon Sep 17 00:00:00 2001
From: Lorenzo Luccioli <lorenzoluccioli@gmail.com>
Date: Tue, 6 Aug 2024 16:24:50 +0200
Subject: [PATCH] fix bug

---
 TestingLowerBounds/DerivAtTop.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/TestingLowerBounds/DerivAtTop.lean b/TestingLowerBounds/DerivAtTop.lean
index 60865b41..39cf73aa 100644
--- a/TestingLowerBounds/DerivAtTop.lean
+++ b/TestingLowerBounds/DerivAtTop.lean
@@ -6,7 +6,6 @@ Authors: Rémy Degenne
 import TestingLowerBounds.Convex
 import TestingLowerBounds.ForMathlib.LeftRightDeriv
 import TestingLowerBounds.ForMathlib.EReal
-import TestingLowerBounds.ForMathlib.Tendsto
 
 /-!