Shake

leanprover-community · Nov 7, 2024 · df54835 · df54835
1 parent e2c514e
commit df54835
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Mathlib/Order/Interval/Set/Infinite.lean b/Mathlib/Order/Interval/Set/Infinite.lean
@@ -3,7 +3,8 @@ Copyright (c) 2020 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton
 -/
-import Mathlib.Data.Set.Finite.Lemmas
+import Mathlib.Data.Set.Finite.Basic
+import Mathlib.Order.Interval.Set.Basic
 
 /-!
 # Infinitude of intervals