Tactic.lean

module  -- shake: keep-all

public import Mathlib.Tactic.Abel
public import Mathlib.Tactic.AdaptationNote
public import Mathlib.Tactic.Algebraize
public import Mathlib.Tactic.ApplyAt
public import Mathlib.Tactic.ApplyCongr
public import Mathlib.Tactic.ApplyFun
public import Mathlib.Tactic.ApplyWith
public import Mathlib.Tactic.ArithMult
public import Mathlib.Tactic.ArithMult.Init
public import Mathlib.Tactic.Attr.Core
public import Mathlib.Tactic.Attr.Register
public import Mathlib.Tactic.Basic
public import Mathlib.Tactic.Bound
public import Mathlib.Tactic.Bound.Attribute
public import Mathlib.Tactic.Bound.Init
public import Mathlib.Tactic.ByCases
public import Mathlib.Tactic.ByContra
public import Mathlib.Tactic.CancelDenoms
public import Mathlib.Tactic.CancelDenoms.Core
public import Mathlib.Tactic.Cases
public import Mathlib.Tactic.CasesM
public import Mathlib.Tactic.CategoryTheory.BicategoricalComp
public import Mathlib.Tactic.CategoryTheory.Bicategory.Basic
public import Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
public import Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
public import Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
public import Mathlib.Tactic.CategoryTheory.BicategoryCoherence
public import Mathlib.Tactic.CategoryTheory.CancelIso
public import Mathlib.Tactic.CategoryTheory.CategoryStar
public import Mathlib.Tactic.CategoryTheory.CheckCompositions
public import Mathlib.Tactic.CategoryTheory.Coherence
public import Mathlib.Tactic.CategoryTheory.Coherence.Basic
public import Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
public import Mathlib.Tactic.CategoryTheory.Coherence.Normalize
public import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
public import Mathlib.Tactic.CategoryTheory.Elementwise
public import Mathlib.Tactic.CategoryTheory.IsoReassoc
public import Mathlib.Tactic.CategoryTheory.Monoidal.Basic
public import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
public import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
public import Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
public import Mathlib.Tactic.CategoryTheory.MonoidalComp
public import Mathlib.Tactic.CategoryTheory.Reassoc
public import Mathlib.Tactic.CategoryTheory.Slice
public import Mathlib.Tactic.CategoryTheory.ToApp
public import Mathlib.Tactic.Change
public import Mathlib.Tactic.Check
public import Mathlib.Tactic.Choose
public import Mathlib.Tactic.Clean
public import Mathlib.Tactic.ClearExcept
public import Mathlib.Tactic.ClearExclamation
public import Mathlib.Tactic.Clear_
public import Mathlib.Tactic.Coe
public import Mathlib.Tactic.Common
public import Mathlib.Tactic.ComputeAsymptotics.Lemmas
public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
public import Mathlib.Tactic.ComputeDegree
public import Mathlib.Tactic.CongrExclamation
public import Mathlib.Tactic.CongrM
public import Mathlib.Tactic.Constructor
public import Mathlib.Tactic.Continuity
public import Mathlib.Tactic.Continuity.Init
public import Mathlib.Tactic.ContinuousFunctionalCalculus
public import Mathlib.Tactic.Contrapose
public import Mathlib.Tactic.Conv
public import Mathlib.Tactic.Convert
public import Mathlib.Tactic.Core
public import Mathlib.Tactic.DSimpPercent
public import Mathlib.Tactic.DeclarationNames
public import Mathlib.Tactic.DefEqAbuse
public import Mathlib.Tactic.DefEqTransformations
public import Mathlib.Tactic.DepRewrite
public import Mathlib.Tactic.DeprecateTo
public import Mathlib.Tactic.DeriveCountable
public import Mathlib.Tactic.DeriveEncodable
public import Mathlib.Tactic.DeriveFintype
public import Mathlib.Tactic.DeriveTraversable
public import Mathlib.Tactic.ENatToNat
public import Mathlib.Tactic.Eqns
public import Mathlib.Tactic.ErwQuestion
public import Mathlib.Tactic.Eval
public import Mathlib.Tactic.ExistsI
public import Mathlib.Tactic.Explode
public import Mathlib.Tactic.Explode.Datatypes
public import Mathlib.Tactic.Explode.Pretty
public import Mathlib.Tactic.Ext
public import Mathlib.Tactic.ExtendDoc
public import Mathlib.Tactic.ExtractGoal
public import Mathlib.Tactic.FBinop
public import Mathlib.Tactic.FailIfNoProgress
public import Mathlib.Tactic.FastInstance
public import Mathlib.Tactic.Field
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.FieldSimp.Attr
public import Mathlib.Tactic.FieldSimp.Discharger
public import Mathlib.Tactic.FieldSimp.Lemmas
public import Mathlib.Tactic.FinCases
public import Mathlib.Tactic.Find
public import Mathlib.Tactic.FindSyntax
public import Mathlib.Tactic.Finiteness
public import Mathlib.Tactic.Finiteness.Attr
public import Mathlib.Tactic.FunProp
public import Mathlib.Tactic.FunProp.Attr
public import Mathlib.Tactic.FunProp.Core
public import Mathlib.Tactic.FunProp.Decl
public import Mathlib.Tactic.FunProp.Elab
public import Mathlib.Tactic.FunProp.FunctionData
public import Mathlib.Tactic.FunProp.Mor
public import Mathlib.Tactic.FunProp.Theorems
public import Mathlib.Tactic.FunProp.ToBatteries
public import Mathlib.Tactic.FunProp.Types
public import Mathlib.Tactic.GCongr
public import Mathlib.Tactic.GCongr.Core
public import Mathlib.Tactic.GCongr.CoreAttrs
public import Mathlib.Tactic.GCongr.ForwardAttr
public import Mathlib.Tactic.GRewrite
public import Mathlib.Tactic.GRewrite.Core
public import Mathlib.Tactic.GRewrite.Elab
public import Mathlib.Tactic.Generalize
public import Mathlib.Tactic.GeneralizeProofs
public import Mathlib.Tactic.Group
public import Mathlib.Tactic.GuardGoalNums
public import Mathlib.Tactic.GuardHypNums
public import Mathlib.Tactic.Have
public import Mathlib.Tactic.HaveI
public import Mathlib.Tactic.HigherOrder
public import Mathlib.Tactic.Hint
public import Mathlib.Tactic.ITauto
public import Mathlib.Tactic.InferParam
public import Mathlib.Tactic.Inhabit
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.IrreducibleDef
public import Mathlib.Tactic.Lemma
public import Mathlib.Tactic.Lift
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Datatypes
public import Mathlib.Tactic.Linarith.Frontend
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.Linarith.NNRealPreprocessor
public import Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
public import Mathlib.Tactic.Linarith.Parsing
public import Mathlib.Tactic.Linarith.Preprocessing
public import Mathlib.Tactic.Linarith.Verification
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination'
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.Linter
public import Mathlib.Tactic.Linter.CommandRanges
public import Mathlib.Tactic.Linter.CommandStart
public import Mathlib.Tactic.Linter.DeprecatedModule
public import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
public import Mathlib.Tactic.Linter.DirectoryDependency
public import Mathlib.Tactic.Linter.DocPrime
public import Mathlib.Tactic.Linter.DocString
public import Mathlib.Tactic.Linter.EmptyLine
public import Mathlib.Tactic.Linter.FindDeprecations
public import Mathlib.Tactic.Linter.FlexibleLinter
public import Mathlib.Tactic.Linter.GlobalAttributeIn
public import Mathlib.Tactic.Linter.HashCommandLinter
public import Mathlib.Tactic.Linter.HaveLetLinter
public import Mathlib.Tactic.Linter.Header
public import Mathlib.Tactic.Linter.Lint
public import Mathlib.Tactic.Linter.MinImports
public import Mathlib.Tactic.Linter.Multigoal
public import Mathlib.Tactic.Linter.OldObtain
public import Mathlib.Tactic.Linter.PPRoundtrip
public import Mathlib.Tactic.Linter.PrivateModule
public import Mathlib.Tactic.Linter.Style
public import Mathlib.Tactic.Linter.TacticDocumentation
public import Mathlib.Tactic.Linter.TextBased
public import Mathlib.Tactic.Linter.TextBased.UnicodeLinter
public import Mathlib.Tactic.Linter.UnusedInstancesInType
public import Mathlib.Tactic.Linter.UnusedTactic
public import Mathlib.Tactic.Linter.UnusedTacticExtension
public import Mathlib.Tactic.Linter.UpstreamableDecl
public import Mathlib.Tactic.Linter.ValidatePRTitle
public import Mathlib.Tactic.Linter.Whitespace
public import Mathlib.Tactic.Measurability
public import Mathlib.Tactic.Measurability.Init
public import Mathlib.Tactic.MinImports
public import Mathlib.Tactic.MkIffOfInductiveProp
public import Mathlib.Tactic.ModCases
public import Mathlib.Tactic.Module
public import Mathlib.Tactic.Monotonicity
public import Mathlib.Tactic.Monotonicity.Attr
public import Mathlib.Tactic.Monotonicity.Basic
public import Mathlib.Tactic.Monotonicity.Lemmas
public import Mathlib.Tactic.MoveAdd
public import Mathlib.Tactic.NoncommRing
public import Mathlib.Tactic.Nontriviality
public import Mathlib.Tactic.Nontriviality.Core
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.Abs
public import Mathlib.Tactic.NormNum.Basic
public import Mathlib.Tactic.NormNum.BigOperators
public import Mathlib.Tactic.NormNum.Core
public import Mathlib.Tactic.NormNum.DivMod
public import Mathlib.Tactic.NormNum.Eq
public import Mathlib.Tactic.NormNum.GCD
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.NormNum.Inv
public import Mathlib.Tactic.NormNum.Irrational
public import Mathlib.Tactic.NormNum.IsCoprime
public import Mathlib.Tactic.NormNum.IsSquare
public import Mathlib.Tactic.NormNum.LegendreSymbol
public import Mathlib.Tactic.NormNum.ModEq
public import Mathlib.Tactic.NormNum.NatFactorial
public import Mathlib.Tactic.NormNum.NatFib
public import Mathlib.Tactic.NormNum.NatLog
public import Mathlib.Tactic.NormNum.NatSqrt
public import Mathlib.Tactic.NormNum.OfScientific
public import Mathlib.Tactic.NormNum.Ordinal
public import Mathlib.Tactic.NormNum.Parity
public import Mathlib.Tactic.NormNum.Pow
public import Mathlib.Tactic.NormNum.PowMod
public import Mathlib.Tactic.NormNum.Prime
public import Mathlib.Tactic.NormNum.RealSqrt
public import Mathlib.Tactic.NormNum.Result
public import Mathlib.Tactic.NthRewrite
public import Mathlib.Tactic.Observe
public import Mathlib.Tactic.OfNat
public import Mathlib.Tactic.Order
public import Mathlib.Tactic.Order.CollectFacts
public import Mathlib.Tactic.Order.Graph.Basic
public import Mathlib.Tactic.Order.Graph.Tarjan
public import Mathlib.Tactic.Order.Preprocessing
public import Mathlib.Tactic.Order.ToInt
public import Mathlib.Tactic.PNatToNat
public import Mathlib.Tactic.PPWithUniv
public import Mathlib.Tactic.Peel
public import Mathlib.Tactic.Polyrith
public import Mathlib.Tactic.Positivity
public import Mathlib.Tactic.Positivity.Basic
public import Mathlib.Tactic.Positivity.Core
public import Mathlib.Tactic.Positivity.Finset
public import Mathlib.Tactic.ProdAssoc
public import Mathlib.Tactic.Propose
public import Mathlib.Tactic.ProxyType
public import Mathlib.Tactic.Push
public import Mathlib.Tactic.Push.Attr
public import Mathlib.Tactic.Qify
public import Mathlib.Tactic.RSuffices
public import Mathlib.Tactic.Recall
public import Mathlib.Tactic.Recover
public import Mathlib.Tactic.ReduceModChar
public import Mathlib.Tactic.ReduceModChar.Ext
public import Mathlib.Tactic.Relation.Rfl
public import Mathlib.Tactic.Relation.Symm
public import Mathlib.Tactic.Rename
public import Mathlib.Tactic.RenameBVar
public import Mathlib.Tactic.Replace
public import Mathlib.Tactic.RewriteSearch
public import Mathlib.Tactic.Rify
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic
public import Mathlib.Tactic.Ring.Common
public import Mathlib.Tactic.Ring.Compare
public import Mathlib.Tactic.Ring.NamePolyVars
public import Mathlib.Tactic.Ring.PNat
public import Mathlib.Tactic.Ring.RingNF
public import Mathlib.Tactic.Sat.FromLRAT
public import Mathlib.Tactic.Says
public import Mathlib.Tactic.ScopedNS
public import Mathlib.Tactic.Set
public import Mathlib.Tactic.SetLike
public import Mathlib.Tactic.SimpIntro
public import Mathlib.Tactic.SimpRw
public import Mathlib.Tactic.Simproc.Divisors
public import Mathlib.Tactic.Simproc.ExistsAndEq
public import Mathlib.Tactic.Simproc.Factors
public import Mathlib.Tactic.Simproc.FinsetInterval
public import Mathlib.Tactic.Simps.Basic
public import Mathlib.Tactic.Simps.NotationClass
public import Mathlib.Tactic.SplitIfs
public import Mathlib.Tactic.Spread
public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Tactic.Subsingleton
public import Mathlib.Tactic.Substs
public import Mathlib.Tactic.SuccessIfFailWithMsg
public import Mathlib.Tactic.SudoSetOption
public import Mathlib.Tactic.SuppressCompilation
public import Mathlib.Tactic.SwapVar
public import Mathlib.Tactic.TFAE
public import Mathlib.Tactic.TacticAnalysis
public import Mathlib.Tactic.TacticAnalysis.Declarations
public import Mathlib.Tactic.Tauto
public import Mathlib.Tactic.TautoSet
public import Mathlib.Tactic.TermCongr
public import Mathlib.Tactic.ToAdditive
public import Mathlib.Tactic.ToDual
public import Mathlib.Tactic.ToExpr
public import Mathlib.Tactic.ToFun
public import Mathlib.Tactic.ToLevel
public import Mathlib.Tactic.Trace
public import Mathlib.Tactic.Translate.Core
public import Mathlib.Tactic.Translate.GuessName
public import Mathlib.Tactic.Translate.TagUnfoldBoundary
public import Mathlib.Tactic.Translate.ToAdditive
public import Mathlib.Tactic.Translate.ToDual
public import Mathlib.Tactic.Translate.UnfoldBoundary
public import Mathlib.Tactic.TryThis
public import Mathlib.Tactic.TypeCheck
public import Mathlib.Tactic.TypeStar
public import Mathlib.Tactic.UnsetOption
public import Mathlib.Tactic.Use
public import Mathlib.Tactic.Variable
public import Mathlib.Tactic.WLOG
public import Mathlib.Tactic.Widget.Calc
public import Mathlib.Tactic.Widget.CommDiag
public import Mathlib.Tactic.Widget.CongrM
public import Mathlib.Tactic.Widget.Conv
public import Mathlib.Tactic.Widget.GCongr
public import Mathlib.Tactic.Widget.InteractiveUnfold
public import Mathlib.Tactic.Widget.LibraryRewrite
public import Mathlib.Tactic.Widget.SelectInsertParamsClass
public import Mathlib.Tactic.Widget.SelectPanelUtils
public import Mathlib.Tactic.Widget.StringDiagram
public import Mathlib.Tactic.WithoutCDot
public import Mathlib.Tactic.Zify