chore(*): remove unnecessary import tactic (#7560)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · May 10, 2021 · ac1f3df · ac1f3df
1 parent 17cba54
commit ac1f3df
Show file tree

Hide file tree

Showing 9 changed files with 6 additions and 8 deletions.
diff --git a/archive/100-theorems-list/83_friendship_graphs.lean b/archive/100-theorems-list/83_friendship_graphs.lean
@@ -8,6 +8,7 @@ import linear_algebra.char_poly.coeff
 import data.int.modeq
 import data.zmod.basic
 import tactic.interval_cases
+import tactic.omega
 
 /-!
 # The Friendship Theorem

diff --git a/src/category_theory/limits/kan_extension.lean b/src/category_theory/limits/kan_extension.lean
@@ -7,7 +7,6 @@ import category_theory.punit
 import category_theory.structured_arrow
 import category_theory.limits.functor_category
 import category_theory.limits.shapes.terminal
-import tactic
 
 /-!
 

diff --git a/src/combinatorics/colex.lean b/src/combinatorics/colex.lean
@@ -6,7 +6,6 @@ Authors: Bhavik Mehta, Alena Gusakov
 import data.finset
 import data.fintype.basic
 import algebra.geom_sum
-import tactic
 
 /-!
 # Colex

diff --git a/src/data/nat/fib.lean b/src/data/nat/fib.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
 import data.stream.basic
-import tactic
 import data.nat.gcd
+import tactic.ring
+
 /-!
 # The Fibonacci Sequence
 

diff --git a/src/data/set/constructions.lean b/src/data/set/constructions.lean
@@ -3,8 +3,6 @@ Copyright (c) 2020 Adam Topaz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
-
-import tactic
 import data.finset.basic
 
 /-!

diff --git a/src/number_theory/arithmetic_function.lean b/src/number_theory/arithmetic_function.lean
@@ -7,7 +7,7 @@ import algebra.big_operators.ring
 import number_theory.divisors
 import algebra.squarefree
 import algebra.invertible
-
+import tactic.omega
 /-!
 # Arithmetic Functions and Dirichlet Convolution
 

diff --git a/src/number_theory/divisors.lean b/src/number_theory/divisors.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import algebra.big_operators.order
-import tactic
+import data.finset.intervals
 import data.nat.prime
 
 /-!

diff --git a/src/ring_theory/polynomial/symmetric.lean b/src/ring_theory/polynomial/symmetric.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Hanting Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hanting Zhang, Johan Commelin
 -/
-import tactic
 import data.mv_polynomial.rename
 import data.mv_polynomial.comm_ring
 import algebra.algebra.subalgebra

diff --git a/src/ring_theory/witt_vector/structure_polynomial.lean b/src/ring_theory/witt_vector/structure_polynomial.lean
@@ -9,6 +9,7 @@ import field_theory.mv_polynomial
 import field_theory.finite.polynomial
 import number_theory.basic
 import ring_theory.witt_vector.witt_polynomial
+import tactic.omega
 
 /-!
 # Witt structure polynomials