Documentation
Mathlib
.
Tactic
Search
return to top
source
Imports
Init
Mathlib.Tactic.Abel
Mathlib.Tactic.AdaptationNote
Mathlib.Tactic.AddGroup
Mathlib.Tactic.Algebraize
Mathlib.Tactic.ApplyAt
Mathlib.Tactic.ApplyCongr
Mathlib.Tactic.ApplyFun
Mathlib.Tactic.ApplyWith
Mathlib.Tactic.ArithMult
Mathlib.Tactic.Assume
Mathlib.Tactic.BDSimp
Mathlib.Tactic.Basic
Mathlib.Tactic.Bound
Mathlib.Tactic.ByCases
Mathlib.Tactic.ByContra
Mathlib.Tactic.CancelDenoms
Mathlib.Tactic.Cases
Mathlib.Tactic.CasesM
Mathlib.Tactic.Change
Mathlib.Tactic.Check
Mathlib.Tactic.Choose
Mathlib.Tactic.Clean
Mathlib.Tactic.ClearExcept
Mathlib.Tactic.ClearExclamation
Mathlib.Tactic.Clear_
Mathlib.Tactic.ClickSuggestions
Mathlib.Tactic.Coe
Mathlib.Tactic.Common
Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.CongrExclamation
Mathlib.Tactic.CongrM
Mathlib.Tactic.Constructor
Mathlib.Tactic.Continuity
Mathlib.Tactic.ContinuousFunctionalCalculus
Mathlib.Tactic.Contrapose
Mathlib.Tactic.Conv
Mathlib.Tactic.Convert
Mathlib.Tactic.Core
Mathlib.Tactic.CrossRefAttribute
Mathlib.Tactic.DSimpPercent
Mathlib.Tactic.DeclarationNames
Mathlib.Tactic.DefEqAbuse
Mathlib.Tactic.DefEqTransformations
Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DeprecateTo
Mathlib.Tactic.DeriveCountable
Mathlib.Tactic.DeriveEncodable
Mathlib.Tactic.DeriveFintype
Mathlib.Tactic.DeriveTraversable
Mathlib.Tactic.DuplicateDecls
Mathlib.Tactic.ENatToNat
Mathlib.Tactic.Eqns
Mathlib.Tactic.ErwQuestion
Mathlib.Tactic.Eval
Mathlib.Tactic.ExistsI
Mathlib.Tactic.Explode
Mathlib.Tactic.Ext
Mathlib.Tactic.ExtendDoc
Mathlib.Tactic.ExtractGoal
Mathlib.Tactic.FBinop
Mathlib.Tactic.FailIfNoProgress
Mathlib.Tactic.FastInstance
Mathlib.Tactic.Field
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FinCases
Mathlib.Tactic.Find
Mathlib.Tactic.FindSyntax
Mathlib.Tactic.Finiteness
Mathlib.Tactic.FunProp
Mathlib.Tactic.GCongr
Mathlib.Tactic.GRewrite
Mathlib.Tactic.Generalize
Mathlib.Tactic.GrindAttrs
Mathlib.Tactic.Group
Mathlib.Tactic.GuardGoalNums
Mathlib.Tactic.GuardHypNums
Mathlib.Tactic.Have
Mathlib.Tactic.HaveI
Mathlib.Tactic.HigherOrder
Mathlib.Tactic.Hint
Mathlib.Tactic.ITauto
Mathlib.Tactic.InferParam
Mathlib.Tactic.Inhabit
Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IrreducibleDef
Mathlib.Tactic.Lemma
Mathlib.Tactic.Lift
Mathlib.Tactic.Linarith
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.Linter
Mathlib.Tactic.Measurability
Mathlib.Tactic.MinImports
Mathlib.Tactic.MkIffOfInductiveProp
Mathlib.Tactic.ModCases
Mathlib.Tactic.Module
Mathlib.Tactic.ModuleNF
Mathlib.Tactic.Monotonicity
Mathlib.Tactic.MoveAdd
Mathlib.Tactic.NoncommRing
Mathlib.Tactic.Nontriviality
Mathlib.Tactic.NormDet
Mathlib.Tactic.NormNum
Mathlib.Tactic.NormRank
Mathlib.Tactic.NthRewrite
Mathlib.Tactic.Observe
Mathlib.Tactic.OfNat
Mathlib.Tactic.Order
Mathlib.Tactic.PNatToNat
Mathlib.Tactic.PPWithUniv
Mathlib.Tactic.Peel
Mathlib.Tactic.Polyrith
Mathlib.Tactic.Positivity
Mathlib.Tactic.ProdAssoc
Mathlib.Tactic.ProxyType
Mathlib.Tactic.Push
Mathlib.Tactic.Qify
Mathlib.Tactic.RSuffices
Mathlib.Tactic.Recall
Mathlib.Tactic.Recover
Mathlib.Tactic.ReduceModChar
Mathlib.Tactic.Rename
Mathlib.Tactic.RenameBVar
Mathlib.Tactic.Replace
Mathlib.Tactic.Rify
Mathlib.Tactic.Ring
Mathlib.Tactic.Says
Mathlib.Tactic.ScopedNS
Mathlib.Tactic.Set
Mathlib.Tactic.SetLike
Mathlib.Tactic.SetNotationForOrder
Mathlib.Tactic.Setm
Mathlib.Tactic.SimpIntro
Mathlib.Tactic.SimpRw
Mathlib.Tactic.Simps
Mathlib.Tactic.SplitIfs
Mathlib.Tactic.Spread
Mathlib.Tactic.StacksAttribute
Mathlib.Tactic.Subsingleton
Mathlib.Tactic.Substs
Mathlib.Tactic.SuccessIfFailWithMsg
Mathlib.Tactic.SudoSetOption
Mathlib.Tactic.SuppressCompilation
Mathlib.Tactic.SwapVar
Mathlib.Tactic.TFAE
Mathlib.Tactic.TacticAnalysis
Mathlib.Tactic.Tauto
Mathlib.Tactic.TautoSet
Mathlib.Tactic.TermCongr
Mathlib.Tactic.ToAdditive
Mathlib.Tactic.ToDual
Mathlib.Tactic.ToExpr
Mathlib.Tactic.ToFun
Mathlib.Tactic.ToLevel
Mathlib.Tactic.Trace
Mathlib.Tactic.TryThis
Mathlib.Tactic.TypeCheck
Mathlib.Tactic.TypeStar
Mathlib.Tactic.UnsetOption
Mathlib.Tactic.Use
Mathlib.Tactic.Variable
Mathlib.Tactic.WLOG
Mathlib.Tactic.WithoutCDot
Mathlib.Tactic.Zify
Mathlib.Tactic.Algebra.AlgebraNF
Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.ArithMult.Init
Mathlib.Tactic.Attr.Core
Mathlib.Tactic.Attr.Register
Mathlib.Tactic.Bound.Attribute
Mathlib.Tactic.Bound.Init
Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CategoryTheory.BicategoricalComp
Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.CategoryTheory.CancelIso
Mathlib.Tactic.CategoryTheory.CategoryStar
Mathlib.Tactic.CategoryTheory.CheckCompositions
Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.CategoryTheory.Elementwise
Mathlib.Tactic.CategoryTheory.IsoReassoc
Mathlib.Tactic.CategoryTheory.MonoidalComp
Mathlib.Tactic.CategoryTheory.Reassoc
Mathlib.Tactic.CategoryTheory.Slice
Mathlib.Tactic.CategoryTheory.ToApp
Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.TryPremises
Mathlib.Tactic.ClickSuggestions.Unfold
Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ComputeAsymptotics.Lemmas
Mathlib.Tactic.Continuity.Init
Mathlib.Tactic.Echelon.Bareiss
Mathlib.Tactic.Echelon.Cert
Mathlib.Tactic.Echelon.Core
Mathlib.Tactic.Echelon.Parsing
Mathlib.Tactic.Echelon.Rat
Mathlib.Tactic.Echelon.Zsqrtd
Mathlib.Tactic.Explode.Datatypes
Mathlib.Tactic.Explode.Pretty
Mathlib.Tactic.FieldSimp.Attr
Mathlib.Tactic.FieldSimp.Discharger
Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.Finiteness.Attr
Mathlib.Tactic.FunProp.Attr
Mathlib.Tactic.FunProp.Core
Mathlib.Tactic.FunProp.Decl
Mathlib.Tactic.FunProp.Elab
Mathlib.Tactic.FunProp.FunctionData
Mathlib.Tactic.FunProp.Mor
Mathlib.Tactic.FunProp.Theorems
Mathlib.Tactic.FunProp.ToBatteries
Mathlib.Tactic.FunProp.Types
Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.CoreAttrs
Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.Elab
Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.NNRealPreprocessor
Mathlib.Tactic.Linarith.Parsing
Mathlib.Tactic.Linarith.Preprocessing
Mathlib.Tactic.Linarith.Verification
Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.Linter.AuxLemma
Mathlib.Tactic.Linter.CommandRanges
Mathlib.Tactic.Linter.DeprecatedModule
Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
Mathlib.Tactic.Linter.DirectoryDependency
Mathlib.Tactic.Linter.DocPrime
Mathlib.Tactic.Linter.DocString
Mathlib.Tactic.Linter.EmptyLine
Mathlib.Tactic.Linter.FindDeprecations
Mathlib.Tactic.Linter.FlexibleLinter
Mathlib.Tactic.Linter.GlobalAttributeIn
Mathlib.Tactic.Linter.HashCommandLinter
Mathlib.Tactic.Linter.HaveILetI
Mathlib.Tactic.Linter.HaveLetLinter
Mathlib.Tactic.Linter.Header
Mathlib.Tactic.Linter.InternalConstructor
Mathlib.Tactic.Linter.Lint
Mathlib.Tactic.Linter.MinImports
Mathlib.Tactic.Linter.Multigoal
Mathlib.Tactic.Linter.OldObtain
Mathlib.Tactic.Linter.OverlappingInstances
Mathlib.Tactic.Linter.PPRoundtrip
Mathlib.Tactic.Linter.PrivateModule
Mathlib.Tactic.Linter.Style
Mathlib.Tactic.Linter.TacticDocumentation
Mathlib.Tactic.Linter.TextBased
Mathlib.Tactic.Linter.UnusedInstancesInType
Mathlib.Tactic.Linter.UnusedTactic
Mathlib.Tactic.Linter.UnusedTacticExtension
Mathlib.Tactic.Linter.UpstreamableDecl
Mathlib.Tactic.Linter.ValidatePRTitle
Mathlib.Tactic.Linter.Whitespace
Mathlib.Tactic.Measurability.Init
Mathlib.Tactic.Monotonicity.Attr
Mathlib.Tactic.Monotonicity.Basic
Mathlib.Tactic.Monotonicity.Lemmas
Mathlib.Tactic.Nontriviality.Core
Mathlib.Tactic.NormNum.Abs
Mathlib.Tactic.NormNum.Basic
Mathlib.Tactic.NormNum.BigOperators
Mathlib.Tactic.NormNum.Core
Mathlib.Tactic.NormNum.DivMod
Mathlib.Tactic.NormNum.Eq
Mathlib.Tactic.NormNum.GCD
Mathlib.Tactic.NormNum.Ineq
Mathlib.Tactic.NormNum.Inv
Mathlib.Tactic.NormNum.Irrational
Mathlib.Tactic.NormNum.IsCoprime
Mathlib.Tactic.NormNum.IsSquare
Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Tactic.NormNum.ModEq
Mathlib.Tactic.NormNum.NatFactorial
Mathlib.Tactic.NormNum.NatFib
Mathlib.Tactic.NormNum.NatLog
Mathlib.Tactic.NormNum.NatSqrt
Mathlib.Tactic.NormNum.OfScientific
Mathlib.Tactic.NormNum.Ordinal
Mathlib.Tactic.NormNum.Parity
Mathlib.Tactic.NormNum.Pow
Mathlib.Tactic.NormNum.PowMod
Mathlib.Tactic.NormNum.Prime
Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Tactic.NormNum.Result
Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Polynomial.Basic
Mathlib.Tactic.Polynomial.Core
Mathlib.Tactic.Positivity.Basic
Mathlib.Tactic.Positivity.Core
Mathlib.Tactic.Positivity.Finset
Mathlib.Tactic.Push.Attr
Mathlib.Tactic.ReduceModChar.Ext
Mathlib.Tactic.Relation.Rfl
Mathlib.Tactic.Relation.Symm
Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.NamePolyVars
Mathlib.Tactic.Ring.NamePowerVars
Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Simproc.Divisors
Mathlib.Tactic.Simproc.ExistsAndEq
Mathlib.Tactic.Simproc.Factors
Mathlib.Tactic.Simproc.FinsetInterval
Mathlib.Tactic.Simproc.VecPerm
Mathlib.Tactic.Simps.Basic
Mathlib.Tactic.Simps.NotationClass
Mathlib.Tactic.TacticAnalysis.Declarations
Mathlib.Tactic.Translate.Attributes
Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.GuessName
Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.TagUnfoldBoundary
Mathlib.Tactic.Translate.ToAdditive
Mathlib.Tactic.Translate.ToDual
Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.Widget.Calc
Mathlib.Tactic.Widget.CommDiag
Mathlib.Tactic.Widget.CongrM
Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Widget.GCongr
Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.Widget.SelectInsertParamsClass
Mathlib.Tactic.Widget.SelectPanelUtils
Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.CategoryTheory.Bicategory.Basic
Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.CategoryTheory.Coherence.Basic
Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.CategoryTheory.Monoidal.Basic
Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Inclusion.Core.Core
Mathlib.Tactic.Inclusion.Core.DiscrTreeExt
Mathlib.Tactic.Inclusion.Core.Elab
Mathlib.Tactic.Inclusion.Core.Expr
Mathlib.Tactic.Inclusion.Core.Extensions
Mathlib.Tactic.Inclusion.Core.Inclusion
Mathlib.Tactic.Inclusion.Core.ToSet
Mathlib.Tactic.Inclusion.Core.Types
Mathlib.Tactic.Inclusion.Extension.Interval
Mathlib.Tactic.Inclusion.ExtensionAPI.Attr
Mathlib.Tactic.Inclusion.ExtensionAPI.Basic
Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
Mathlib.Tactic.Linter.TextBased.UnicodeLinter
Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Graph.Tarjan
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Mathlib.Tactic.Inclusion.Extension.Core.Core
Mathlib.Tactic.Inclusion.Extension.Core.Init
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Basic
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.BinarySplit
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Hypotheses
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Init
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Rational
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Tactic
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
Imported by
← Mathematical handbook