feat: add Mathlib.Tactic.Common, and import

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

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

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
 

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

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

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`

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

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.

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

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
 
 /-!
 

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

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

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

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

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
 

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

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

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