diff --git a/Mathlib/Data/Fin/Tuple/Take.lean b/Mathlib/Data/Fin/Tuple/Take.lean index 1ff923b04788e..462351c63a8d1 100644 --- a/Mathlib/Data/Fin/Tuple/Take.lean +++ b/Mathlib/Data/Fin/Tuple/Take.lean @@ -3,7 +3,6 @@ Copyright (c) 2024 Quang Dao. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao -/ -import Batteries.Data.List.OfFn import Mathlib.Data.Fin.Tuple.Basic /-! diff --git a/Mathlib/Data/List/OfFn.lean b/Mathlib/Data/List/OfFn.lean index 1b5493bc76efe..61652e235bfb4 100644 --- a/Mathlib/Data/List/OfFn.lean +++ b/Mathlib/Data/List/OfFn.lean @@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Batteries.Data.List.OfFn import Mathlib.Data.Fin.Tuple.Basic /-!