Import Mathlib.Tactic everywhere

MIL/C02_Basics/Source_S01_Calculating.lean

@@ -32,6 +32,7 @@ Let's try out ``rw``.
 TEXT. -/
 -- An example.
 -- QUOTE:
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 example (a b c : ℝ) : a * b * c = b * (a * c) := by

MIL/C02_Basics/Source_S04_More_on_Order_and_Divisibility.lean

@@ -1,4 +1,5 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 namespace C02S04

MIL/C02_Basics/Source_S05_Proving_Facts_about_Algebraic_Structures.lean

@@ -1,4 +1,5 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Topology.MetricSpace.Basic
 
 /- TEXT:

MIL/C03_Logic/Source_S01_Implication_and_the_Universal_Quantifier.lean

@@ -1,4 +1,5 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 namespace C03S01

MIL/C03_Logic/Source_S02_The_Existential_Quantifier.lean

@@ -1,4 +1,5 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 namespace C03S02

MIL/C03_Logic/Source_S03_Negation.lean

@@ -1,4 +1,5 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 namespace C03S03

MIL/C03_Logic/Source_S04_Conjunction_and_Bi-implication.lean

@@ -1,7 +1,7 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Nat.Prime
-import Mathlib.Tactic.NormNum
 
 namespace C03S04
 /- TEXT:

MIL/C03_Logic/Source_S05_Disjunction.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 namespace C03S05

MIL/C03_Logic/Source_S06_Sequences_and_Convergence.lean

@@ -1,4 +1,5 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 namespace C03S06

MIL/C04_Sets_and_Functions/Source_S02_Functions.lean

@@ -1,4 +1,5 @@
 -- BOTH:
+import Mathlib.Tactic
 import Mathlib.Data.Set.Lattice
 import Mathlib.Data.Set.Function
 import Mathlib.Analysis.SpecialFunctions.Log.Basic

MIL/C05_Number_Theory/Source_S01_Irrational_Roots.lean

@@ -1,7 +1,6 @@
+import Mathlib.Tactic
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Data.Nat.Prime
-import Mathlib.Tactic.NormNum.GCD
-import Mathlib.Tactic.NormNum.Prime
 /- OMIT:
 -- fix this.
 -- import Mathlib.Data.Real.Irrational

MIL/C05_Number_Theory/Source_S03_Infinitely_Many_Primes.lean

@@ -1,7 +1,6 @@
 import Mathlib.Data.Nat.Prime
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Tactic
-import Mathlib.Tactic.IntervalCases
 
 open BigOperators
 

MIL/C06_Structures/Source_S01_Structures.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Data.Real.Basic
 

MIL/C06_Structures/Source_S02_Algebraic_Structures.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 
 namespace C06S02

MIL/C07_Hierarchies/Source_S01_Basics.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Data.Real.Basic
 

MIL/C07_Hierarchies/Source_S02_Morphisms.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Topology.Instances.Real
 
 /- TEXT:

MIL/C07_Hierarchies/Source_S03_Subobjects.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.GroupTheory.QuotientGroup
 
 

MIL/C08_Topology/Source_S01_Filters.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Topology.Instances.Real
 
 open Set Filter Topology

MIL/C08_Topology/Source_S02_Metric_Spaces.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Topology.Instances.Real
 import Mathlib.Analysis.NormedSpace.BanachSteinhaus
 

MIL/C08_Topology/Source_S03_Topological_Spaces.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Topology.Instances.Real
 import Mathlib.Analysis.NormedSpace.BanachSteinhaus
 

MIL/C09_Differential_Calculus/Source_S01_Elementary_Differential_Calculus.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.Analysis.Calculus.MeanValue
 

MIL/C09_Differential_Calculus/Source_S02_Differential_Calculus_in_Normed_Spaces.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Analysis.NormedSpace.BanachSteinhaus
 import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.Calculus.Inverse

MIL/C10_Integration_and_Measure_Theory/Source_S01_Elementary_Integration.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.Convolution

MIL/C10_Integration_and_Measure_Theory/Source_S02_Measure_Theory.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.Convolution
 import Mathlib.MeasureTheory.Function.Jacobian

MIL/C10_Integration_and_Measure_Theory/Source_S03_Integration.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic
 import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.Convolution
 import Mathlib.MeasureTheory.Function.Jacobian

check_import.py

@@ -0,0 +1,8 @@
+"""
+Print the list of lean files in the MIL folder that do not import Mathlib.Tactic
+"""
+from pathlib import Path
+
+for path in (Path(__file__).parent/"MIL").glob("**/*.lean"):
+    if not any([l == "import Mathlib.Tactic" for l in path.read_text().split("\n")]):
+        print(path)