Documentation
Init
Search
Google site search
return to top
source
Imports
Init.BinderPredicates
Init.ByCases
Init.Control
Init.Conv
Init.Core
Init.Data
Init.Dynamic
Init.Ext
Init.Grind
Init.Guard
Init.Hints
Init.MacroTrace
Init.Meta
Init.MetaTypes
Init.Notation
Init.NotationExtra
Init.Omega
Init.Prelude
Init.PropLemmas
Init.RCases
Init.ShareCommon
Init.SimpLemmas
Init.Simproc
Init.SizeOfLemmas
Init.Syntax
Init.System
Init.Tactics
Init.TacticsExtra
Init.Util
Init.WF
Init.WFTactics
Init.While
Init.Data.Basic
Imported by
Mathlib.Algebra.BigOperators.Group.List
Mathlib.Tactic.IrreducibleDef
Mathlib.Tactic.ProjectionNotation
Lake.Build.Key
Mathlib.Data.List.Duplicate
Mathlib.Order.Hom.Bounded
Lake.Config.WorkspaceConfig
Mathlib.Algebra.GroupWithZero.Defs
Mathlib.Data.Multiset.Sort
Mathlib.Data.Finset.Image
Mathlib.Data.Finite.Defs
Lake.Util.Version
Mathlib.Tactic.Hint
Mathlib.Tactic.GCongr.CoreAttrs
Batteries.Control.Nondet.Basic
Qq.AssertInstancesCommute
Lake.Util.OrdHashSet
Mathlib.Tactic.CC.Addition
Plausible.Functions
Aesop.Builder.Cases
Mathlib.Data.PNat.Equiv
Aesop.Script.StructureStatic
Aesop.Frontend.Extension
Mathlib.Logic.Nonempty
Mathlib.Data.Set.Monotone
Mathlib.Tactic.ExistsI
Mathlib.Algebra.Divisibility.Hom
Batteries.Tactic.Lint.Basic
Batteries.Util.ExtendedBinder
Mathlib.Logic.Pairwise
Batteries.Lean.NameMapAttribute
Mathlib.Data.Int.Notation
Mathlib.Tactic.Simps.Basic
Mathlib.Algebra.Ring.Parity
Mathlib.Tactic.TermCongr
Mathlib.Data.Vector.Defs
Mathlib.Algebra.Order.Monoid.WithTop
Mathlib.Logic.Embedding.Set
Batteries.Data.Nat.Basic
Aesop.Stats.Report
Lake.Toml.Grammar
Qq.Macro
Mathlib.Order.SymmDiff
Batteries.Lean.TagAttribute
Mathlib.Data.Finset.Max
Mathlib.Order.Defs.PartialOrder
Lake.Build.Index
Lake.Version
Batteries.Tactic.Basic
Mathlib.Tactic.ToAdditive.Frontend
Aesop.Stats.Basic
Mathlib.Data.List.Range
Batteries.Lean.Meta.Basic
Lake
Lake.Util.Compare
Qq.ForLean.ToExpr
Aesop.Tree.Data
Lake.Toml.Load
Mathlib.Logic.ExistsUnique
Mathlib.Algebra.Group.Units.Hom
Mathlib.Tactic.Common
Mathlib.Tactic.Linter.HashCommandLinter
Mathlib.Control.EquivFunctor
Mathlib.Tactic.Linter.PPRoundtrip
Mathlib.Logic.Function.Defs
Lake.Build.Info
Aesop.RuleTac.Forward
Lake.Util.IO
Mathlib.Tactic.Nontriviality
Mathlib.Algebra.Order.Monoid.Canonical.Defs
Mathlib.Algebra.Order.Sub.Defs
Batteries.Lean.HashSet
Aesop.Tree.RunMetaM
Mathlib.Algebra.Group.Semiconj.Units
Mathlib.Util.Notation3
Batteries.Lean.MonadBacktrack
Mathlib.Tactic.GCongr.ForwardAttr
Batteries.Lean.Meta.Expr
Mathlib.Algebra.Ring.Nat
Mathlib.Data.Finset.Dedup
Aesop.BuiltinRules
Mathlib.Data.SetLike.Basic
Mathlib.Data.Finset.Insert
Aesop.Constants
Lake.Util.List
Mathlib.Order.Max
Mathlib.Data.Int.Cast.Defs
Mathlib.Order.Interval.Set.Basic
Mathlib.Order.Hom.Set
Mathlib.Tactic.NthRewrite
Mathlib.Algebra.Group.Int
Mathlib.Tactic.GCongr.Core
Mathlib.Util.MemoFix
Mathlib.Computability.Primrec
Mathlib.Logic.Equiv.Basic
PartialCombinatoryAlgebras.FreeCombinatoryAlgebra
Mathlib.Data.Nat.Sqrt
Mathlib.Logic.Equiv.Defs
Batteries.WF
Lake.Toml.Data.Dict
Mathlib.Tactic.TypeStar
Mathlib.Data.Finset.Defs
Lake.Util.Git
Mathlib.Logic.Nontrivial.Basic
Lake.Config.FacetConfig
Lake.Build.Imports
Mathlib.Tactic.SudoSetOption
Mathlib.Tactic.Trace
Lake.Util.Exit
Aesop.RuleTac.Basic
Aesop.Options.Internal
Mathlib.Lean.Name
Mathlib.Tactic.Rename
Lake.Build.Basic
Mathlib.Data.FunLike.Embedding
ProofWidgets.Util
Mathlib.Data.Set.Notation
Mathlib.Algebra.Group.Commute.Defs
Mathlib.Algebra.Group.InjSurj
Aesop.RuleSet
Mathlib.Data.List.Chain
Aesop.RuleSet.Member
Aesop.Frontend.Saturate
Aesop.Util.EqualUpToIds
Aesop.Builder.Basic
Mathlib.Logic.IsEmpty
Mathlib.Algebra.Order.GroupWithZero.Synonym
Mathlib.Algebra.Opposites
Lake.Build.Executable
Batteries.Tactic.Exact
Mathlib.Tactic.Use
Aesop.RuleTac.Tactic
Aesop.Tree.UnsafeQueue
Mathlib.Tactic.Eqns
Mathlib.Algebra.Order.GroupWithZero.Unbundled
Aesop.Index.Basic
Mathlib.Algebra.Group.Units.Basic
Mathlib.Order.Compare
Mathlib.Data.List.Dedup
Batteries.Lean.Expr
Mathlib.Data.List.MinMax
Mathlib.Tactic.TypeCheck
Lake.Util.Task
Mathlib.Tactic.Says
LeanSearchClient.Basic
Batteries.CodeAction.Basic
Lake.DSL
Mathlib.Util.Tactic
Mathlib.Tactic.Relation.Symm
Mathlib.Order.Notation
PartialCombinatoryAlgebras.Programming
Mathlib.Algebra.Group.Basic
Batteries.Data.List.Lemmas
ProofWidgets.Component.MakeEditLink
Mathlib.Data.Vector.Basic
Mathlib.Data.List.Monad
Mathlib.Data.Set.Image
Mathlib.Algebra.Group.Embedding
Mathlib.Tactic.Finiteness.Attr
Mathlib.Tactic.Attr.Register
Mathlib.Data.Nat.BinaryRec
Mathlib.Data.Set.Lattice
Aesop.Builder.NormSimp
Mathlib.Logic.Function.Conjugate
Mathlib.Order.GaloisConnection
Lake.Util.StoreInsts
Mathlib.Algebra.GroupWithZero.Nat
Lake.Util.Lift
Mathlib.Algebra.Group.Hom.Basic
Mathlib.Algebra.BigOperators.Group.Multiset
Mathlib.Algebra.Group.Hom.Defs
ProofWidgets.Compat
Mathlib.Data.List.Pairwise
Mathlib.Tactic.Linter.RefineLinter
Aesop.ElabM
Batteries.Data.List.Count
Mathlib.Tactic.DeclarationNames
Mathlib.Tactic.ByContra
Lake.Build.Store
Lake.Util.Proc
Lake.CLI.Actions
Batteries.Lean.Meta.UnusedNames
Batteries.Tactic.PermuteGoals
Mathlib.Order.WithBot
Aesop.Script.Step
Mathlib.Data.Multiset.Lattice
Mathlib.Order.Hom.Lattice
Mathlib.Data.ULift
Mathlib.Data.Part
Mathlib.Algebra.Order.AddGroupWithTop
Mathlib.Order.RelIso.Basic
Lake.Util.Message
Batteries.Data.BinomialHeap.Basic
Batteries.Data.Array.Basic
Mathlib.Algebra.Order.Monoid.Defs
Lake.Config.LeanExe
Batteries.Data.List.Basic
Mathlib.Data.Quot
Mathlib.Data.Finset.Empty
Lake.Build.Common
Mathlib.Algebra.Group.Even
Aesop.Builder.Constructors
Batteries.CodeAction.Misc
Aesop.Options.Public
Mathlib.Algebra.GroupWithZero.Units.Equiv
Lake.Util.Family
Batteries.Tactic.Lint.Misc
Lake.Config.ExternLibConfig
Mathlib.Util.WithWeakNamespace
Aesop.RuleTac.FVarIdSubst
Mathlib.Algebra.Order.Ring.Nat
Mathlib.Tactic.Cases
Mathlib.Data.Multiset.Nodup
Mathlib.Data.Set.Defs
Qq.ForLean.ReduceEval
Batteries.Data.Array.Init.Lemmas
Mathlib.Data.Nat.Order.Lemmas
Mathlib.Data.List.NodupEquivFin
Mathlib.Tactic.Linter.GlobalAttributeIn
Mathlib.Data.List.Flatten
Mathlib.Data.List.Infix
Batteries.Tactic.Lint.Frontend
Aesop.RuleSet.Name
Mathlib.Data.Multiset.Fold
Aesop.Script.TacticState
Lake.Util.Name
Mathlib.Data.Countable.Defs
Mathlib.Util.Delaborators
Mathlib.Data.Int.Cast.Basic
Mathlib.Algebra.Group.Nat.Even
Aesop.Script.SpecificTactics
Mathlib.Tactic.Widget.CongrM
Lake.Build.Fetch
Mathlib.Tactic.Conv
Lake.Build.Trace
Mathlib.Tactic.RenameBVar
Lake.Config.Script
Mathlib.Tactic.Substs
Batteries.Linter
Mathlib.Data.FunLike.Basic
Aesop.Stats.Extension
Lake.Load.Config
Mathlib.Algebra.Group.Units.Defs
Batteries.Lean.Syntax
Mathlib.Data.Finset.Lattice.Lemmas
Mathlib.Logic.OpClass
Mathlib.Logic.Encodable.Basic
Mathlib.Data.Set.NAry
Mathlib.Data.Nat.Pairing
Lake.Toml.Elab.Value
Aesop.Search.Main
Mathlib.Data.List.Defs
Mathlib.Tactic.Set
Mathlib.Tactic.Inhabit
Mathlib.Tactic.Linter.MinImports
Mathlib.Algebra.Order.Ring.Defs
Aesop.Script.Tactic
Mathlib.Data.Int.Order.Basic
Lake.Toml.Data.Value
Mathlib.Data.Set.SymmDiff
Mathlib.Tactic.GeneralizeProofs
Lake.Build.Topological
Lake.Config.Package
Mathlib.Algebra.Group.Pi.Basic
Mathlib.Algebra.Ring.Commute
Batteries.Tactic.Alias
Aesop.Script.GoalWithMVars
Batteries.Tactic.Lint.Simp
Mathlib.Data.Finset.Union
Lake.Toml.ParserUtil
Lake.Config.ExternLib
Mathlib.Data.Bool.Basic
Batteries.Data.List.Init.Lemmas
Aesop.BuiltinRules.Ext
Mathlib.Data.Int.Defs
PartialCombinatoryAlgebras.PartialCombinatoryAlgebra
Aesop.Tree.TreeM
Plausible
Mathlib.Tactic.ExtendDoc
Mathlib.Tactic.RSuffices
Mathlib.Logic.Equiv.Set
Mathlib.Data.Bracket
Mathlib.Tactic.WLOG
PartialCombinatoryAlgebras.Basic
Mathlib.Tactic.Linter.HaveLetLinter
Aesop.Tree.Traversal
Mathlib.Order.BoundedOrder.Lattice
Mathlib.Computability.PartrecCode
Mathlib.Data.Fin.Tuple.Basic
Lake.Reservoir
Mathlib.Data.Nat.Set
Aesop.Check
Mathlib.Data.Fintype.Card
Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas
Mathlib.Algebra.Group.Equiv.Basic
ProofWidgets.Cancellable
Mathlib.Tactic.DeriveToExpr
Mathlib.Data.FunLike.Equiv
Aesop.Script.Check
Mathlib.Algebra.Order.Sub.Unbundled.Basic
Plausible.Sampleable
Aesop.Script.StructureDynamic
Batteries.Data.RBMap.Basic
Mathlib.Algebra.Group.Nat.Units
Mathlib.Logic.Function.Basic
Mathlib.Logic.Relator
Aesop.Tree.State
Mathlib.Tactic.Find
Batteries.CodeAction.Attr
LeanSearchClient.LoogleSyntax
Mathlib.Tactic.CongrExclamation
Mathlib.Tactic.ScopedNS
Batteries.Lean.Meta.InstantiateMVars
Aesop.Exception
Mathlib.Data.Nat.PSub
ImportGraph.Imports
Aesop.Tree.ExtractProof
Mathlib.Data.Finset.SymmDiff
Mathlib.Data.List.Perm.Lattice
Aesop.Search.Queue
Qq
Mathlib.Algebra.Group.Defs
Mathlib.Algebra.Group.Opposite
Lake.DSL.Script
Mathlib.Lean.PrettyPrinter.Delaborator
Batteries.Control.ForInStep.Lemmas
Mathlib.Order.Defs.LinearOrder
Batteries.Tactic.HelpCmd
Batteries.Lean.Position
Batteries.Util.ProofWanted
Batteries.Tactic.Unreachable
Mathlib.Tactic.CongrM
Mathlib.Algebra.Ring.Basic
Mathlib.Data.Multiset.FinsetOps
Mathlib.Order.TypeTags
Lake.DSL.DeclUtil
Mathlib.Init
Mathlib.Algebra.NeZero
Lake.DSL.Config
Aesop.Tree.AddRapp
ProofWidgets.Data.Html
Mathlib.Data.Fintype.Basic
Aesop.BuiltinRules.Rfl
Batteries.Tactic.SeqFocus
Mathlib.Logic.Equiv.Option
Aesop.Script.SScript
Mathlib.Algebra.Group.Operations
Batteries.Tactic.Trans
Batteries.Classes.Order
Lake.Build.Job
Mathlib.Data.Nat.Notation
Mathlib.Order.Interval.Set.Defs
Aesop.Builder.Tactic
Mathlib.Order.Synonym
Aesop.Tracing
Mathlib.Tactic.CC.Lemmas
Mathlib.Data.Finset.Filter
Aesop.RuleTac.Preprocess
Mathlib.Tactic.Subsingleton
Mathlib.Data.Set.Subsingleton
Aesop.Util.Basic
Mathlib.Tactic.Linter.UnusedTactic
Mathlib.Data.Set.Pairwise.Basic
Plausible.Attr
Mathlib.Tactic.Convert
Qq.Delab
Mathlib.Tactic.Linter.OldObtain
Mathlib.Tactic.MkIffOfInductiveProp
Aesop.Tree.Check
Mathlib.Data.Prod.Basic
Mathlib.Algebra.GroupWithZero.Commute
Mathlib.Data.Nat.Cast.Defs
Mathlib.Data.Finset.Range
Mathlib.Algebra.Ring.Semiconj
ProofWidgets.Component.OfRpcMethod
Mathlib.Tactic.Widget.SelectInsertParamsClass
Mathlib.Algebra.Order.Group.Nat
Mathlib.Algebra.Ring.Units
Batteries.Util.LibraryNote
Mathlib.Logic.Relation
Aesop.Saturate
Mathlib.Order.CompleteBooleanAlgebra
Mathlib.Order.BoundedOrder.Monotone
Mathlib.Tactic.GuardGoalNums
Mathlib.Control.Applicative
Aesop.Builder.Forward
Qq.Match
Aesop.Frontend.Extension.Init
Mathlib.Tactic.Linter.Multigoal
Mathlib.Data.List.Lattice
Mathlib.Util.AssertExistsExt
Mathlib.Data.List.FinRange
Lake.Config.InstallPath
Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Mathlib.Algebra.Group.Commute.Units
Mathlib.Tactic.Choose
Mathlib.Order.Defs.Unbundled
Mathlib.Order.BooleanAlgebra
Lake.Util.Lock
Aesop.RuleSet.Filter
Mathlib.Tactic.Basic
Aesop.BuiltinRules.Intros
Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.Order.Hom.Basic
Aesop.Util.UnionFind
Mathlib.Data.Multiset.Dedup
Mathlib.Algebra.Order.Ring.Unbundled.Basic
Mathlib.Algebra.Group.Nat.Basic
Mathlib.Tactic.SplitIfs
Aesop.Util.UnorderedArraySet
Lake.Config.Module
Lake.CLI.Build
PartialCombinatoryAlgebras.CombinatoryAlgebra
Lake.Config
Mathlib.Data.Finset.Erase
Mathlib.Data.Fin.Basic
Mathlib.Algebra.Order.Monoid.NatCast
Lake.Config.Dependency
Mathlib.Tactic.CC.Datatypes
Mathlib.Data.Multiset.Basic
Mathlib.Tactic.Lift
Mathlib.Tactic.Linter.FlexibleLinter
Lake.Build.Facets
Mathlib.Control.Traversable.Basic
Batteries.Data.String.Basic
Aesop.Rule.Name
Lake.Config.Context
Mathlib.Data.Ordering.Basic
Mathlib.Tactic.InferParam
Batteries.Data.List.Perm
Mathlib.Algebra.Order.GroupWithZero.Canonical
Lake.Build.Data
Batteries.Data.RBMap.WF
Mathlib.Lean.Elab.Term
Mathlib.Data.Multiset.Range
Mathlib.Data.Sigma.Basic
Lake.Util.Casing
PartialCombinatoryAlgebras
Qq.MetaM
Mathlib.Algebra.Order.Ring.Canonical
Aesop.Util.Tactic.Ext
Lake.Config.Defaults
Mathlib.Tactic.Spread
Mathlib.Algebra.Group.ZeroOne
Mathlib.Tactic.Linter.Header
Mathlib.Logic.Basic
Batteries.Tactic.Init
Lake.Util.JsonObject
Aesop.Search.Queue.Class
Mathlib.Tactic.DeprecateTo
Mathlib.Data.Finset.Disjoint
Mathlib.Algebra.Order.Monoid.TypeTags
Mathlib.Util.AssertExists
Lake.Config.LeanExeConfig
Mathlib.Tactic.Attr.Core
Mathlib.Lean.EnvExtension
Mathlib.Order.Lattice
Lake.DSL.Require
Lake.Config.Opaque
Mathlib.Tactic.ClearExclamation
Plausible.Testable
Mathlib.Logic.Function.Iterate
Mathlib.Control.Combinators
Mathlib.Tactic.Bound.Attribute
Mathlib.Algebra.GroupWithZero.Semiconj
Aesop.Nanos
Lake.Util.Sugar
Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Mathlib.Data.Set.Prod
Mathlib.Data.Finset.Basic
Mathlib.Order.WellFounded
Mathlib.Data.Finset.Lattice.Fold
Aesop.Rule
Batteries.Tactic.Where
Aesop.Search.RuleSelection
Mathlib.Tactic.ApplyCongr
Aesop.Options
Batteries.Tactic.Congr
Mathlib.Data.Nat.Cast.Commute
Lake.Config.LeanLibConfig
Mathlib.Order.PropInstances
Lake.Util.Opaque
Aesop.Script.CtorNames
LeanSearchClient
Mathlib.Algebra.Order.Group.Unbundled.Basic
Mathlib.Order.RelClasses
Lake.Util.OrderedTagAttribute
Mathlib.Data.Array.Defs
Mathlib.Data.Set.Function
Aesop.Builder.Apply
Lake.CLI.Error
Mathlib.Order.CompleteLattice
PartialCombinatoryAlgebras.FirstKleeneAlgebra
Mathlib.Order.Disjoint
Aesop.Rule.Basic
Mathlib.Logic.Function.ULift
Lake.Config.TargetConfig
Mathlib.Data.Nat.Find
Lake.DSL.Extensions
Aesop.Builder.Default
Lake.Toml.Elab.Expression
Mathlib.Data.List.Rotate
Batteries.Lean.PersistentHashMap
Mathlib.Algebra.Group.Semiconj.Defs
Mathlib.Data.Finset.Attr
Mathlib.Data.Int.DivMod
Lake.Config.LeanConfig
Mathlib.Order.Directed
Aesop.Tree.Free
Aesop.BuiltinRules.ApplyHyps
Mathlib.Tactic.ClearExcept
Mathlib.Algebra.Order.Monoid.Basic
Mathlib.Order.SetNotation
Aesop.BuiltinRules.DestructProducts
Mathlib.Tactic.SetLike
Mathlib.Tactic.Widget.Conv
Mathlib.Data.Nat.Cast.Basic
Lake.Util.Date
ProofWidgets.Component.Basic
Lake.Toml
Mathlib.Tactic.Nontriviality.Core
Mathlib.Logic.Equiv.Nat
Mathlib.Data.Finset.Attach
Aesop.Search.ExpandSafePrefix
Plausible.Gen
Mathlib.Algebra.Ring.Defs
Lake.Build.Package
Mathlib.Data.Multiset.Bind
Mathlib.Algebra.Group.TypeTags.Basic
Mathlib.Lean.Expr.ExtraRecognizers
Plausible.Random
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Tactic.FBinop
Lake.Build
Mathlib.Order.Fin.Basic
Lake.Util.Store
Lake.Util.Cycle
Batteries.Util.Cache
Aesop.RuleTac.Forward.Basic
Lake.Util.DRBMap
Mathlib.Tactic.Core
Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Mathlib.Order.BoundedOrder.Basic
Mathlib.Order.Bounds.Defs
Mathlib.Algebra.Order.ZeroLEOne
Batteries.Lean.Except
Lake.Build.Targets
Lake.Config.Workspace
Mathlib.Tactic.CasesM
Mathlib.Order.Heyting.Basic
Batteries.Control.ForInStep.Basic
Mathlib.Order.Bounds.Basic
Mathlib.Logic.Denumerable
Mathlib.Tactic.PPWithUniv
Mathlib.Order.Basic
Mathlib.Algebra.Ring.InjSurj
Mathlib.Data.String.Defs
Qq.ForLean.Do
Mathlib.Logic.Equiv.List
Mathlib.Tactic.Contrapose
Mathlib.Tactic.SimpRw
Mathlib.Tactic.Tauto
Mathlib.Data.PNat.Notation
Mathlib.Logic.Nontrivial.Defs
Mathlib.Data.List.Perm.Basic
Mathlib.Data.List.OfFn
Mathlib.Data.Finset.Card
Mathlib.Logic.Unique
Aesop.RulePattern
Batteries.Linter.UnreachableTactic
Aesop.RuleTac.Apply
Mathlib.Tactic.DefEqTransformations
Aesop.Util.Tactic.Unfold
Lake.Config.Glob
Mathlib.Control.ULift
Mathlib.Tactic.SimpIntro
Mathlib.Tactic.Observe
Aesop.BuiltinRules.Subst
Mathlib.Data.List.Perm.Subperm
Mathlib.Data.Finset.SDiff
Lake.DSL.Package
Lake.Toml.Elab
Aesop.RuleTac.GoalDiff
Batteries.Data.Array.Merge
Mathlib.Data.PNat.Defs
Aesop.Script.Main
Mathlib.Util.WhatsNew
Mathlib.Control.Functor
Mathlib.Tactic.CC
ImportGraph.RequiredModules
Mathlib.Control.Basic
Mathlib.Data.Int.Sqrt
Mathlib.Data.List.Basic
Mathlib.Algebra.GroupWithZero.Basic
Aesop.Search.Expansion.Norm
Mathlib.Lean.Elab.Tactic.Basic
Mathlib.Tactic.ToExpr
Lake.Build.Actions
Mathlib.Algebra.Divisibility.Basic
Mathlib.Logic.Embedding.Basic
Lake.Util.Log
Mathlib.Data.List.Lex
Batteries.Tactic.Lint
Mathlib.Data.Nat.Defs
Mathlib.Lean.Meta
Mathlib.Tactic.ExtractGoal
Mathlib.Data.List.ProdSigma
Mathlib.Tactic.Coe
Mathlib.Order.ULift
Mathlib.Data.List.Sort
Batteries.Data.List.Pairwise
Mathlib.Order.Nat
Lake.Util.RBArray
Mathlib.Algebra.GroupWithZero.InjSurj
Aesop
Mathlib.Algebra.GroupWithZero.NeZero
Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Batteries.Lean.PersistentHashSet
Mathlib.Tactic.Variable
Plausible.Tactic
Lean
Qq.SortLocalDecls
Lake.Config.LeanLib
Batteries.Lean.AttributeExtra
Mathlib.Util.CompileInductive
Aesop.RuleTac.ElabRuleTerm
Aesop.Script.OptimizeSyntax
Batteries.Lean.Meta.SavedState
Mathlib.Tactic.Constructor
Aesop.Frontend.Command
Mathlib.Tactic.Simps.NotationClass
Mathlib.Data.Option.NAry
Mathlib.Tactic.FailIfNoProgress
Aesop.Frontend.Tactic
Mathlib.Tactic.Linter.Lint
Batteries.Data.MLList.Basic
Mathlib.Tactic.ToAdditive
Aesop.Index
Mathlib.Data.List.Nodup
Aesop.RuleTac
Mathlib.Data.Prod.PProd
Mathlib.Data.SProd
Aesop.Search.Expansion
Mathlib.Data.Multiset.Pi
Batteries.CodeAction
Mathlib.Tactic.Propose
Aesop.RuleTac.Cases
Mathlib.Tactic.Linter.Style
Aesop.Script.UScriptToSScript
Mathlib.Algebra.Group.Units.Equiv
Mathlib.Data.Option.Basic
Aesop.Frontend.Basic
Mathlib.Util.CountHeartbeats
Mathlib.Tactic.AdaptationNote
Mathlib.Tactic.Linter.DocPrime
Lake.DSL.AttributesCore
Mathlib.Data.Finset.Fold
Mathlib.Order.Monotone.Basic
Aesop.Frontend.Attribute
Lake.Toml.Data.DateTime
PartialCombinatoryAlgebras.GraphModel
Mathlib.Tactic.HigherOrder
Mathlib.Algebra.CharZero.Defs
Batteries.Lean.Meta.Inaccessible
Mathlib.Data.Option.Defs
Mathlib.Tactic.Linter.UpstreamableDecl
Mathlib.Algebra.Order.Sub.Basic
Aesop.Script.Util
Mathlib.Tactic.Relation.Rfl
Mathlib.Algebra.Group.WithOne.Defs
Mathlib.Data.Set.List
Lake.Build.Module
Mathlib.Tactic.Widget.SelectPanelUtils
Mathlib.Tactic.Widget.Calc
Mathlib.Data.Nat.Bits
Aesop.Search.SearchM
Mathlib.Algebra.Order.Group.Synonym
Mathlib.Tactic.MinImports
Aesop.Search.Expansion.Basic
Mathlib.Data.Finset.Sort
Mathlib.Tactic.Linter
Mathlib.Computability.Partrec
Mathlib.Tactic.ApplyWith
Aesop.Builder.Unfold
Batteries.Linter.UnnecessarySeqFocus
Mathlib.Tactic.Clear_
Mathlib.Tactic.Lemma
Aesop.Tree.ExtractScript
Mathlib.Data.Bool.Set
Lake.DSL.Targets
Mathlib.Algebra.Order.Monoid.OrderDual
Mathlib.Data.PFun
Mathlib.Data.Set.Basic
Mathlib.Tactic.Check
Lake.Config.Env
Lake.Util.Binder
Batteries.CodeAction.Deprecated
Lake.Util.NativeLib
Lake.Build.Run
Mathlib.Algebra.GroupWithZero.Hom
Mathlib.Tactic.Bound.Init
Mathlib.Data.Set.Operations
Mathlib.Algebra.Group.TypeTags.Hom
Aesop.Percent
Mathlib.Algebra.Order.Group.Defs
Mathlib.Tactic.ExtractLets
Aesop.Util.Tactic
Mathlib.Data.Finset.Lattice.Basic
Lake.Util.FilePath
Mathlib.Data.Finset.Pi
Mathlib.Lean.Meta.Simp
Batteries.Tactic.OpenPrivate
Lake.DSL.Attributes
Batteries.Lean.Meta.DiscrTree
Mathlib.Tactic.Recover
Lake.Build.Library
Mathlib.Tactic.PushNeg
Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Mathlib.Tactic.Monotonicity.Attr
Mathlib.Data.List.Forall2
Aesop.Script.ScriptM
Mathlib.Data.Sum.Basic
Mathlib.Order.MinMax
Batteries.Tactic.Lint.TypeClass
Lake.Util.Error
Mathlib.Tactic.SuccessIfFailWithMsg
Mathlib.Algebra.Group.Prod
Aesop.Main
Aesop.Search.Expansion.Simp
Aesop.Script.UScript
Mathlib.Lean.Meta.CongrTheorems
Mathlib.Tactic.UnsetOption
Mathlib.Data.Subtype
Aesop.BuiltinRules.Assumption
Mathlib.Data.Rel
Mathlib.Algebra.GroupWithZero.WithZero
Mathlib.Lean.Expr.ReplaceRec
Mathlib.Tactic.GuardHypNums
Mathlib.Lean.Meta.Basic
Mathlib.Order.Bounds.Image
Mathlib.Tactic.StacksAttribute
Mathlib.Tactic.SwapVar
Mathlib.Lean.Expr.Basic
Aesop.Tree
Mathlib.Tactic.ApplyAt
Aesop.Frontend.RuleExpr
Lake.Util.EStateT
Mathlib.Data.Finset.Prod
Qq.Typ
Batteries.Logic
Batteries.Data.RBMap.Alter
Lake.DSL.Meta
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Mathlib.Tactic.ToLevel
Aesop.BuiltinRules.Split
Lake.Config.Monad
LeanSearchClient.Syntax
Lake.Util.EquipT
Aesop.Tree.Tracing
Mathlib.Order.RelIso.Set