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.System
Init.Tactics
Init.TacticsExtra
Init.Util
Init.WF
Init.WFTactics
Init.Data.Basic
Imported by
Batteries.Tactic.Init
Batteries.Data.List.Lemmas
Aesop.Search.Expansion.Basic
Batteries.Lean.AttributeExtra
Aesop.Builder
Mathlib.Data.Set.Image
Batteries.Control.Lemmas
Mathlib.Data.Finset.Basic
Mathlib.Algebra.Order.Monoid.Canonical.Defs
Mathlib.Data.Int.GCD
Aesop.Tree.ExtractProof
Mathlib.Data.Bool.Basic
Mathlib.Data.Nat.Set
Aesop.Builder.NormSimp
Mathlib.Algebra.Ring.Hom.Basic
Arithmetization.ISigmaOne.HFS.Seq
Mathlib.Algebra.Order.Monoid.Units
Mathlib.Algebra.CharZero.Defs
Mathlib.Algebra.GroupWithZero.Units.Lemmas
Lake.CLI.Error
Mathlib.Logic.Basic
Mathlib.Algebra.Order.Group.Synonym
Mathlib.Algebra.GroupWithZero.WithZero
Mathlib.Tactic.Eqns
Aesop.RuleTac.Tactic
Mathlib.Util.MemoFix
Mathlib.Data.PFun
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Algebra.Field.Rat
Batteries.CodeAction.Attr
Mathlib.Algebra.Star.SelfAdjoint
Batteries.Data.Sum.Lemmas
Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Arithmetization.ISigmaOne.Metamath.Proof.Derivation
Mathlib.Algebra.Order.Ring.InjSurj
Mathlib.Tactic.TryThis
Batteries
Mathlib.Algebra.Order.Field.InjSurj
Logic.Vorspiel.NotationClass
Mathlib.Algebra.GroupWithZero.Basic
Batteries.Data.Array.Basic
Mathlib.Data.List.Enum
Mathlib.Order.WellFounded
Mathlib.Algebra.Opposites
Mathlib.Algebra.Order.Monoid.WithTop
Incompleteness.Arith.First
Batteries.Lean.NameMap
Aesop.RuleTac.ElabRuleTerm
Mathlib.Control.EquivFunctor
Mathlib.Data.Part
Batteries.Util.CheckTactic
Mathlib.Algebra.GroupWithZero.Defs
Mathlib.Data.Int.Order.Lemmas
Aesop.Nanos
Mathlib.Algebra.Order.Ring.Int
Logic.FirstOrder.Basic.Operator
Lake.Build.Common
Mathlib.Tactic.SplitIfs
Logic.Vorspiel.Arith
Mathlib.Data.Set.Pairwise.Basic
Arithmetization.ISigmaZero.Exponential.PPow2
Mathlib.Tactic.Lemma
Mathlib.Util.Delaborators
Mathlib.Algebra.Order.ZeroLEOne
Aesop.RuleTac.Cases
Lake.Build.Key
Mathlib.Data.Nat.Cast.Defs
Logic.FirstOrder.Arith.Theory
Mathlib.Data.SProd
Mathlib.Data.List.Pairwise
Mathlib.Data.W.Basic
Aesop.Options
Mathlib.Order.Iterate
Mathlib.Order.PiLex
Mathlib.Tactic.Says
Mathlib.Tactic.UnsetOption
Batteries.Lean.Float
Mathlib.Tactic.Coe
Mathlib.Tactic.SimpRw
Lake.Build.Executable
Logic.FirstOrder.Completeness.SearchTree
Aesop.BuiltinRules.Subst
Mathlib.Order.Antisymmetrization
Logic.Modal.Formula
Aesop.Script.Step
Logic.Modal.ModalCompanion.Basic
Mathlib.Data.Finset.Piecewise
Mathlib.Algebra.Group.Invertible.Defs
Logic.Modal.System
Mathlib.Tactic.NormNum.Eq
Mathlib.Mathport.Notation
Batteries.CodeAction.Deprecated
Logic.IntProp.Deduction
Mathlib.Algebra.Order.Interval.Set.Monoid
Lake.Toml.Data.Dict
Mathlib.Data.Set.Function
Mathlib.Data.Set.Functor
Mathlib.Data.ULift
Mathlib.Algebra.GroupWithZero.Commute
Mathlib.Order.Compare
Logic.FirstOrder.Basic.Soundness
Mathlib.Algebra.Group.Defs
Batteries.Data.UInt
Mathlib.Data.List.InsertNth
Lake.Build.Index
Batteries.Lean.NameMapAttribute
Mathlib.Mathport.Attributes
Mathlib.Data.Nat.ChineseRemainder
Mathlib.Tactic.Simps.NotationClass
Lake.Config.Defaults
Mathlib.Tactic.GeneralizeProofs
Mathlib.Lean.Name
Aesop.Script.SpecificTactics
Mathlib.Tactic.GCongr.Core
Batteries.Data.HashMap.Basic
Arithmetization.Vorspiel.Lemmata
Arithmetization.ISigmaZero.Exponential.Exp
Mathlib.Data.Nat.Prime.Defs
Lake.Util.IO
Mathlib.Algebra.Order.BigOperators.Group.List
Mathlib.Init.Logic
Aesop.Script.GoalWithMVars
Lake.Config.TargetConfig
Aesop.Builder.Default
Lake.DSL.Package
Mathlib.Control.Basic
Batteries.Data.Nat
Mathlib.Init.Data.Fin.Basic
Mathlib.Util.CompileInductive
Mathlib.Init.Data.Int.Order
Mathlib.Data.Nat.Cast.Commute
Mathlib.Order.Interval.Set.Basic
Incompleteness
Aesop.Util.Tactic
Mathlib.Tactic.Common
Batteries.Test.Internal.DummyLabelAttr
Batteries.Data.MLList.IO
Mathlib.Mathport.Rename
Logic.FirstOrder.Arith.Model
Mathlib.Tactic.Linter.HashCommandLinter
Mathlib.Data.FunLike.Embedding
Mathlib.Algebra.Order.Sub.Canonical
Lake.Config.InstallPath
Mathlib.Tactic.Ring
Mathlib.Algebra.Group.Hom.End
Mathlib.Algebra.Order.Field.Canonical.Defs
Aesop.Frontend.Basic
Mathlib.Order.Filter.Basic
Mathlib.Data.Nat.ModEq
Batteries.Data.LazyList
Batteries.Tactic.Classical
Lake.Config.Script
Mathlib.Data.List.Count
Mathlib.Algebra.BigOperators.Ring.Multiset
Mathlib.Control.Applicative
Aesop.Builder.Unfold
Mathlib.Logic.Equiv.Nat
ImportGraph.Imports
Mathlib.Data.Vector.Defs
Mathlib.Order.SuccPred.Basic
Mathlib.Data.List.GetD
Mathlib.Algebra.GCDMonoid.Basic
Logic.FirstOrder.Completeness.Corollaries
Arithmetization.Basic.PeanoMinus
Qq
Mathlib.Data.Finite.Basic
Mathlib.Tactic.Linarith.Preprocessing
Aesop.BuiltinRules.ApplyHyps
Batteries.Lean.Meta.AssertHypotheses
Logic.FirstOrder.Interpretation
Mathlib.Data.Rat.Cast.CharZero
Mathlib.Order.ZornAtoms
Aesop.RuleTac.Forward.Basic
Mathlib.Tactic.Widget.CongrM
Mathlib.Tactic.SetLike
Batteries.Data.Thunk
Mathlib.Data.List.Basic
Qq.ForLean.ReduceEval
Aesop.Stats.Basic
Batteries.Classes.SatisfiesM
Logic.Logic.Kripke.Tree
Batteries.Control.ForInStep.Lemmas
Mathlib.Tactic.Abel
Batteries.Classes.BEq
Batteries.Lean.Position
Qq.MetaM
Batteries.Lean.SMap
Mathlib.Data.NNRat.Defs
Mathlib.Data.Set.Lattice
Mathlib.Data.Finset.Prod
Aesop.Tree
Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.ExtendDoc
Batteries.Tactic.Where
Mathlib.Order.Interval.Set.Disjoint
Batteries.Tactic.Instances
Lake.Util.Task
Mathlib.Computability.Partrec
Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Batteries.Data.BinaryHeap
Mathlib.Algebra.Field.Defs
Mathlib.Data.Multiset.Range
Mathlib.Tactic.InferParam
Mathlib.Data.Multiset.Fold
Logic.IntProp.IntProp
Lake.Build.Targets
Mathlib.Order.Hom.Lattice
Mathlib.Tactic.SwapVar
Batteries.Data.List.Pairwise
Aesop.Search.SearchM
Aesop.Util.Tactic.Unfold
Qq.AssertInstancesCommute
Logic.Modal.Complemental
Mathlib.Tactic.Attr.Core
Mathlib.Data.Sym.Basic
Mathlib.Logic.Function.Defs
Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Mathlib.Order.UpperLower.Basic
Mathlib.Data.Multiset.Basic
Mathlib.Data.Fin.Basic
Lake.DSL.Meta
Mathlib.Tactic.ToAdditive.Frontend
Mathlib.Data.Tree.Basic
Mathlib.Tactic.Subsingleton
Lake.DSL.Config
Mathlib.Data.Option.Defs
Mathlib.Algebra.Ring.Equiv
Mathlib.Tactic.Core
Lake.DSL.Extensions
Batteries.Data.String.Basic
Mathlib.Init.Set
Aesop.RuleTac
Logic.FirstOrder.Basic.Calculus2
Mathlib.Lean.Elab.Tactic.Basic
Mathlib.Tactic.NormNum.Result
ProofWidgets.Cancellable
Logic.Modal.Kripke.Filteration
Logic.FirstOrder.Arith.PeanoMinus
Logic.FirstOrder.Ultraproduct
Aesop.Tree.TreeM
Mathlib.Data.Int.Cast.Defs
Mathlib.Data.Finset.Slice
Lake.Util.FilePath
Mathlib.Computability.Primrec
Mathlib.Algebra.Order.Group.OrderIso
Batteries.Lean.Meta.UnusedNames
Logic.FirstOrder.Basic.Syntax.Formula
Incompleteness.Arith.Theory
Mathlib.Tactic.ToLevel
Logic.IntProp.Kripke.DP
Lake.DSL
Mathlib.Tactic.Rename
Mathlib.Order.ULift
Lake.DSL.Script
Mathlib.Algebra.Order.Field.Defs
Batteries.Tactic.PrintPrefix
Mathlib.Tactic.DeprecateMe
Incompleteness.ProvabilityLogic.ProvabilityLogic
Mathlib.Algebra.Order.GroupWithZero.Synonym
Logic.FirstOrder.Arith.StrictHierarchy
Mathlib.Data.Rat.Cast.Lemmas
Mathlib.Init.ZeroOne
Mathlib.Order.LatticeIntervals
Mathlib.Tactic.ApplyWith
Mathlib.Tactic.HaveI
Aesop.RuleSet.Member
Mathlib.Order.Hom.Set
Batteries.StdDeprecations
Mathlib.Data.Set.Prod
Mathlib.Data.List.NodupEquivFin
Mathlib.Tactic.CC.Datatypes
Mathlib.Algebra.Ring.Pi
Mathlib.Data.Nat.Bitwise
Aesop.Frontend.Extension.Init
Mathlib.Data.List.Rotate
Lake.Build.Topological
Batteries.Tactic.Lint
Mathlib.Data.Fintype.Basic
Batteries.Classes.RatCast
Logic.Modal.Axioms
Mathlib.Data.Nat.GCD.BigOperators
Batteries.Data.Nat.Lemmas
Mathlib.Data.List.Range
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
Batteries.Tactic.PermuteGoals
Batteries.Data.Rat.Lemmas
Lake.Util.Proc
ImportGraph.RequiredModules
Mathlib.Order.Interval.Multiset
Mathlib.Tactic.Linter.UnusedTactic
Mathlib.Order.Zorn
Mathlib.Tactic.CasesM
Mathlib.Algebra.Ring.Action.Basic
Aesop.Script.SScript
Mathlib.Data.Set.Subsingleton
Mathlib.Tactic.Relation.Trans
Mathlib.Data.Sum.Basic
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.Init.Data.Nat.Lemmas
Lake
Mathlib.Algebra.Order.Group.Units
Mathlib.Data.Finset.Sigma
Mathlib.Algebra.Order.Group.Defs
Lake.Util.OrdHashSet
Logic.Modal.Kripke.Preservation
Mathlib.Algebra.Group.Invertible.Basic
ProofWidgets.Data.Svg
Batteries.Data.Nat.Gcd
Mathlib.Algebra.Order.Group.InjSurj
Mathlib.Tactic.Linter.Lint
Batteries.WF
Mathlib.Data.Fintype.Pi
ProofWidgets.Component.HtmlDisplay
Mathlib.Tactic.ToAdditive
Logic.Modal.Kripke.Ver
Arithmetization.Basic.Ind
Mathlib.GroupTheory.GroupAction.Group
Aesop.Exception
Lake.Build.Trace
Mathlib.Lean.Meta.Basic
Mathlib.Logic.Relation
Mathlib.Tactic.ClearExclamation
Batteries.Data.Rat.Basic
Mathlib.Tactic.Use
Aesop.Frontend.Extension
Mathlib.Algebra.GroupWithZero.Semiconj
Arithmetization.Basic.IOpen
Batteries.Tactic.Case
Mathlib.Util.Qq
Mathlib.Data.Array.Defs
Mathlib.Data.SetLike.Basic
Mathlib.Algebra.Group.Action.Units
Mathlib.Tactic.NormNum.Pow
Mathlib.Order.RelClasses
Batteries.Data.Fin
Mathlib.Tactic.Linter
Lake.Util.Lock
Mathlib.Algebra.Ring.Units
Aesop.Rule.Basic
Logic.Modal.Kripke.GL.GL
Mathlib.Order.Chain
Incompleteness.Arith.D1
Mathlib.Tactic.DeriveToExpr
Mathlib.Data.Nat.Bits
Logic.Logic.HilbertStyle.Basic
Batteries.Data.List.Perm
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
Aesop.Builder.Cases
Mathlib.Tactic.SuccessIfFailWithMsg
Aesop.RuleTac.Apply
Mathlib.Algebra.Ring.Regular
Mathlib.Algebra.Ring.Commute
Lake.Config.WorkspaceConfig
Lake.Config.Module
Mathlib.Algebra.Order.Group.Abs
Mathlib.Algebra.Group.Subsemigroup.Basic
Mathlib.Algebra.Group.Submonoid.Basic
Logic.IntProp.ConsistentTableau
Logic.FirstOrder.Basic.Coding
Mathlib.Data.Rat.Cast.Defs
Mathlib.Tactic.Monotonicity.Attr
Batteries.Data.Char
Batteries.Data.MLList.Basic
Arithmetization.Vorspiel.ExistsUnique
Lake.Util.Family
Batteries.Lean.Meta.SavedState
Mathlib.Tactic.Linter.Style
Logic.Logic.Kripke.Preservation
Mathlib.Data.Nat.Cast.NeZero
Mathlib.Tactic.FBinop
Batteries.Data.Array.Lemmas
Mathlib.Tactic.NormNum.OfScientific
Mathlib.Algebra.Ring.Semiconj
Lake.Build
Mathlib.Data.Rat.Init
Mathlib.Order.Nat
Mathlib.Data.Nat.Order.Lemmas
Mathlib.Tactic.Contrapose
Logic.FirstOrder.Arith.Hierarchy
Lake.Config.LeanLib
Mathlib.Init.Data.Nat.Basic
Mathlib.Tactic.Ring.Basic
Logic.Modal.Hilbert
Lake.Util.Message
Mathlib.Algebra.Field.Basic
Aesop.Options.Internal
Lake.Build.Job
Mathlib.Data.Nat.Notation
Mathlib.Order.Filter.Pi
Mathlib.Logic.Function.ULift
Aesop.Search.Queue
Logic.Logic.Semantics
Mathlib.Algebra.Group.Commute.Units
Mathlib.Tactic.PPWithUniv
Incompleteness.Arith.D3
Mathlib.Algebra.Order.Field.Basic
Mathlib.Logic.Encodable.Basic
Lake.CLI.Actions
Mathlib.Data.Nat.Cast.Order.Basic
Aesop.Builder.Constructors
Mathlib.Computability.Halting
Mathlib.Logic.Function.Basic
ProofWidgets.Component.Basic
Logic.Logic.Kripke.RelItr
Lake.Util.JsonObject
Batteries.Lean.Util.EnvSearch
Mathlib.Tactic.Choose
Mathlib.Init.Data.List.Instances
Batteries.Data.UnionFind.Basic
Arithmetization.ISigmaOne.Metamath
Aesop.RuleSet.Name
Lake.Config.Monad
Mathlib.Data.List.OfFn
Logic.FirstOrder.Basic.BinderNotation
Mathlib.Data.List.Permutation
Logic.Vorspiel.Order
Logic.Modal.PLoN.PLoN
Mathlib.Tactic.Linter.OldObtain
Lake.Util.Store
Mathlib.Lean.Elab.Term
Logic.IntProp.Kripke.LEM
Arithmetization.ISigmaOne.Metamath.Language
Mathlib.Algebra.Group.Int
Mathlib.Data.List.Dedup
Arithmetization.Definability.Init
Mathlib.Order.Filter.Ultrafilter
Mathlib.Tactic.AdaptationNote
Lake.DSL.DeclUtil
Mathlib.Order.Basic
Mathlib.Order.Antichain
Mathlib.Order.RelIso.Basic
Mathlib.Algebra.Ring.InjSurj
Lake.DSL.Require
Batteries.Data.Fin.Lemmas
Arithmetization.ISigmaZero.Exponential.Log
Aesop.Tree.State
Mathlib.Logic.Nontrivial.Defs
Mathlib.GroupTheory.Perm.Basic
Mathlib.Tactic.ExistsI
Mathlib.Util.SynthesizeUsing
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Tactic.Widget.SelectPanelUtils
Aesop.Builder.Forward
Aesop.BuiltinRules.Ext
Mathlib.Order.SetNotation
Batteries.Util.ExtendedBinder
Arithmetization.ISigmaOne.HFS.Vec
Logic.Modal.Kripke.S5
Mathlib.Control.Functor
Mathlib.Data.FunLike.Basic
Mathlib.Order.Filter.AtTopBot
Logic.Logic.HilbertStyle.Context
Arithmetization.ISigmaOne.Metamath.Formula.Basic
Incompleteness.ProvabilityLogic.Basic
Logic.Modal.LogicSymbol
Logic.Propositional.Classical.Basic.Semantics
Mathlib.Algebra.GroupWithZero.Pi
Mathlib.Data.String.Defs
Mathlib.Tactic.ApplyFun
Mathlib.Order.Bounds.OrderIso
Mathlib.Tactic.ExtractGoal
Mathlib.Tactic.WLOG
Lake.Util.OrderedTagAttribute
Batteries.Data.Array.Init.Lemmas
Mathlib.Data.Int.Cast.Lemmas
Logic.Logic.HilbertStyle.Lukasiewicz
Arithmetization.ISigmaOne.Metamath.Proof.Thy
Arithmetization.ISigmaOne.Metamath.Formula.Typed
Logic.Modal.Kripke.GL.Completeness
Mathlib.Order.Interval.Finset.Defs
Aesop.Script.UScript
Mathlib.Algebra.Order.Sub.Defs
Mathlib.Algebra.Ring.Invertible
Arithmetization.OmegaOne.Basic
Mathlib.Data.Finset.Sort
Arithmetization.ISigmaOne.Metamath.Term.Basic
Mathlib.Data.Int.Sqrt
Lake.Util.Opaque
Lake.Config.Workspace
Batteries.Tactic.SqueezeScope
Logic.Logic.HilbertStyle.Supplemental
Aesop.RulePattern
Mathlib.Tactic.Nontriviality.Core
Mathlib.Logic.IsEmpty
Mathlib.Tactic.Simps.Basic
Mathlib.Logic.Equiv.Defs
Incompleteness.Arith.Second
ProofWidgets.Component.Recharts
Mathlib.Order.Interval.Set.UnorderedInterval
Logic.Modal.Boxdot.Boxdot
Mathlib.Logic.Function.Iterate
Lake.Toml.ParserUtil
Mathlib.Tactic.ProjectionNotation
Batteries.Data.Int.DivMod
Mathlib.Tactic.Inhabit
Logic.FirstOrder.Arith.Basic
Batteries.Data.BitVec.Lemmas
Mathlib.Algebra.Group.TypeTags
Batteries.Tactic.OpenPrivate
Aesop.Script.Main
Mathlib.Data.Multiset.Sort
Logic.Modal.PLoN.Soundness
Lake.Util.RBArray
Mathlib.Algebra.BigOperators.Group.Multiset
Batteries.Data.RBMap.Alter
Logic
Mathlib.Order.Hom.Basic
Mathlib.Algebra.Order.Ring.Rat
Mathlib.Tactic.SudoSetOption
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
Mathlib.Data.Option.Basic
Batteries.Lean.Util.Path
Aesop.Stats.Extension
Logic.FirstOrder.Completeness.SubLanguage
Lake.Util.DRBMap
Lake.Toml.Elab.Value
Logic.IntProp.Kripke.Completeness
Mathlib.Data.List.Infix
Aesop.RuleSet
Mathlib.Logic.Relator
ProofWidgets.Component.OfRpcMethod
Aesop.Tree.UnsafeQueue
Logic.FirstOrder.Order.Le
Arithmetization.Vorspiel.Graph
Mathlib.Data.Multiset.Lattice
Aesop.Script.CtorNames
Mathlib.Logic.Nonempty
Incompleteness.Arith.DC
Lake.Toml.Data.DateTime
Arithmetization.ISigmaOne.Metamath.Proof.Typed
Batteries.Data.Range.Lemmas
Aesop.Script.Check
Mathlib.Algebra.Group.WithOne.Defs
Mathlib.Algebra.SMulWithZero
Incompleteness.DC.Basic
Mathlib.Logic.Embedding.Set
Mathlib.Data.Int.Defs
Mathlib.Data.Subtype
Qq.SortLocalDecls
Batteries.Tactic.PrintDependents
Mathlib.Algebra.Order.Invertible
Batteries.Lean.Meta.Simp
Logic.FirstOrder.Basic.Eq
Lean
Mathlib.Data.Fintype.Sum
Mathlib.Logic.Function.Conjugate
Mathlib.Data.Multiset.FinsetOps
Mathlib.Logic.Godel.GodelBetaFunction
ProofWidgets.Component.Panel.GoalTypePanel
Mathlib.Algebra.Order.Monoid.Defs
Batteries.Control.Nondet.Basic
Mathlib.Data.FunLike.Equiv
Mathlib.Algebra.GroupWithZero.Hom
Mathlib.Tactic.TypeStar
Arithmetization.Definability.Absoluteness
Mathlib.Tactic.ExtractLets
Mathlib.Control.Traversable.Basic
Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Batteries.CodeAction.Misc
Arithmetization.ISigmaOne.HFS.Basic
Mathlib.Algebra.CharZero.Lemmas
Mathlib.Data.Finset.Union
Lake.Toml.Elab
Mathlib.Order.Closure
Mathlib.Order.WithBot
Logic.Vorspiel.Vorspiel
Logic.Modal.PLoN.Semantics
Mathlib.Algebra.BigOperators.Group.Finset
Batteries.Data.Int.Lemmas
Mathlib.Init.Classical
Mathlib.Tactic.Linarith.Parsing
Lake.Util.NativeLib
Mathlib.Algebra.Order.AbsoluteValue
Mathlib.Tactic.NormNum.DivMod
Mathlib.Algebra.Ring.CompTypeclasses
Batteries.Lean.Expr
Mathlib.Order.BooleanAlgebra
Batteries.Data.Int.Order
Lake.Config.Opaque
Mathlib.Data.Nat.Find
Mathlib.Algebra.Ring.Aut
Lake.Util.List
Aesop
Mathlib.Data.Finset.Card
Qq.ForLean.ToExpr
Arithmetization.ISigmaZero.Exponential.Pow2
Mathlib.Algebra.Group.Units
Logic.IntProp.Kripke.Semantics
Mathlib.Tactic.Spread
Batteries.Data.Option.Lemmas
Mathlib.Algebra.Group.Indicator
Mathlib.Tactic.NormNum
Mathlib.Data.Set.Sigma
Mathlib.Data.Set.List
Mathlib.Algebra.Order.AddGroupWithTop
Mathlib.Algebra.Group.Pi.Basic
Mathlib.Order.Max
Mathlib.Tactic.Observe
Batteries.Data.Nat.Basic
Arithmetization.ISigmaOne.Bit
Mathlib.Control.Combinators
Batteries.Tactic.SeqFocus
Mathlib.Data.Bracket
Mathlib.Data.Rat.Defs
Aesop.Saturate
Aesop.Script.StructureStatic
Logic.FirstOrder.Completeness.Coding
Mathlib.Tactic.Linter.GlobalAttributeIn
Mathlib.Data.Set.NAry
Mathlib.Data.Multiset.Pi
Logic.Logic.Axioms
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Data.Int.Cast.Basic
Mathlib.Order.Hom.Bounded
Mathlib.Data.Finset.Preimage
Mathlib.Data.List.Lattice
ProofWidgets.Component.MakeEditLink
Batteries.Tactic.Lint.Frontend
Lake.Toml.Elab.Expression
Mathlib.Tactic.FailIfNoProgress
Qq.Match
Mathlib.Logic.Equiv.Set
Aesop.Util.Tactic.Ext
Lake.Util.Cycle
Mathlib.Algebra.Group.Action.Opposite
Mathlib.Tactic.Attr.Register
Mathlib.Tactic.Conv
Mathlib.Init.Data.Ordering.Basic
Aesop.Options.Public
Mathlib.Algebra.Order.Ring.Unbundled.Basic
Batteries.Data.RBMap.Lemmas
Batteries.Lean.Meta.Expr
Mathlib.Algebra.Regular.Basic
Mathlib.Algebra.Order.Group.Unbundled.Basic
ProofWidgets.Compat
Lake.Config.Glob
Aesop.Script.OptimizeSyntax
Mathlib.Tactic.CongrM
Mathlib.Logic.Equiv.Option
Mathlib.Algebra.Order.BigOperators.Ring.List
Lake.Util.StoreInsts
Aesop.Tree.Free
Aesop.Tree.ExtractScript
Mathlib.Util.WithWeakNamespace
Mathlib.Tactic.GuardGoalNums
Batteries.Lean.Meta.Inaccessible
Qq.Delab
Logic.Vorspiel.BinaryRelations
Mathlib.Order.Filter.Prod
Mathlib.Algebra.Ring.Opposite
Mathlib.Order.Interval.Set.OrdConnected
Mathlib.Tactic.NthRewrite
Aesop.BuiltinRules.Split
Logic.Logic.Init
Batteries.Tactic.Unreachable
Mathlib.Tactic.HigherOrder
Mathlib.Order.Interval.Set.OrderIso
Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Mathlib.GroupTheory.GroupAction.Units
Logic.Logic.Kripke.Closure
Mathlib.Tactic.Set
Mathlib.Tactic.IrreducibleDef
Mathlib.Algebra.Order.Group.Instances
Mathlib.Init.Data.Sigma.Basic
Batteries.Data.Array
Mathlib.Order.MinMax
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
Aesop.Search.Queue.Class
Batteries.Data.RBMap.WF
Mathlib.Algebra.Order.GroupWithZero.Canonical
Batteries.Logic
Logic.Modal.ModalCompanion.ModalCompanion
Mathlib.Algebra.Module.Defs
Mathlib.Tactic.Widget.Conv
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Mathlib.Logic.Denumerable
Mathlib.Order.Interval.Set.OrderEmbedding
Lake.Build.Facets
Logic.Modal.Kripke.Dot3
Batteries.Tactic.Lint.Basic
Mathlib.Init.Data.List.Lemmas
Mathlib.Algebra.Divisibility.Basic
Mathlib.Data.PNat.Equiv
Lake.Util.Git
Mathlib.Order.Filter.Bases
Lake.Version
ProofWidgets
Mathlib.Data.List.Forall2
Lake.Config.FacetConfig
Mathlib.Combinatorics.Colex
Aesop.Search.Expansion
Mathlib.Tactic.Find
Mathlib.Tactic.Recover
Mathlib.Algebra.Group.Units.Equiv
Aesop.Script.TacticState
Mathlib.Data.List.Sublists
Mathlib.Tactic.Basic
Aesop.RuleTac.Basic
Mathlib.Algebra.Order.Group.MinMax
Mathlib.Tactic.ApplyAt
Aesop.Script.UScriptToSScript
Logic.IntProp.Kripke.Kripke
Batteries.Data.Bool
Mathlib.Lean.Expr.ReplaceRec
Batteries.Data.RBMap.Depth
Batteries.Linter.UnreachableTactic
ProofWidgets.Component.InteractiveSvg
Aesop.Search.Expansion.Simp
Aesop.Stats.Report
Aesop.ElabM
Arithmetization.ISigmaOne.Metamath.Term.Typed
Lake.Build.Module
Mathlib.Init.Data.Quot
Batteries.Data.Rat
Batteries.Tactic.Lint.Misc
Lake.Config.ExternLibConfig
Mathlib.Data.Quot
Batteries.Lean.System.IO
Mathlib.Data.Multiset.Powerset
Mathlib.Tactic.CC.Lemmas
Mathlib.Tactic.TypeCheck
Lake.Build.Basic
ProofWidgets.Component.PenroseDiagram
Mathlib.Data.Finite.Defs
Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Batteries.Linter
Mathlib.Data.List.MinMax
Mathlib.Algebra.Ring.Parity
Logic.Logic.System
Mathlib.Order.Cover
Logic.Modal.Boxdot.GL_Grz
Batteries.Data.Array.Match
Mathlib.Tactic.DefEqTransformations
Mathlib.Algebra.Group.InjSurj
Lake.Config.LeanExeConfig
Batteries.Data.MLList
Mathlib.Order.Interval.Finset.Nat
Lake.Config.LeanExe
Mathlib.Algebra.Star.Rat
Batteries.Data.List.Init.Attach
Mathlib.Algebra.Order.BigOperators.Group.Multiset
Mathlib.Data.Countable.Defs
Logic.Modal.ConsistentTheory
Mathlib.Tactic.SimpIntro
Batteries.Data.List.Basic
Logic.Vorspiel.ExistsUnique
Lake.Config.LeanConfig
Mathlib.Data.Finset.Lattice
Batteries.Util.Cache
Logic.Vorspiel.Collection
Mathlib.Logic.Equiv.Fin
Mathlib.Init.Data.List.Basic
Arithmetization.ISigmaOne.Metamath.Formula.Functions
Batteries.Util.LibraryNote
Mathlib.Algebra.Order.Nonneg.Field
Mathlib.Lean.Meta.Simp
Arithmetization.ISigmaOne.Metamath.Coding
Mathlib.Algebra.Order.Ring.Defs
Arithmetization.ISigmaOne.Metamath.CodedTheory
Mathlib.Tactic.CancelDenoms.Core
Batteries.Data.MLList.Heartbeats
Batteries.Data.RBMap.Basic
Mathlib.Tactic.Nontriviality
Mathlib.Algebra.Divisibility.Units
Logic.FirstOrder.Completeness.Completeness
Mathlib.Data.Nat.Cast.Field
Mathlib.Tactic.GuardHypNums
Mathlib.Init.Order.LinearOrder
Mathlib.Algebra.Order.Ring.Nat
Mathlib.Tactic.Hint
Batteries.Data.Fin.Basic
Mathlib.Algebra.Group.Semiconj.Basic
Lake.Build.Store
Mathlib.Algebra.Order.Group.PosPart
Mathlib.Lean.PrettyPrinter.Delaborator
Mathlib.Logic.Nontrivial.Basic
Mathlib.Algebra.Order.Group.Nat
Logic.FirstOrder.Arith.CobhamR0
Logic.Logic.LogicSymbol
Mathlib.Data.Nat.Factorial.Basic
Mathlib.Data.Fin.VecNotation
Mathlib.Data.Finset.Image
Batteries.Tactic.Congr
Batteries.Util.ProofWanted
Mathlib.Algebra.Group.Pi.Lemmas
Lake.DSL.Targets
Mathlib.Order.Bounds.Basic
Batteries.Tactic.Exact
Mathlib.Tactic.Trace
Mathlib.Data.List.FinRange
Mathlib.Algebra.Group.Conj
Mathlib.Tactic.CC
Lake.Util.EquipT
Mathlib.Tactic.Widget.Calc
Mathlib.Data.List.Lex
Mathlib.Data.List.ProdSigma
Mathlib.Lean.EnvExtension
Mathlib.Data.Option.NAry
Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Lake.Toml.Grammar
Mathlib.Algebra.Order.Nonneg.Ring
Mathlib.Order.Disjoint
Mathlib.Algebra.Group.Aut
ProofWidgets.Presentation.Expr
Mathlib.Tactic.NormNum.Basic
Mathlib.Algebra.Group.Nat
Lake.Config.LeanLibConfig
Mathlib.Order.Notation
Logic.Propositional.Classical.Basic.Calculus
Mathlib.Tactic.ClearExcept
Aesop.Rule
Mathlib.Order.Filter.Ker
Batteries.Data.String.Lemmas
Logic.FirstOrder.Basic.Syntax.Term
Aesop.Search.Expansion.Norm
Mathlib.Algebra.Order.Group.Lattice
Aesop.BuiltinRules.DestructProducts
Batteries.Lean.PersistentHashSet
Batteries.Lean.Meta.Clear
Mathlib.Algebra.Group.Even
Logic.FirstOrder.Basic.Calculus
Mathlib.Algebra.GroupWithZero.NeZero
Batteries.Lean.Syntax
Mathlib.Tactic.ApplyCongr
Mathlib.Tactic.Clear_
Aesop.Tree.AddRapp
Mathlib.Order.Atoms
Batteries.Lean.TagAttribute
Batteries.Data.Sum.Basic
Mathlib.Algebra.GroupWithZero.Invertible
Mathlib.Util.CountHeartbeats
Incompleteness.ToFoundation.Basic
Aesop.Tracing
Mathlib.Data.Set.Notation
Mathlib.Data.Int.Cast.Field
Batteries.Lean.Except
Batteries.Control.ForInStep.Basic
Logic.Propositional.Classical.Basic.Formula
Batteries.Data.HashMap
Mathlib.Data.List.Perm
Batteries.Tactic.Alias
Mathlib.Order.CompleteBooleanAlgebra
Aesop.Tree.Check
Mathlib.Algebra.Group.Action.Prod
Arithmetization.OmegaOne.Nuon
Batteries.Lean.Meta.DiscrTree
Batteries.Data.List.Count
Aesop.RuleTac.Preprocess
Batteries.Linter.UnnecessarySeqFocus
Mathlib.Tactic.Linarith.Frontend
Batteries.Data.UnionFind.Lemmas
Arithmetization.Definability.BoundedBoldface
Mathlib.Order.ConditionallyCompleteLattice.Basic
Mathlib.Util.Tactic
Mathlib.Data.Rel
Lake.Build.Library
Mathlib.Data.Fintype.Card
Lake.Util.Lift
Logic.Propositional.Classical.Basic.Completeness
Qq.Macro
Mathlib.Tactic.Linarith.Verification
Batteries.Classes.Cast
Batteries.Tactic.NoMatch
Lake.Util.Casing
Mathlib.Algebra.Order.Ring.Abs
Aesop.Main
Aesop.Constants
Mathlib.Algebra.Group.Subsemigroup.Operations
Mathlib.Algebra.Ring.Basic
Mathlib.Algebra.Group.Submonoid.Operations
Lake.Util.Name
Arithmetization.ISigmaOne.HFS
Aesop.Frontend
Batteries.Classes.Order
Logic.Modal.Kripke.GL.MDP
Mathlib.Tactic.Relation.Symm
Mathlib.Data.List.Sort
Aesop.Tree.Data
Mathlib.Algebra.Group.Semiconj.Units
Batteries.Data.Sum
Logic.Logic.Calculus
Batteries.Data.DList
Batteries.Tactic.Basic
Mathlib.Order.PropInstances
Logic.FirstOrder.Basic.Syntax.Rew
Mathlib.Order.Interval.Set.Image
Mathlib.Tactic.Tauto
Mathlib.Data.Finset.Attr
Aesop.Rule.Name
Aesop.Search.RuleSelection
Mathlib.Order.Minimal
Aesop.Util.UnorderedArraySet
Mathlib.Algebra.Order.BigOperators.Group.Finset
Mathlib.Algebra.Order.GroupWithZero.Unbundled
Mathlib.Data.Prod.PProd
Batteries.Data.Int
Aesop.Frontend.RuleExpr
Aesop.Index
Mathlib.Util.AtomM
Logic.FirstOrder.Basic.Syntax.Language
ProofWidgets.Component.Panel.Basic
Mathlib.Algebra.Order.Interval.Finset
Aesop.Frontend.Saturate
Aesop.Frontend.Tactic
Mathlib.Data.Finset.Pi
Mathlib.Data.Set.Basic
Aesop.BuiltinRules.Intros
Batteries.Data.Array.Merge
Batteries.Data.RBMap
Lake.Toml
Mathlib.Order.Lattice
Lake.Build.Package
Mathlib.Order.Synonym
Batteries.Data.List.EraseIdx
Logic.Modal.ModalCompanion.GMT
Batteries.Data.ByteArray
Batteries.Data.AssocList
Mathlib.Algebra.NeZero
Mathlib.Lean.Meta
Lake.Config.Dependency
Lake.Util.Compare
Mathlib.Data.Nat.Pairing
Mathlib.Data.Prod.Basic
Mathlib.Algebra.Ring.Rat
Mathlib.Data.Nat.Cast.Basic
Mathlib.Tactic.Positivity.Core
Mathlib.Algebra.Order.Monoid.Basic
Batteries.Data.List
Mathlib.Algebra.Ring.Action.Group
Mathlib.Data.List.Join
Mathlib.Data.Set.Countable
Mathlib.Data.PNat.Basic
Mathlib.Data.Set.Defs
Mathlib.Tactic.Constructor
Mathlib.Data.Vector.Basic
Mathlib.Tactic.Cases
Aesop.Builder.Tactic
Mathlib.Data.Fintype.Sigma
Lake.Config.Env
Batteries.Data.Array.Monadic
Mathlib.Tactic.CC.Addition
Logic.FirstOrder.Arith.Nonstandard
Arithmetization.ISigmaOne.Metamath.Formula.Iteration
Mathlib.Algebra.Order.Ring.Unbundled.Nonneg
Mathlib.Algebra.Order.Ring.Basic
Arithmetization.Definability.Boldface
Mathlib.Algebra.Ring.Defs
Mathlib.Data.Int.CharZero
Arithmetization.ISigmaOne.Metamath.Term.Functions
Lake.Toml.Load
Batteries.Lean.HashSet
Qq.Typ
Mathlib.Tactic.MkIffOfInductiveProp
Logic.Modal.Kripke.GL.Tree
Mathlib.Util.WhatsNew
Aesop.RuleSet.Filter
Logic.Modal.Kripke.Grz.Completeness
Mathlib.Data.Fin.Tuple.Basic
Logic.IntProp.Formula
Mathlib.Data.Fintype.Prod
Mathlib.Algebra.Order.Group.Int
Aesop.Script.StructureDynamic
Batteries.Data.BitVec
Mathlib.Tactic.ScopedNS
Logic.FirstOrder.Basic.Semantics.Elementary
Aesop.Search.Main
Batteries.Data.HashMap.WF
Mathlib.Algebra.Group.Action.Defs
Mathlib.Algebra.Group.Hom.Instances
Mathlib.Algebra.Order.Monoid.OrderDual
Mathlib.Order.GaloisConnection
Mathlib.Data.List.Nodup
Arithmetization.Definability.Hierarchy
Logic.Modal.Geach
Mathlib.Computability.PartrecCode
Incompleteness.Arith.FormalizedArithmetic
Mathlib.Algebra.Group.Units.Hom
Batteries.Data.BinomialHeap.Lemmas
Mathlib.Algebra.Order.Monoid.Unbundled.Defs
ProofWidgets.Data.Html
Aesop.Builder.Basic
Logic.Propositional.Classical.Basic
Mathlib.Order.CompleteLattice
Mathlib.Algebra.Group.Commute.Defs
Mathlib.Algebra.Order.Positive.Ring
Mathlib.Algebra.Field.Opposite
Mathlib.Algebra.Order.Field.Rat
Mathlib.Tactic.NormNum.Inv
Mathlib.Order.BoundedOrder
Batteries.Data.String.Matcher
Mathlib.Algebra.Order.BigOperators.Ring.Finset
Mathlib.Algebra.Group.Equiv.Basic
Mathlib.Tactic.Zify
Lake.Config.Context
Mathlib.Algebra.Ring.Nat
Logic.FirstOrder.Basic.Semantics.Semantics
Aesop.Script.Tactic
Lake.Util.Error
Mathlib.Algebra.BigOperators.Ring
Mathlib.Data.Finset.Powerset
Mathlib.Order.Monotone.Basic
Mathlib.Lean.Expr.Basic
Mathlib.Order.SymmDiff
Mathlib.Logic.Unique
Mathlib.Tactic.Propose
Mathlib.Algebra.BigOperators.Group.List
Mathlib.Tactic.Linarith
Mathlib.Data.Nat.Defs
Mathlib.Data.Nat.PSub
Logic.Modal.PLoN.Completeness
Mathlib.Data.Set.Finite
Lake.Config.ExternLib
Batteries.Lean.Meta.Basic
Mathlib.Algebra.Order.Ring.Canonical
Mathlib.Tactic.RenameBVar
Aesop.Frontend.Command
Mathlib.Lean.Expr.ExtraRecognizers
Mathlib.Algebra.Order.Monoid.NatCast
Mathlib.Tactic.PushNeg
Lake.Build.Data
Lake.Build.Info
Mathlib.Data.Bool.Set
Batteries.Util.Pickle
Mathlib.Algebra.BigOperators.Intervals
Batteries.Data.HashMap.Lemmas
Aesop.Tree.Traversal
Mathlib.Data.List.Defs
Mathlib.Data.Rat.Lemmas
Mathlib.Algebra.Order.Monoid.TypeTags
Aesop.BuiltinRules.Assumption
Mathlib.Algebra.Order.Ring.Cast
Mathlib.Data.Multiset.Sum
Mathlib.Order.Interval.Finset.Basic
Mathlib.Data.Multiset.Bind
Batteries.Data.Range
Logic.Modal.Kripke.Grz.Grz
Mathlib.Lean.Meta.CongrTheorems
Mathlib.Algebra.GroupWithZero.Units.Equiv
Mathlib.Algebra.BigOperators.Ring.List
Mathlib.Tactic.Widget.SelectInsertParamsClass
Lake.Util.Sugar
Mathlib.Data.Rat.Cast.Order
ProofWidgets.Component.FilterDetails
Lake.Util.Binder
Lake.Config
Logic.Modal.Kripke.Grz.Definability
Logic.Modal.Kripke.Kripke
Mathlib.Algebra.Star.Basic
Arithmetization.ISigmaOne.HFS.PRF
Mathlib.Data.Nat.Choose.Basic
Mathlib.Tactic.ByContra
Logic.Modal.Kripke.Geach
Mathlib.Tactic.Relation.Rfl
Mathlib.Tactic.Convert
Mathlib.Order.Fin
Batteries.Data.PairingHeap
Mathlib.Algebra.Order.Hom.Basic
Mathlib.Data.Finset.Fold
Mathlib.Data.Multiset.Nodup
Batteries.Data.String
Lake.Toml.Data.Value
Mathlib.Tactic.HelpCmd
Mathlib.Data.List.Zip
Mathlib.Control.ULift
Mathlib.Data.Countable.Basic
Lake.Util.Exit
Logic.FirstOrder.Basic
Batteries.CodeAction
Mathlib.Init.Order.Defs
Aesop.Tree.RunMetaM
Arithmetization.Vorspiel.Vorspiel
Mathlib.Tactic.ToExpr
Batteries.Lean.HashMap
Mathlib.Algebra.GroupWithZero.Divisibility
Mathlib.Data.PNat.Defs
Arithmetization.ISigmaOne.HFS.Fixpoint
Batteries.Lean.MonadBacktrack
Mathlib.Tactic.CongrExclamation
Lake.Build.Run
Mathlib.Tactic.Lift
Logic.Modal.Kripke.ComplexityLimited
Mathlib.Algebra.Group.Commute.Basic
Batteries.Tactic.Lint.Simp
Mathlib.Data.Nat.BitIndices
Logic.Modal.Kripke.Completeness
Mathlib.Algebra.Star.StarRingHom
Aesop.Check
Lake.Util.Log
Aesop.Percent
Mathlib.Data.Int.Notation
Batteries.Lean.PersistentHashMap
Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Logic.Equiv.Basic
Lake.DSL.Attributes
Mathlib.Algebra.Group.Embedding
Mathlib.Order.Filter.Cofinite
Aesop.Tree.Tracing
Mathlib.Data.Fintype.List
Mathlib.Data.Finset.Sum
Batteries.Tactic.ShowUnused
Mathlib.Algebra.Associated.Basic
Aesop.Script.Util
Lake.DSL.AttributesCore
Batteries.Data.Option
Mathlib.Order.CompleteLatticeIntervals
Batteries.Lean.Json
Batteries.Data.BinomialHeap.Basic
Mathlib.Tactic.Variable
Aesop.Index.Basic
Mathlib.Data.Sigma.Basic
Mathlib.Algebra.Group.Hom.Basic
Mathlib.Data.Nat.Cast.Order.Ring
Batteries.Data.UnionFind
Mathlib.Algebra.Star.Order
Mathlib.Logic.Embedding.Basic
Aesop.Script.ScriptM
Batteries.Lean.Meta.InstantiateMVars
Mathlib.Tactic.Check
Mathlib.GroupTheory.GroupAction.Defs
Mathlib.Algebra.Ring.Int
Mathlib.Order.SupClosed
Mathlib.Tactic.Ring.PNat
Lake.Config.Package
Mathlib.Algebra.Group.Support
Mathlib.Algebra.Group.Prod
Mathlib.Data.Multiset.Sections
Mathlib.Data.Fintype.Powerset
Aesop.Util.EqualUpToIds
Mathlib.Logic.Pairwise
Mathlib.Order.Directed
Mathlib.Tactic.Linarith.Lemmas
Batteries.CodeAction.Basic
Mathlib.Algebra.Ring.Divisibility.Basic
Mathlib.Init.Quot
Mathlib.Data.Nat.GCD.Basic
Aesop.BuiltinRules
Mathlib.Data.Fintype.Vector
Mathlib.Data.List.Duplicate
Mathlib.Tactic.NormNum.Core
Mathlib.Tactic.RSuffices
Batteries.Data.BinomialHeap
Logic.Modal.Kripke.GL.Definability
Arithmetization
Mathlib.Tactic.Substs
Batteries.Lean.Delaborator
Lake.CLI.Build
Mathlib.Order.Heyting.Basic
Mathlib.Tactic.Positivity.Basic
Batteries.Data.List.Init.Lemmas
Mathlib.Algebra.GeomSum
Mathlib.Logic.Equiv.List
Lake.Build.Imports
Mathlib.Algebra.Group.Opposite
Mathlib.Algebra.GroupWithZero.InjSurj
Mathlib.Init.Algebra.Classes
Logic.Logic.Disjunctive
Aesop.Frontend.Attribute
Aesop.RuleTac.Forward
Logic.Logic.Kripke.Basic
Mathlib.Util.AssertExists
Batteries.Control.ForInStep
Aesop.Search.ExpandSafePrefix
Lake.Build.Actions
Mathlib.Data.List.Chain
Logic.Modal.Kripke.Semantics
Logic.Modal.Maximal
Lake.Build.Fetch
Mathlib.Algebra.Group.Action.Basic
Mathlib.Algebra.Star.Pi
Lake.Util.EStateT
Mathlib.Algebra.Group.Semiconj.Defs
Batteries.Tactic.Lint.TypeClass
Lake.Load.Config
Mathlib.Data.Finset.Option
Aesop.Util.Basic
Qq.ForLean.Do
Mathlib.Data.Multiset.Dedup
Batteries.Lean.IO.Process
Aesop.Builder.Apply
Mathlib.Order.ModularLattice
Logic.FirstOrder.Basic.Model
Mathlib.Algebra.Group.Basic
Logic.Modal.Boxdot.Basic
Logic.FirstOrder.Arith.Representation
Logic.Modal.Modal
Mathlib.Algebra.GroupPower.IterateHom
ProofWidgets.Component.Panel.SelectionPanel
Mathlib.Data.Setoid.Basic
ProofWidgets.Util
Mathlib.Tactic.TermCongr
Mathlib.Algebra.GroupWithZero.Prod
Mathlib.Algebra.Group.Subgroup.Basic
Aesop.Util.UnionFind
Mathlib.Tactic.NormNum.Ineq
Mathlib.Data.Multiset.Antidiagonal
Mathlib.Order.RelIso.Set