making tactics widely available

Stream: mathlib4

[Johan Commelin]

Is this our prefered way to make tactics widely available? Or should we just import Mathlib.Tactic.Common at some point?

$ head -20 Mathlib/Logic/Equiv/Basic.lean
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
import Mathlib.Data.Bool.Basic
import Mathlib.Data.Option.Defs
import Mathlib.Data.Prod.Basic
import Mathlib.Data.Sigma.Basic
import Mathlib.Data.Subtype
import Mathlib.Data.Sum.Basic
import Mathlib.Logic.Equiv.Defs
import Mathlib.Logic.Function.Conjugate
import Mathlib.Tactic.Coe
import Mathlib.Tactic.Lift
import Mathlib.Tactic.Convert
import Mathlib.Tactic.Contrapose
import Mathlib.Tactic.GeneralizeProofs
import Mathlib.Tactic.SimpRw
import Mathlib.Tactic.CC