From 1ce2f69bc4ff126f3b6b97bddae3bd43d0a54a9c Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 17 May 2023 17:33:59 -0400
Subject: [PATCH] feat: add Mathlib.Tactic.Common, and import

---
 Mathlib.lean                            |  1 +
 Mathlib/Algebra/Group/Defs.lean         |  1 +
 Mathlib/Algebra/Quotient.lean           |  2 +
 Mathlib/Control/Monad/Basic.lean        |  1 +
 Mathlib/Data/Option/Basic.lean          |  2 +-
 Mathlib/Data/Prod/Basic.lean            |  2 +-
 Mathlib/Data/Real/CauSeq.lean           |  2 -
 Mathlib/Data/Seq/Computation.lean       |  2 +-
 Mathlib/Data/Sum/Basic.lean             |  2 +-
 Mathlib/Data/TypeVec.lean               |  5 +-
 Mathlib/Logic/Pairwise.lean             |  1 +
 Mathlib/Logic/Relation.lean             |  4 +-
 Mathlib/Logic/Unique.lean               |  2 +-
 Mathlib/Tactic.lean                     |  1 +
 Mathlib/Tactic/Backtracking.lean        |  3 +-
 Mathlib/Tactic/Common.lean              | 98 +++++++++++++++++++++++++
 Mathlib/Testing/SlimCheck/Gen.lean      |  6 +-
 Mathlib/Testing/SlimCheck/Testable.lean |  2 -
 18 files changed, 117 insertions(+), 20 deletions(-)
 create mode 100644 Mathlib/Tactic/Common.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index dd5879345d22e..7d5a4c87f2701 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1890,6 +1890,7 @@ import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Common
 import Mathlib.Tactic.Congr!
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index bb2639412213c..880b908d31961 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -12,6 +12,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 import Mathlib.Init.ZeroOne
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Logic.Function.Basic
+import Mathlib.Tactic.Common
 
 /-!
 # Typeclasses for (semi)groups and monoids
diff --git a/Mathlib/Algebra/Quotient.lean b/Mathlib/Algebra/Quotient.lean
index 3d0dc08372589..f5f4c9de5115a 100644
--- a/Mathlib/Algebra/Quotient.lean
+++ b/Mathlib/Algebra/Quotient.lean
@@ -9,6 +9,8 @@ Authors: Anne Baanen
 ! if you have ported upstream changes.
 -/
 import Mathlib.Mathport.Rename
+import Mathlib.Tactic.Common
+
 /-!
 # Algebraic quotients
 
diff --git a/Mathlib/Control/Monad/Basic.lean b/Mathlib/Control/Monad/Basic.lean
index ab231f858e127..9774789197da0 100644
--- a/Mathlib/Control/Monad/Basic.lean
+++ b/Mathlib/Control/Monad/Basic.lean
@@ -10,6 +10,7 @@ Authors: Simon Hudon
 -/
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Control.SimpSet
+import Mathlib.Tactic.Common
 
 /-!
 # Monad
diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean
index 42e19b81c1098..8bea0b8f542a7 100644
--- a/Mathlib/Data/Option/Basic.lean
+++ b/Mathlib/Data/Option/Basic.lean
@@ -12,7 +12,7 @@ import Mathlib.Init.Control.Combinators
 import Mathlib.Data.Option.Defs
 import Mathlib.Logic.IsEmpty
 import Mathlib.Logic.Relator
-import Mathlib.Mathport.Rename
+import Mathlib.Tactic.Common
 
 /-!
 # Option of a type
diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
index 907c839fa78de..cca00fe3d49d0 100644
--- a/Mathlib/Data/Prod/Basic.lean
+++ b/Mathlib/Data/Prod/Basic.lean
@@ -12,7 +12,7 @@ import Mathlib.Init.Core
 import Mathlib.Init.Data.Prod
 import Mathlib.Init.Function
 import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Inhabit
+import Mathlib.Tactic.Common
 
 /-!
 # Extra facts about `prod`
diff --git a/Mathlib/Data/Real/CauSeq.lean b/Mathlib/Data/Real/CauSeq.lean
index d307792dcd5c3..88151e9eaf6c8 100644
--- a/Mathlib/Data/Real/CauSeq.lean
+++ b/Mathlib/Data/Real/CauSeq.lean
@@ -928,7 +928,6 @@ protected theorem sup_eq_right {a b : CauSeq α abs} (h : a ≤ b) : a ⊔ b ≈
     exact ε0.le.trans (h _ hj)
   · refine' Setoid.trans (sup_equiv_sup h (Setoid.refl _)) _
     rw [CauSeq.sup_idem]
-    exact Setoid.refl _
 #align cau_seq.sup_eq_right CauSeq.sup_eq_right
 
 protected theorem inf_eq_right {a b : CauSeq α abs} (h : b ≤ a) : a ⊓ b ≈ b := by
@@ -941,7 +940,6 @@ protected theorem inf_eq_right {a b : CauSeq α abs} (h : b ≤ a) : a ⊓ b ≈
     exact ε0.le.trans (h _ hj)
   · refine' Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) _
     rw [CauSeq.inf_idem]
-    exact Setoid.refl _
 #align cau_seq.inf_eq_right CauSeq.inf_eq_right
 
 protected theorem sup_eq_left {a b : CauSeq α abs} (h : b ≤ a) : a ⊔ b ≈ a := by
diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
index 920221e28be0d..057dbce91d4ae 100644
--- a/Mathlib/Data/Seq/Computation.lean
+++ b/Mathlib/Data/Seq/Computation.lean
@@ -11,7 +11,7 @@ Coinductive formalization of unbounded computations.
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Stream.Init
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.Common
 
 /-!
 # Coinductive formalization of unbounded computations.
diff --git a/Mathlib/Data/Sum/Basic.lean b/Mathlib/Data/Sum/Basic.lean
index 453f8d6927309..9e70c7b86f267 100644
--- a/Mathlib/Data/Sum/Basic.lean
+++ b/Mathlib/Data/Sum/Basic.lean
@@ -9,7 +9,7 @@ Authors: Mario Carneiro, Yury G. Kudryashov
 ! if you have ported upstream changes.
 -/
 import Mathlib.Logic.Function.Basic
-import Mathlib.Mathport.Rename
+import Mathlib.Tactic.Rename
 
 /-!
 # Disjoint union of types
diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean
index 0be448b81a58a..72b10c51ac820 100644
--- a/Mathlib/Data/TypeVec.lean
+++ b/Mathlib/Data/TypeVec.lean
@@ -11,10 +11,7 @@ Authors: Jeremy Avigad, Mario Carneiro, Simon Hudon
 import Mathlib.Data.Fin.Fin2
 import Mathlib.Data.TypeVec.Attr
 import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Basic
-import Mathlib.Tactic.ScopedNS
-import Mathlib.Tactic.Replace
-import Mathlib.Tactic.SolveByElim
+import Mathlib.Tactic.Common
 
 /-!
 
diff --git a/Mathlib/Logic/Pairwise.lean b/Mathlib/Logic/Pairwise.lean
index 38ed8e491de1f..7c7583278cdb5 100644
--- a/Mathlib/Logic/Pairwise.lean
+++ b/Mathlib/Logic/Pairwise.lean
@@ -11,6 +11,7 @@ Authors: Johannes Hölzl
 import Mathlib.Logic.Function.Basic
 import Mathlib.Logic.Relation
 import Mathlib.Init.Set
+import Mathlib.Tactic.Common
 
 /-!
 # Relations holding pairwise
diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index 2a5d6d0e9ae0f..96ceb7573a293 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -10,10 +10,8 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Logic.Relator
 import Mathlib.Init.Propext
-import Mathlib.Tactic.Relation.Rfl
-import Mathlib.Tactic.Use
 import Mathlib.Init.Data.Quot
-import Mathlib.Tactic.MkIffOfInductiveProp
+import Mathlib.Tactic.Common
 
 /-!
 # Relation closures
diff --git a/Mathlib/Logic/Unique.lean b/Mathlib/Logic/Unique.lean
index eecb7adcc6394..9003cfaac49a2 100644
--- a/Mathlib/Logic/Unique.lean
+++ b/Mathlib/Logic/Unique.lean
@@ -11,7 +11,7 @@ Authors: Johan Commelin
 import Mathlib.Logic.IsEmpty
 import Mathlib.Init.Logic
 import Mathlib.Init.Data.Fin.Basic
-import Mathlib.Tactic.Inhabit
+import Mathlib.Tactic.Common
 
 /-!
 # Types with a unique term
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 6ced62363cc27..5484b979caf0f 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -16,6 +16,7 @@ import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Common
 import Mathlib.Tactic.Congr!
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity
diff --git a/Mathlib/Tactic/Backtracking.lean b/Mathlib/Tactic/Backtracking.lean
index d3eac52912843..ee0f37da19f54 100644
--- a/Mathlib/Tactic/Backtracking.lean
+++ b/Mathlib/Tactic/Backtracking.lean
@@ -45,7 +45,8 @@ def Except.emoji : Except ε α → String
 returning the list of elements on which the function fails, and the list of successful results. -/
 def List.tryAllM [Monad m] [Alternative m] (L : List α) (f : α → m β) : m (List α × List β) := do
   let R ← L.mapM (fun a => (Sum.inr <$> f a) <|> (pure (Sum.inl a)))
-  return (R.filterMap Sum.getLeft, R.filterMap Sum.getRight)
+  return (R.filterMap (fun s => match s with | .inl a => a | _ => none),
+    R.filterMap (fun s => match s with | .inr b => b | _ => none))
 
 namespace Lean.MVarId
 
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
new file mode 100644
index 0000000000000..d414899e97fe1
--- /dev/null
+++ b/Mathlib/Tactic/Common.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+/-
+This file imports all tactics which do not have significant theory imports,
+and hence can be imported very low in the theory import hierarchy,
+thereby making tactics widely available without needing specific imports.
+
+We include some commented out imports here, with an explanation of their theory requirements,
+to save some time for anyone wondering why they are not here.
+-/
+
+import Mathlib.Mathport.Rename
+import Mathlib.Tactic.Alias
+import Mathlib.Tactic.ApplyCongr
+-- ApplyFun imports `Mathlib.Order.Monotone.Basic`
+-- import Mathlib.Tactic.ApplyFun
+import Mathlib.Tactic.ApplyWith
+import Mathlib.Tactic.Basic
+import Mathlib.Tactic.ByContra
+import Mathlib.Tactic.Cases
+import Mathlib.Tactic.CasesM
+import Mathlib.Tactic.Choose
+import Mathlib.Tactic.Classical
+import Mathlib.Tactic.Clear_
+import Mathlib.Tactic.Clear!
+import Mathlib.Tactic.ClearExcept
+import Mathlib.Tactic.Congr!
+import Mathlib.Tactic.Constructor
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Conv
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.DeriveToExpr
+import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Existsi
+import Mathlib.Tactic.Find
+import Mathlib.Tactic.GeneralizeProofs
+import Mathlib.Tactic.GuardGoalNums
+import Mathlib.Tactic.GuardHypNums
+import Mathlib.Tactic.Have
+import Mathlib.Tactic.HelpCmd
+import Mathlib.Tactic.HigherOrder
+import Mathlib.Tactic.InferParam
+import Mathlib.Tactic.Inhabit
+import Mathlib.Tactic.IrreducibleDef
+import Mathlib.Tactic.LabelAttr
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.LibrarySearch
+import Mathlib.Tactic.Lift
+import Mathlib.Tactic.MkIffOfInductiveProp
+-- NormCast imports `Mathlib.Algebra.Group.Defs`
+-- import Mathlib.Tactic.NormCast
+import Mathlib.Tactic.NthRewrite
+import Mathlib.Tactic.PermuteGoals
+import Mathlib.Tactic.PrintPrefix
+import Mathlib.Tactic.ProjectionNotation
+import Mathlib.Tactic.Propose
+import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Recover
+import Mathlib.Tactic.Rename
+import Mathlib.Tactic.RenameBVar
+import Mathlib.Tactic.Relation.Rfl
+import Mathlib.Tactic.Relation.Symm
+import Mathlib.Tactic.Relation.Trans
+import Mathlib.Tactic.Replace
+import Mathlib.Tactic.Rewrites
+import Mathlib.Tactic.RSuffices
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.ScopedNS
+import Mathlib.Tactic.Set
+import Mathlib.Tactic.SimpIntro
+import Mathlib.Tactic.SimpRw
+-- SlimCheck has unnecessarily complicated imports, and could be streamlined.
+-- `Gen` / `Testable` / `Sampleable` instances for types should be out in the library,
+-- rather than the theory for those types being imported into `SlimCheck`.
+-- import Mathlib.Tactic.SlimCheck
+import Mathlib.Tactic.SolveByElim
+import Mathlib.Tactic.SplitIfs
+import Mathlib.Tactic.Spread
+import Mathlib.Tactic.Substs
+import Mathlib.Tactic.SuccessIfFailWithMsg
+import Mathlib.Tactic.SudoSetOption
+import Mathlib.Tactic.SwapVar
+import Mathlib.Tactic.SplitIfs
+import Mathlib.Tactic.Tauto
+-- TFAE imports `Mathlib.Data.List.TFAE` and thence `Mathlib.Data.List.Basic`.
+-- import Mathlib.Tactic.TFAE
+import Mathlib.Tactic.ToExpr
+import Mathlib.Tactic.ToLevel
+import Mathlib.Tactic.Trace
+import Mathlib.Tactic.TryThis
+import Mathlib.Tactic.TypeCheck
+import Mathlib.Tactic.UnsetOption
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.WLOG
diff --git a/Mathlib/Testing/SlimCheck/Gen.lean b/Mathlib/Testing/SlimCheck/Gen.lean
index 223a24abc3b39..49dc291e09818 100644
--- a/Mathlib/Testing/SlimCheck/Gen.lean
+++ b/Mathlib/Testing/SlimCheck/Gen.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
 import Mathlib.Control.Random
-import Mathlib.Data.List.Perm
-import Mathlib.Data.Subtype
-import Mathlib.Data.Nat.Basic
+-- import Mathlib.Data.List.Perm
+-- import Mathlib.Data.Subtype
+-- import Mathlib.Data.Nat.Basic
 
 /-!
 # `Gen` Monad
diff --git a/Mathlib/Testing/SlimCheck/Testable.lean b/Mathlib/Testing/SlimCheck/Testable.lean
index 60342d3779e25..1db2253cf0a2c 100644
--- a/Mathlib/Testing/SlimCheck/Testable.lean
+++ b/Mathlib/Testing/SlimCheck/Testable.lean
@@ -3,8 +3,6 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
-
-import Mathlib.Data.Array.Basic
 import Mathlib.Testing.SlimCheck.Sampleable
 import Lean