Documentation
Init
Search
return to top
source
Imports
Init.BinderNameHint
Init.BinderPredicates
Init.ByCases
Init.Control
Init.Conv
Init.Core
Init.Data
Init.Dynamic
Init.Ext
Init.Grind
Init.Guard
Init.Hints
Init.Internal
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.Try
Init.Util
Init.WF
Init.WFTactics
Init.While
Init.Data.Basic
Imported by
Foundation.Logic.HilbertStyle.Basic
Mathlib.Tactic.Zify
Mathlib.Util.TermReduce
Foundation.Propositional.Kripke.Hilbert.LC
Foundation.Vorspiel.Relation.Supplemental
Mathlib.Order.Basic
Mathlib.Tactic.FBinop
Mathlib.Algebra.Order.Nonneg.Basic
Foundation.Modal.Kripke.Hilbert.Geach
Mathlib.Order.Notation
Aesop.Forward.RuleInfo
Foundation.FirstOrder.Arith.CobhamR0
Foundation.Logic.Disjunctive
Mathlib.Algebra.GeomSum
Mathlib.Algebra.Order.Ring.Unbundled.Rat
Foundation.Modal.Kripke.Hilbert.K4
Mathlib.Tactic.Ring.RingNF
Aesop.RuleSet.Member
Aesop.Constants
Foundation.Propositional.Kripke.AxiomDummett
Mathlib.Data.Int.Cast.Pi
Mathlib.Order.Hom.Bounded
Mathlib.Data.Sym.Basic
Aesop.Builder.Cases
Foundation.Modal.Kripke.Undefinability
Mathlib.Data.Multiset.Sort
Batteries.Tactic.Basic
Mathlib.Data.Prod.Basic
Aesop.Rule
Mathlib.Data.Finset.Attach
Mathlib.Algebra.BigOperators.Group.List.Lemmas
Foundation.Arithmetization.ISigmaOne.Metamath.Term.Functions
Qq.SortLocalDecls
Aesop.Script.Main
Foundation.Modal.Kripke.Hilbert.KT4B
Mathlib.Data.Int.Cast.Field
Foundation.Propositional.ClassicalSemantics.Basic
Mathlib.Data.Finset.Filter
Foundation.Modal.Kripke.Hilbert.S4Point2
Mathlib.Data.List.TFAE
Mathlib.Data.Nat.Notation
Foundation.Logic.LogicSymbol
Mathlib.Data.List.Lemmas
Foundation.FirstOrder.Basic.Semantics.Elementary
Mathlib.Tactic.Cases
Foundation.AutoProver.Classical
Mathlib.Order.Filter.Prod
Foundation.Arithmetization.ISigmaOne.Metamath.Formula.Functions
Mathlib.Tactic.Linter.UpstreamableDecl
Mathlib.Data.PNat.Equiv
Mathlib.Tactic.TypeStar
Mathlib.Data.List.TakeDrop
Foundation.Incompleteness.DC.Basic
Mathlib.Data.PFun
Batteries.Tactic.Lint.Basic
Batteries.Tactic.SeqFocus
Foundation.Modal.Kripke.Hilbert.S4Point3
Aesop.Builder.Unfold
Mathlib.Tactic.Trace
Mathlib.Algebra.Order.Ring.Unbundled.Basic
Mathlib.Data.Fintype.Vector
Mathlib.Tactic.SudoSetOption
Mathlib.Data.List.MinMax
Mathlib.Algebra.Order.Sub.Defs
Foundation.Arithmetization.ISigmaOne.Metamath.Term.Basic
Mathlib.Data.Int.Cast.Lemmas
Mathlib.Order.Interval.Set.Disjoint
Aesop.Forward.LevelIndex
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
Foundation.Propositional.Entailment.Basic
Foundation.FirstOrder.Arith.Theory
Mathlib.Data.Set.Disjoint
Mathlib.Tactic.OfNat
Mathlib.Lean.Expr.Rat
Mathlib.Logic.Denumerable
Mathlib.Algebra.Ring.Units
Batteries.Lean.Meta.DiscrTree
Mathlib.Tactic.Relation.Rfl
Mathlib.Data.Fin.Rev
Foundation.Modal.Kripke.Closure
Mathlib.Algebra.Group.Action.Defs
Foundation.Arithmetization.OmegaOne.Nuon
Mathlib.Algebra.Group.Semiconj.Defs
Mathlib.Order.Filter.Basic
Mathlib.Data.Tree.Basic
Mathlib.Lean.Meta.CongrTheorems
Mathlib.Algebra.Group.Nat.Hom
Foundation.Modal.Logic.Sublogic.Trivials
Mathlib.Order.BooleanAlgebra
Mathlib.Tactic.StacksAttribute
Foundation.Propositional.Entailment.Cl
Aesop.Frontend.Extension
Mathlib.Data.Countable.Defs
Aesop.Script.Step
Mathlib.Data.List.Perm.Basic
Foundation.Modal.Logic.Basic
Aesop.Util.EqualUpToIds
Mathlib.Logic.Unique
Mathlib.Algebra.GroupWithZero.Defs
Mathlib.Tactic.InferParam
Mathlib.Computability.PartrecCode
Mathlib.Tactic.DefEqTransformations
Aesop.Stats.Basic
Mathlib.Algebra.Order.BigOperators.Group.List
Mathlib.Algebra.Ring.Regular
Mathlib.Logic.Function.DependsOn
Mathlib.Logic.Nontrivial.Basic
Mathlib.Data.List.Permutation
Mathlib.Tactic.Bound.Init
Mathlib.Order.Filter.Defs
Mathlib.Algebra.Group.Even
Aesop.RuleTac.FVarIdSubst
Mathlib.Algebra.Group.Int.Units
Mathlib.Tactic.ScopedNS
Mathlib.Tactic.Positivity.Basic
Foundation.FirstOrder.Completeness.Completeness
Foundation.Propositional.Kripke.Preservation
Mathlib.Logic.ExistsUnique
Aesop.Frontend.Basic
Mathlib.Order.Filter.Ultrafilter.Defs
Mathlib.Data.List.ProdSigma
Foundation.Modal.Kripke.Hilbert.KB5
Mathlib.Algebra.Group.Units.Defs
Mathlib.Tactic.GeneralizeProofs
Aesop.Options.Internal
Mathlib.Data.Multiset.Fold
Mathlib.Data.Set.Prod
Mathlib.Data.Finset.SDiff
Aesop.Forward.State
Foundation.Arithmetization.ISigmaOne.HFS.Coding
Mathlib.Logic.Pairwise
Mathlib.Tactic.Recover
Mathlib.Data.Finset.Lattice.Prod
Mathlib.Algebra.Ring.Int.Units
Foundation.Propositional.Kripke.Hilbert.Cl
Mathlib.Data.List.Count
Foundation.Modal.Kripke.Hilbert.Grz.Soundness
Qq.ForLean.Do
Mathlib.Data.Multiset.FinsetOps
Mathlib.Util.AtomM
Mathlib.Tactic.Substs
Mathlib.Order.Heyting.Basic
Mathlib.Data.Nat.Sqrt
Aesop.Builder.NormSimp
Mathlib.Algebra.Group.Int.Even
Mathlib.Data.Finset.Attr
Mathlib.Data.List.Nodup
Foundation.Vorspiel.Relation.CWF
Foundation.Propositional.Hilbert.WellKnown
Mathlib.Logic.Relator
Mathlib.Algebra.GroupWithZero.Basic
Mathlib.Data.Int.Cast.Defs
Mathlib.Algebra.Order.Monoid.Basic
Mathlib.Tactic.DeprecateTo
Mathlib.Tactic.Linter.FlexibleLinter
Foundation.Modal.Complement
Mathlib.Data.List.OfFn
Aesop.Script.StructureDynamic
Mathlib.Data.Nat.ChineseRemainder
Mathlib.Tactic.Variable
Batteries.Data.NameSet
Mathlib.Data.Nat.Cast.Order.Basic
Foundation.Modal.Boxdot.GL_Grz
Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Mathlib.Tactic.Find
Aesop.Tree.Traversal
Mathlib.Data.Finset.Insert
Aesop.Index.RulePattern
Mathlib.Data.Nat.GCD.BigOperators
Batteries.Lean.AttributeExtra
Foundation.Incompleteness.Arith.Theory
Mathlib.Algebra.CharZero.Defs
Foundation.Meta.Kite.Generator
Mathlib.Data.Fintype.OfMap
Mathlib.Data.Bool.Basic
Foundation.Modal.ModalCompanion.Cl
Foundation.Modal.PLoN.Hilbert.N
Mathlib.Order.Nat
Foundation.Modal.Kripke.AxiomVer
Mathlib.Data.List.Infix
Foundation.Modal.Entailment.GL
Mathlib.Algebra.Order.Ring.Abs
Mathlib.Order.Cover
Mathlib.Tactic.Nontriviality
Mathlib.Data.Multiset.Count
Batteries.Data.Rat.Basic
ProofWidgets.Util
Mathlib.Algebra.Group.Invertible.Basic
Aesop.Frontend.Saturate
Mathlib.Data.List.Dedup
Mathlib.Data.Nat.GCD.Basic
Foundation.FirstOrder.Basic.Padding
Aesop.BuiltinRules.Intros
Batteries.Data.String.Basic
Mathlib.Data.Nat.Set
Batteries.Util.ExtendedBinder
Mathlib.Algebra.Order.Group.PosPart
Mathlib.Data.Finset.Prod
Foundation.ProvabilityLogic.GL.Soundness
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Foundation.Incompleteness.Arith.First
Foundation.FirstOrder.Basic.Operator
Batteries.Tactic.HelpCmd
Aesop.BuiltinRules.Assumption
Foundation.Modal.MaximalConsistentSet
Mathlib.Algebra.Order.GroupWithZero.Unbundled
Mathlib.Order.Interval.Set.WithBotTop
Mathlib.Data.Fintype.Powerset
Mathlib.Data.Fin.VecNotation
Plausible.Random
Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Order.Closure
Aesop.Index.Forward
Mathlib.Algebra.Group.Basic
Mathlib.Order.Bounds.Defs
Mathlib.Data.Nat.Cast.NeZero
Mathlib.Algebra.Opposites
Mathlib.Algebra.Order.Field.Defs
Aesop.Tree.State
Mathlib.Data.Multiset.MapFold
Mathlib.Data.List.InsertIdx
Batteries.Data.List.Pairwise
Batteries.Lean.Except
Mathlib.Data.Fintype.Sigma
Mathlib.Tactic.Use
Plausible.Attr
Mathlib.Tactic.Linter.DocString
Mathlib.Algebra.Group.Indicator
Batteries.Lean.Meta.Basic
Foundation.Propositional.Axioms
Mathlib.Data.Finset.Sum
Mathlib.Logic.Function.Conjugate
Mathlib.Algebra.Order.Ring.Defs
Mathlib.Order.RelClasses
Mathlib.Algebra.Order.Nonneg.Field
Foundation.Propositional.Kripke.Basic
Aesop.Tree.TreeM
Mathlib.Algebra.Order.Interval.Finset.Basic
Foundation.Modal.Kripke.Hilbert.KT
Mathlib.Algebra.GroupWithZero.Associated
Foundation.Modal.LogicSymbol
Foundation.FirstOrder.Ultraproduct
Batteries.Linter.UnnecessarySeqFocus
Aesop.RuleSet.Filter
Mathlib.Order.Fin.Basic
Mathlib.Tactic.ApplyAt
Batteries.Tactic.Trans
Foundation.Modal.Kripke.NNFormula
Mathlib.Tactic.ToAdditive
Mathlib.Tactic.Coe
Mathlib.Data.Finset.Sort
Mathlib.Order.SuccPred.Basic
Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Batteries.Util.ProofWanted
Mathlib.Logic.Encodable.Basic
Batteries.Data.List.Init.Lemmas
Mathlib.Tactic.Says
Foundation.FirstOrder.Completeness.SearchTree
Aesop.BuiltinRules
Foundation.Logic.Entailment
Mathlib.Algebra.BigOperators.Ring.Finset
Foundation.Modal.Kripke.AxiomGrz
Mathlib.Tactic.NormNum.Pow
Mathlib.Tactic.TautoSet
Mathlib.Tactic.Set
Mathlib.Algebra.Group.Hom.Basic
Batteries.CodeAction.Misc
Foundation.Vorspiel.Relation.WCWF
Aesop.Tree.Free
Foundation.Logic.Predicate.Rew
Mathlib.Data.PNat.Notation
Mathlib.Tactic.WLOG
Aesop.Builder.Apply
Foundation.FirstOrder.Arith.Hierarchy
Batteries.Data.Nat.Basic
Mathlib.Order.Interval.Finset.Defs
Foundation.Meta.Kite.Modal
Mathlib.Tactic.Linter.DocPrime
Foundation.FirstOrder.Hauptsatz
Plausible.Sampleable
Foundation.FirstOrder.Arith.Representation
Mathlib.Algebra.Order.Ring.Basic
Mathlib.Tactic.Observe
Mathlib.Data.Rat.Cast.Lemmas
Mathlib.Algebra.Group.Embedding
Mathlib.Logic.Function.Defs
Mathlib.Lean.Expr.ExtraRecognizers
Foundation.Modal.Kripke.Hilbert.KDB
Foundation.Propositional.ConsistentTableau
Foundation.FirstOrder.Basic.Syntax.Rew
Aesop.RuleTac
Mathlib.Order.Iterate
Batteries.Util.Cache
Batteries.Logic
Mathlib.Data.Set.Finite.Basic
Aesop.RuleTac.Forward.Basic
Mathlib.Tactic.Linter.GlobalAttributeIn
Mathlib.Util.TransImports
Mathlib.Tactic.ClearExclamation
Foundation.Propositional.Logic.Letterless_Int_Cl
Mathlib.Algebra.GCDMonoid.Basic
Mathlib.Tactic.ExtractLets
Foundation.Modal.Kripke.Hilbert.KTB
Aesop.Search.Expansion.Basic
Mathlib.Data.SProd
Aesop.Frontend.Extension.Init
Mathlib.Data.Subtype
Foundation.Arithmetization.ISigmaOne.Bit
Mathlib.Tactic.Linter.Multigoal
Aesop.Script.Util
Foundation.Propositional.Kripke.Hilbert.Soundness
Mathlib.Algebra.Order.Field.Rat
Mathlib.Tactic.Widget.Calc
Mathlib.Algebra.Group.Invertible.Defs
Lean
Aesop.Util.Tactic.Unfold
Aesop.Tree.ExtractScript
Mathlib.Data.Set.CoeSort
Mathlib.Logic.Function.Basic
Mathlib.Logic.Equiv.List
Aesop.BaseM
Plausible.Tactic
Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Qq
ProofWidgets.Data.Html
Mathlib.Computability.Primrec
ImportGraph.Imports
Mathlib.Algebra.Group.Commute.Defs
Mathlib.Order.WithBot
Mathlib.Data.Finset.Union
Foundation.FirstOrder.Arith.Nonstandard
Mathlib.Data.Multiset.OrderedMonoid
Mathlib.Data.List.Perm.Subperm
Mathlib.Algebra.GroupWithZero.Semiconj
Mathlib.Tactic.ApplyFun
Mathlib.Algebra.Group.InjSurj
Foundation.Arithmetization.Definability.Init
Mathlib.Data.Nat.Basic
Foundation.Propositional.Kripke.Completeness
Mathlib.Data.Set.Basic
Qq.Simp
Mathlib.Tactic.Ring
Mathlib.Data.Nat.ModEq
Foundation.Logic.Semantics
Foundation.Arithmetization.ISigmaZero.Exponential.Pow2
Mathlib.Tactic.Linter.Style
Mathlib.Algebra.Group.Nat.Units
Foundation.Modal.Kripke.Hilbert.Triv
Mathlib.Order.Filter.AtTopBot.Tendsto
Aesop.Stats.Report
Mathlib.Tactic.Ring.Basic
Batteries.Classes.RatCast
Mathlib.Data.Finset.Range
Mathlib.Algebra.Order.Ring.InjSurj
Mathlib.Data.Multiset.Replicate
Mathlib.Util.Qq
Foundation.Arithmetization.Vorspiel.ExistsUnique
Mathlib.Data.Set.Notation
Aesop.RuleTac.RuleTerm
Mathlib.Data.Fintype.Pigeonhole
Aesop.Rule.Name
Aesop.Frontend.RuleExpr
Mathlib.Algebra.Order.AbsoluteValue.Basic
Aesop.Builder.Constructors
Mathlib.Algebra.Order.Ring.Rat
Mathlib.Order.WellFounded
Mathlib.Algebra.BigOperators.Ring.Multiset
Mathlib.Data.Multiset.Dedup
Mathlib.Tactic.GuardGoalNums
Mathlib.Data.Finset.Preimage
Aesop.Script.CtorNames
Foundation.Arithmetization.Definability.BoundedBoldface
Batteries.Lean.Meta.InstantiateMVars
Aesop.BuiltinRules.Subst
Mathlib.Algebra.Order.AddGroupWithTop
Mathlib.Algebra.Order.Group.Lattice
Mathlib.Tactic.PPWithUniv
Mathlib.Data.Nat.Pairing
Qq.Typ
Mathlib.Logic.Godel.GodelBetaFunction
Mathlib.Logic.Relation
Aesop.Search.Expansion
Mathlib.Lean.EnvExtension
Mathlib.Algebra.Group.Pi.Basic
Mathlib.Order.Filter.Pi
Mathlib.Data.Multiset.Basic
Foundation.Propositional.Kripke.Hilbert.KC
Foundation.FirstOrder.Completeness.SubLanguage
Aesop.Script.ScriptM
Mathlib.Data.PNat.Defs
Foundation.Modal.Kripke.Hilbert.GL.Completeness
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Foundation.Propositional.Heyting.Semantics
Mathlib.Algebra.Order.Invertible
Aesop.Tree.Data
Mathlib.Data.Multiset.Filter
Batteries.Data.Array.Basic
Mathlib.Algebra.GroupWithZero.Opposite
Mathlib.Lean.Elab.Term
Mathlib.Order.Antichain
Mathlib.Tactic.Spread
Foundation.Modal.ComplementClosedConsistentFinset
Mathlib.Data.Multiset.Range
Foundation.Incompleteness.Arith.FormalizedArithmetic
Foundation.Arithmetization.ISigmaOne.Metamath.Proof.Typed
Batteries.Lean.Meta.SavedState
Aesop.Options
ProofWidgets.Cancellable
Mathlib.Data.Finset.Lattice.Basic
Mathlib.Algebra.Group.Action.Prod
Mathlib.Algebra.Group.Pi.Lemmas
Mathlib.Data.ENat.Defs
Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Mathlib.Data.List.Forall2
Foundation.Modal.Kripke.Filteration
Mathlib.Algebra.Ring.Int.Parity
Mathlib.Data.NNRat.Defs
Mathlib.Tactic.UnsetOption
Aesop.Script.Check
Mathlib.Algebra.Order.Monoid.WithTop
Mathlib.Tactic.CC.Datatypes
Foundation.Logic.LindenbaumAlgebra
Foundation.FirstOrder.Basic.Coding
Mathlib.Data.Multiset.Defs
Mathlib.Tactic.Widget.Conv
Mathlib.Data.Set.SymmDiff
Mathlib.Algebra.Group.Nat.Defs
Foundation.Arithmetization.ISigmaOne.Metamath.Formula.Basic
Mathlib.Data.Fintype.Defs
Foundation.ProvabilityLogic.Soundness
Aesop.Script.SScript
Mathlib.Logic.Function.ULift
Mathlib.Algebra.Order.Group.Nat
Foundation.Modal.Kripke.AxiomPoint3
Mathlib.Algebra.Ring.Basic
Foundation.Arithmetization.ISigmaOne.Metamath.Language
Foundation.Arithmetization.ISigmaOne.HFS.Fixpoint
Aesop.Frontend.Attribute
Mathlib.Tactic.CC
Mathlib.Util.Notation3
Mathlib.Tactic.Push
Mathlib.Logic.Equiv.Set
Batteries.Data.RBMap.Basic
Foundation.Vorspiel.Arith
Qq.ForLean.ReduceEval
Foundation.Modal.Logic.Sublogic.KTc
Aesop.Script.GoalWithMVars
Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Mathlib.Algebra.Group.NatPowAssoc
Mathlib.Tactic.Linter.RefineLinter
Aesop.Index.Basic
Mathlib.Tactic.CC.MkProof
Mathlib.Algebra.Field.Defs
Batteries.Data.Array.Merge
Mathlib.Algebra.Order.BigOperators.Group.Multiset
Mathlib.Lean.Meta.Simp
Mathlib.Control.Combinators
Mathlib.Order.MinMax
Mathlib.Algebra.Order.Hom.Basic
Mathlib.Data.Set.Inclusion
Mathlib.Algebra.GroupWithZero.InjSurj
Foundation.FirstOrder.Arith.Basic
Batteries.Data.List.Count
Batteries.Lean.TagAttribute
Mathlib.Tactic.Common
Foundation.FirstOrder.Basic.Syntax.Formula
Foundation.Modal.Tableau
Foundation.FirstOrder.Completeness.Corollaries
Aesop.Rule.Basic
Mathlib.Order.Interval.Multiset
Mathlib.Order.ZornAtoms
Batteries.Lean.Expr
Mathlib.Tactic.MkIffOfInductiveProp
Batteries.Lean.Meta.UnusedNames
Aesop.Forward.State.Initial
Foundation.Modal.Kripke.Hilbert.Soundness
Batteries.Tactic.Lint.Simp
Mathlib.Data.Multiset.Pi
Plausible.Functions
Mathlib.Data.Sum.Basic
Mathlib.Order.BoundedOrder.Monotone
Mathlib.Tactic.TFAE
Batteries.Data.BinomialHeap.Basic
Mathlib.Order.GaloisConnection.Defs
Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Mathlib.Data.ULift
Foundation.Modal.Maximal.Makinson
Mathlib.Algebra.Group.WithOne.Defs
Foundation.Modal.Hilbert.K
Mathlib.Algebra.BigOperators.Ring.List
Foundation.Modal.Logic.Sublogic.S5Grz
Foundation.ProvabilityLogic.Basic
Aesop.RuleTac.Forward
Mathlib.Order.Hom.Basic
Mathlib.Order.Interval.Set.OrdConnected
Foundation.Logic.HilbertStyle.Cl
Mathlib.Tactic.GCongr.CoreAttrs
Mathlib.Tactic.Linarith
Mathlib.Order.Filter.AtTopBot.Defs
Foundation.Modal.Logic.Sublogic.K4
Mathlib.Data.Multiset.Sections
Mathlib.Order.Defs.LinearOrder
Aesop.Tree.RunMetaM
Mathlib.Data.Part
Mathlib.Tactic.FailIfNoProgress
Mathlib.Logic.Nontrivial.Defs
Mathlib.Tactic.Eqns
Mathlib.Order.UpperLower.Basic
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Algebra.Order.Nonneg.Ring
Foundation.FirstOrder.Basic.Model
Mathlib.Data.Nat.Order.Lemmas
Mathlib.Tactic.Nontriviality.Core
Mathlib.Algebra.Order.Interval.Set.Monoid
Mathlib.Tactic.TypeCheck
Mathlib.Order.Interval.Set.Basic
Aesop.Frontend.Tactic
Mathlib.Algebra.Order.Group.Unbundled.Abs
Mathlib.Logic.Encodable.Pi
Batteries.Tactic.Unreachable
Aesop.Script.SpecificTactics
Foundation.Modal.Kripke.AxiomGeach
Mathlib.Tactic.Widget.CongrM
Mathlib.Tactic.Bound.Attribute
Mathlib.Data.Ineq
Mathlib.Algebra.BigOperators.Group.Finset.Pi
Batteries.Lean.PersistentHashSet
Plausible.Testable
Foundation.Modal.Logic.Extension
Mathlib.Data.Rat.Lemmas
Foundation.Propositional.Logic.Disjunctive
Mathlib.Tactic.Linarith.Frontend
Mathlib.Lean.Meta.Basic
Mathlib.Data.Option.Basic
Aesop.Forward.SlotIndex
Mathlib.Tactic.NormNum.OfScientific
Mathlib.Data.Nat.Cast.Commute
Aesop.Script.OptimizeSyntax
Mathlib.Data.Finite.Defs
Mathlib.Tactic.SimpRw
Mathlib.Order.LatticeIntervals
Mathlib.Data.Nat.PSub
Mathlib.Algebra.Group.Int.Defs
Mathlib.Algebra.Order.Monoid.OrderDual
Aesop.RuleTac.GoalDiff
Mathlib.Algebra.Ring.Associated
Mathlib.Order.Interval.Finset.Nat
Mathlib.Algebra.Prime.Defs
Mathlib.Algebra.Group.Action.TypeTags
Mathlib.Data.Rat.Init
Batteries.Control.ForInStep.Basic
Mathlib.Tactic.Linter.PPRoundtrip
Mathlib.Tactic.Inhabit
Mathlib.Data.List.Lattice
Foundation.Modal.PLoN.Basic
Mathlib.Algebra.Order.Field.Canonical
Mathlib.Data.Set.Subsingleton
Mathlib.Tactic.Simps.Basic
Mathlib.Data.Set.Lattice
Mathlib.Algebra.Ring.Opposite
Mathlib.Logic.Embedding.Basic
Batteries.Lean.Meta.Inaccessible
Foundation.Modal.Kripke.Preservation
Batteries.Lean.Syntax
Foundation.Propositional.ClassicalSemantics.NNFormula
Mathlib.Data.Fintype.Basic
Batteries.Data.List.Lemmas
Batteries.Control.Nondet.Basic
Foundation.Modal.Entailment.K
Mathlib.Algebra.Group.Opposite
Foundation.Propositional.Logic.WellKnown
Mathlib.Algebra.Order.Monoid.Canonical.Defs
Mathlib.Order.RelIso.Set
Batteries.CodeAction.Attr
Mathlib.Data.Finite.Sigma
Mathlib.Order.Interval.Set.Defs
Foundation.Logic.HilbertStyle.Context
Foundation.Modal.Kripke.Hilbert.GL.Tree
Foundation.Modal.Kripke.Hilbert.GrzPoint3
Foundation.Modal.Kripke.Hilbert.KB
Mathlib.Data.List.TakeWhile
Mathlib.Data.Set.Finite.Lemmas
Mathlib.Data.FunLike.Basic
Aesop.Tree
Mathlib.Order.Filter.Bases.Finite
Mathlib.Data.Nat.Cast.Order.Ring
Mathlib.Util.CountHeartbeats
Mathlib.Control.Traversable.Basic
Mathlib.Tactic.Relation.Symm
Aesop.RuleTac.Descr
Foundation.Incompleteness.Arith.WitnessComparizon
Mathlib.Algebra.Notation.Defs
Mathlib.Tactic.Rename
Mathlib.Data.Fintype.Prod
Foundation.Vorspiel.Vorspiel
Mathlib.Algebra.Order.Group.InjSurj
Mathlib.Algebra.Group.Units.Basic
Mathlib.Data.Finset.Dedup
Mathlib.Algebra.Order.Ring.Cast
Aesop.Util.UnionFind
Aesop.Builder.Basic
Foundation.FirstOrder.Basic.BinderNotation
Mathlib.Data.Multiset.AddSub
Aesop.Search.Main
Mathlib.Tactic.ToExpr
Foundation.Arithmetization.ISigmaOne.Metamath.Formula.Typed
Mathlib.Algebra.Ring.Hom.Defs
Foundation.Arithmetization.ISigmaOne.HFS
Mathlib.Order.BoundedOrder.Lattice
Aesop.Tree.AddRapp
Mathlib.Tactic.RSuffices
Aesop.Util.Tactic.Ext
Foundation.Modal.Entailment.S5
Mathlib.Data.Finset.Basic
Foundation.Modal.PLoN.Completeness
LeanSearchClient.Syntax
Mathlib.Data.Finset.Defs
Foundation.Modal.Entailment.Basic
Mathlib.Lean.Name
Mathlib.Algebra.BigOperators.Group.List.Basic
Mathlib.Data.List.GetD
Mathlib.Tactic.Convert
Mathlib.Order.GaloisConnection.Basic
Foundation.Modal.Kripke.Completeness
Mathlib.Order.Lattice
Mathlib.Order.CompleteLattice.Finset
Mathlib.Tactic.GCongr.Core
Aesop.RuleTac.Cases
Mathlib.Data.Nat.BinaryRec
Mathlib.Logic.Equiv.Option
Foundation.Propositional.ClassicalSemantics.Hilbert
Mathlib.Tactic.SuccessIfFailWithMsg
Mathlib.Data.Fin.Basic
Mathlib.Order.Monotone.Basic
Aesop.Script.StructureStatic
Mathlib.Data.List.Perm.Lattice
Mathlib.Tactic.DeclarationNames
ImportGraph.RequiredModules
Mathlib.Tactic.NormNum.Ineq
Mathlib.Data.Multiset.Antidiagonal
Aesop.Builder.Tactic
Foundation.Arithmetization.ISigmaOne.Metamath.Proof.Derivation
Foundation.Incompleteness.Arith.FixedPoint
Aesop.BuiltinRules.DestructProducts
Foundation.Modal.Entailment.Grz
Aesop.Forward.Match
Foundation.IntFO.Basic.Formula
Qq.ForLean.ToExpr
Mathlib.Data.Finset.Card
Aesop.RPINF.Basic
Foundation.Modal.Entailment.KT
Foundation.FirstOrder.Completeness.Coding
Mathlib.Order.Max
Mathlib.Data.List.Induction
Mathlib.Order.Filter.Cofinite
Foundation.Arithmetization.ISigmaZero.Exponential.PPow2
Mathlib.Tactic.Linarith.Datatypes
Aesop.Forward.Match.Types
Mathlib.Algebra.Order.Group.Abs
Mathlib.Logic.Embedding.Set
Foundation.Propositional.Kripke.AxiomWeakLEM
Mathlib.Algebra.Order.Group.Multiset
Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Mathlib.Tactic.CasesM
Mathlib.Data.Nat.Bitwise
Mathlib.Data.Fintype.Pi
Mathlib.Data.List.NodupEquivFin
Mathlib.Order.SetNotation
Foundation.Arithmetization.ISigmaOne.HFS.PRF
Foundation.Logic.Predicate.Language
Mathlib.Lean.Expr.ReplaceRec
Aesop.Rule.Forward
Mathlib.Order.Interval.Finset.Basic
Mathlib.Control.Functor
Foundation.Propositional.Logic.Basic
Mathlib.Data.Finset.Image
Aesop.Forward.Substitution
Foundation.Modal.Kripke.Hilbert.GL.Unnecessitation
Foundation.Modal.Kripke.Hilbert.KD4
Mathlib.Data.List.FinRange
Foundation.Arithmetization.Basic.IOpen
Mathlib.Algebra.Order.Group.Unbundled.Basic
Mathlib.Algebra.Group.Hom.Instances
Aesop.Search.Expansion.Norm
Mathlib.Tactic.SimpIntro
Mathlib.Order.Filter.AtTopBot.Disjoint
Foundation.Modal.Geachean
Aesop.Forward.PremiseIndex
Mathlib.Algebra.Field.Rat
Mathlib.Algebra.GroupWithZero.Invertible
Mathlib.Algebra.Group.Action.Pretransitive
Mathlib.Data.List.Range
Mathlib.Order.ConditionallyCompleteLattice.Basic
Batteries.Data.MLList.Basic
Mathlib.Data.Int.CharZero
Mathlib.Tactic.SplitIfs
Mathlib.Algebra.Group.Semiconj.Basic
Mathlib.Logic.Basic
Mathlib.Data.List.Flatten
Mathlib.Order.Interval.Set.Image
Mathlib.Algebra.Order.Monoid.Defs
Foundation.Arithmetization.Basic.PeanoMinus
Aesop.BuiltinRules.Split
Aesop.RuleTac.Apply
Mathlib.Order.Filter.AtTopBot.Basic
Foundation.Modal.Kripke.Hilbert.Grz.Completeness
Mathlib.Algebra.Ring.Semiconj
Mathlib.Tactic.Conv
Foundation.Modal.Kripke.Hilbert.GL.Soundness
Mathlib.Data.Fin.Tuple.Basic
LeanSearchClient
Foundation.FirstOrder.Basic.Eq
Mathlib.Logic.Nonempty
Aesop.BuiltinRules.Rfl
Mathlib.Order.Bounds.Image
Foundation.Modal.Boxdot.Basic
Mathlib.Tactic.Widget.SelectPanelUtils
Mathlib.Data.Finset.Slice
Mathlib.Tactic.CC.Lemmas
Batteries.Data.List.Basic
Foundation.Modal.Kripke.AxiomL
Mathlib.Data.Set.Monotone
Foundation.IntFO.Basic.Deduction
Mathlib.Tactic.SwapVar
Foundation.Modal.Kripke.Hilbert.S4
Batteries.Classes.Order
Mathlib.Tactic.NormNum.Core
Foundation.Modal.Logic.Sublogic.KH
Foundation.Modal.ModalCompanion.LC
Foundation.Vorspiel.Relation.Iterate
Mathlib.Data.Fintype.Sets
Mathlib.Util.WhatsNew
Mathlib.Algebra.BigOperators.Group.List.Defs
Mathlib.Data.Countable.Basic
Foundation.IntFO.Basic.Rew
Mathlib.Algebra.Group.TypeTags.Hom
Mathlib.Data.String.Defs
Batteries.Data.Nat.Gcd
Foundation.Arithmetization.ISigmaOne.Metamath.Proof.Thy
Foundation.Modal.Kripke.Hilbert.KD45
Mathlib.Order.ConditionallyCompleteLattice.Defs
Foundation.Arithmetization.Definability.Boldface
Foundation.Modal.Entailment.KTc
Aesop.ElabM
Mathlib.Tactic.Tauto
Mathlib.Data.Set.Pairwise.Lattice
Batteries.Control.ForInStep.Lemmas
Foundation.Arithmetization.ISigmaOne.HFS.Basic
Mathlib.Data.Nat.Choose.Basic
Foundation.Arithmetization.Vorspiel.Graph
Mathlib.Algebra.Order.Ring.Nat
Mathlib.Tactic.Linarith.Lemmas
Aesop.RuleTac.Preprocess
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Tactic.ClearExcept
Mathlib.Algebra.Group.Support
Batteries.Tactic.Alias
Mathlib.Data.Int.Init
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
Mathlib.Order.RelIso.Basic
Mathlib.Data.Setoid.Basic
Mathlib.Algebra.Ring.Defs
Mathlib.Data.Multiset.Bind
Mathlib.Algebra.BigOperators.Intervals
Mathlib.Data.Multiset.ZeroCons
Qq.Macro
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
Mathlib.Data.Int.DivMod
Mathlib.Util.AssertExists
Mathlib.Data.Int.Cast.Basic
Mathlib.Tactic.TermCongr
Foundation.Propositional.ClassicalSemantics.ZeroSubst
Mathlib.Tactic.Linarith.Parsing
Mathlib.Tactic.SetLike
Mathlib.Order.PropInstances
Foundation.Arithmetization.ISigmaZero.Exponential.Log
Foundation.FirstOrder.Basic.Semantics.Semantics
Mathlib.Data.Set.Finite.Range
Mathlib.Algebra.Ring.Hom.Basic
Qq.MetaM
Mathlib.Tactic.ToLevel
Mathlib.Data.Multiset.Sum
Mathlib.Algebra.Order.GroupWithZero.Canonical
Foundation.FirstOrder.Interpretation
Mathlib.Tactic.Subsingleton
Mathlib.Data.Set.Pairwise.Basic
Foundation.Modal.Kripke.Hilbert.KTc
Aesop.Tree.Check
LeanSearchClient.Basic
Mathlib.Tactic.HigherOrder
Mathlib.Data.List.Rotate
Mathlib.Data.Set.List
Mathlib.Init
Mathlib.Algebra.Notation.Pi
Batteries.Lean.PersistentHashMap
Foundation.Modal.Logic.Sublogic.Grz
Mathlib.Algebra.Order.Sub.Basic
Mathlib.Data.Fintype.EquivFin
Foundation.Modal.Hilbert.GL.Alternatives
Qq.Match
Mathlib.Tactic.Choose
Aesop.Tree.ExtractProof
Mathlib.Order.Filter.CountablyGenerated
Mathlib.Order.Filter.Ultrafilter.Basic
Foundation.Propositional.Hilbert.Basic
Qq.AssertInstancesCommute
Mathlib.Lean.PrettyPrinter.Delaborator
Mathlib.Lean.Expr.Basic
Foundation.Arithmetization.ISigmaOne.Metamath.Formula.Iteration
Foundation.Logic.Calculus
Mathlib.Data.Set.Order
Mathlib.Algebra.GroupWithZero.Nat
Mathlib.Tactic.Linter.UnusedTactic
Mathlib.Algebra.Ring.Invertible
Batteries.Tactic.Lint.Misc
Foundation.Arithmetization.OmegaOne.Basic
Mathlib.Algebra.GroupWithZero.Units.Equiv
Foundation.Modal.Kripke.Hilbert.K4Point2
Mathlib.Data.Multiset.Powerset
Foundation.Arithmetization.Vorspiel.Lemmata
Mathlib.Order.Hom.Lattice
Mathlib.Data.Set.Function
Foundation.Propositional.Kripke.AxiomLEM
Mathlib.Algebra.Notation.Prod
Foundation.Modal.Kripke.Hilbert.GrzPoint2
Mathlib.Data.Nat.Cast.Defs
Foundation.Logic.HilbertStyle.Supplemental
Mathlib.Data.Fintype.List
Foundation.Meta.Kite.Arith
Mathlib.Order.CompleteLatticeIntervals
Foundation.Arithmetization.ISigmaOne.Metamath
Mathlib.Util.Delaborators
Mathlib.Algebra.Group.Units.Equiv
Mathlib.Order.CompleteLattice
Mathlib.Tactic.GuardHypNums
Foundation.Logic.Axioms
Mathlib.Order.Filter.Finite
Batteries.Data.RBMap.Alter
Mathlib.Algebra.Group.Commute.Units
Mathlib.Tactic.CancelDenoms.Core
Mathlib.Data.List.Monad
Mathlib.Util.WithWeakNamespace
Aesop.Nanos
Aesop.RuleSet.Name
Foundation.Arithmetization.ISigmaOne.Metamath.Term.Typed
Batteries.Data.List.Perm
Mathlib.Data.Ordering.Basic
Aesop.RulePattern.Cache
Aesop.RuleTac.Tactic
Mathlib.Data.Prod.PProd
Mathlib.Data.Nat.Find
Mathlib.Order.Defs.PartialOrder
Foundation.Vorspiel.Chain
Mathlib.Data.List.Duplicate
Foundation.Logic.Predicate.Term
Mathlib.Control.Applicative
Aesop.Options.Public
Mathlib.Computability.Partrec
Mathlib.Algebra.Order.Monoid.TypeTags
Mathlib.Tactic.Positivity.Core
Foundation.Modal.Kripke.Hilbert.K5
Mathlib.Tactic.ExtendDoc
Mathlib.Data.PNat.Basic
Mathlib.Tactic.Linter
Mathlib.Algebra.Order.Monoid.NatCast
Mathlib.Lean.Elab.Tactic.Basic
Mathlib.Algebra.Divisibility.Hom
Mathlib.Tactic.HaveI
Mathlib.Data.Set.Countable
Mathlib.Tactic.ByContra
Aesop.Saturate
Mathlib.Data.Finset.Lattice.Lemmas
Mathlib.Data.Multiset.Lattice
Foundation.Modal.Kripke.Hilbert.K45
Mathlib.Data.SetLike.Basic
Mathlib.Order.Interval.Set.UnorderedInterval
Aesop.BuiltinRules.Ext
Foundation.Modal.Kripke.Hilbert.Ver
Mathlib.Data.Set.Insert
Foundation.Modal.Kripke.Hilbert.KD
Foundation.Propositional.Formula
Foundation.Modal.ModalCompanion.Basic
Mathlib.Data.Option.NAry
Foundation.Modal.Formula
Mathlib.Algebra.Regular.Basic
Mathlib.Data.List.Basic
Foundation.Logic.Predicate.Quantifier
Foundation.IntFO.Basic
Mathlib.Algebra.GroupWithZero.WithZero
Mathlib.Tactic.Linter.MinImports
Mathlib.Data.Finset.SymmDiff
Aesop.Index.DiscrTreeConfig
Mathlib.Algebra.Notation
Mathlib.Order.Defs.Unbundled
Mathlib.Data.Set.Defs
Mathlib.Algebra.Divisibility.Basic
Foundation.Subformula
Mathlib.Lean.Meta
Mathlib.Tactic.NormNum
Aesop.Tree.Tracing
Qq.Delab
Mathlib.Order.BoundedOrder.Basic
Mathlib.Algebra.GroupWithZero.Commute
Mathlib.Algebra.Group.Equiv.Opposite
Foundation.Arithmetization.ISigmaOne.Metamath.Coding
Mathlib.Data.Finset.Erase
Mathlib.Data.Array.Defs
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Mathlib.Algebra.Ring.Divisibility.Basic
Mathlib.Algebra.GroupWithZero.Divisibility
Mathlib.Data.Rat.Defs
Foundation.Modal.Entailment.K5
Aesop.Script.UScript
Mathlib.Data.List.Sort
Batteries.Lean.NameMapAttribute
Mathlib.Data.Finite.Prod
Foundation.Modal.Hilbert.S5Grz
Foundation.Modal.Kripke.ComplexityLimited
Mathlib.Data.Set.Finite.Powerset
Mathlib.Algebra.Ring.Rat
Mathlib.Algebra.Order.ZeroLEOne
Aesop
Aesop.Util.UnorderedArraySet
Foundation.ProvabilityLogic.GL.Unprovability
Mathlib.Order.Disjoint
Foundation.Arithmetization.ISigmaZero.Exponential.Exp
Mathlib.Order.Minimal
Mathlib.Order.Filter.Map
Aesop.Builder.Forward
Mathlib.Data.Int.Order.Basic
Batteries.Tactic.Lint
Mathlib.Tactic.Core
Mathlib.Logic.Equiv.Defs
Mathlib.Util.PPOptions
Foundation.Propositional.Hilbert.Int
Mathlib.Order.Bounds.Basic
Mathlib.Data.Rat.Cast.Order
Mathlib.Data.Rel
Mathlib.Data.Fintype.Card
Aesop.Exception
Mathlib.Data.List.Chain
Foundation.Modal.Axioms
Mathlib.Data.Quot
Foundation.Incompleteness.Arith.Second
Aesop.Util.Basic
Mathlib.Tactic.Propose
Mathlib.Data.List.Zip
Foundation.FirstOrder.Arith.Model
Mathlib.Algebra.Group.Units.Hom
Aesop.Builder.Default
Mathlib.Data.Int.Notation
Mathlib.Tactic.FastInstance
Mathlib.Algebra.Ring.Nat
Mathlib.Order.Interval.Set.OrderIso
Mathlib.Tactic.Linarith.Verification
Mathlib.Algebra.Order.Nonneg.Lattice
Foundation.Vorspiel.ExistsUnique
Mathlib.Data.FunLike.Embedding
Mathlib.Tactic.Linter.Header
Batteries.Data.Array.Init.Lemmas
Mathlib.Algebra.Prime.Lemmas
Mathlib.Tactic.NormNum.DivMod
Mathlib.Algebra.Ring.Commute
Foundation.Arithmetization.Vorspiel.Vorspiel
ProofWidgets.Compat
Mathlib.Algebra.Order.Field.InjSurj
Aesop.Index
Foundation.Modal.Entailment.K4
Mathlib.Tactic.ToAdditive.Frontend
Mathlib.Tactic.Contrapose
Foundation.Modal.Kripke.AxiomWeakPoint2
Mathlib.Tactic.AdaptationNote
Foundation.Modal.Kripke.AxiomWeakPoint3
Mathlib.Data.Set.NAry
Mathlib.Tactic.Ring.PNat
Mathlib.Order.Chain
Mathlib.Tactic.Clear_
Mathlib.Algebra.Ring.Int.Defs
Mathlib.Order.Hom.Set
Aesop.Search.SearchM
Mathlib.Tactic.Linter.OldObtain
Batteries.Tactic.PermuteGoals
Foundation.FirstOrder.Basic.Calculus
Foundation.Propositional.NNFormula
Mathlib.Data.Nat.Init
Mathlib.Algebra.GroupWithZero.Hom
Foundation.Propositional.Kripke.Hilbert.Int
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
Mathlib.Tactic.Monotonicity.Attr
Mathlib.Data.Int.GCD
Batteries.Lean.Position
Foundation.Modal.Kripke.Hilbert.GLPoint3
Mathlib.Data.Finset.Pi
Mathlib.Tactic.Linter.Lint
Foundation.Modal.Boxdot.Ver_Triv
Foundation.Modal.Logic.WellKnown
Mathlib.Tactic.Linter.HaveLetLinter
Mathlib.Data.Set.Image
Mathlib.Algebra.Group.Equiv.Defs
Aesop.Search.Queue
Mathlib.Logic.Function.Iterate
Mathlib.Data.Vector.Basic
Batteries.Tactic.Lint.TypeClass
Mathlib.Util.CompileInductive
Mathlib.Data.Int.Basic
Plausible
Mathlib.Tactic.MinImports
Mathlib.Algebra.Group.Action.Hom
Foundation.Modal.ModalCompanion.Int
Mathlib.Data.List.Scan
Mathlib.Order.CompleteBooleanAlgebra
Mathlib.Tactic.ProjectionNotation
Foundation.Vorspiel.Order
Mathlib.Order.Zorn
Mathlib.Data.Multiset.UnionInter
Mathlib.Algebra.Order.BigOperators.Ring.List
Mathlib.Data.Finset.Fold
Batteries.CodeAction.Deprecated
Aesop.Check
Mathlib.Data.FunLike.Equiv
Mathlib.Tactic.ApplyWith
Foundation.Vorspiel.Relation.Closure
Mathlib.Data.List.Defs
Mathlib.Tactic.ApplyCongr
Aesop.Search.Expansion.Simp
Mathlib.Util.AssertExistsExt
Mathlib.Algebra.Group.TypeTags.Basic
Foundation.Modal.Kripke.Hilbert.GL.MDP
Foundation.Modal.Logic.Sublogic.GL
Mathlib.Algebra.Order.Group.Synonym
Batteries.Lean.MonadBacktrack
Mathlib.Order.Filter.Ker
Mathlib.Algebra.Group.Nat.Even
Mathlib.Order.Atoms
Mathlib.Tactic.RenameBVar
Aesop.Search.Queue.Class
Mathlib.Control.EquivFunctor
Aesop.RulePattern
Aesop.RuleSet
Mathlib.Data.Nat.Bits
Mathlib.Order.ModularLattice
Mathlib.Order.Synonym
Mathlib.Algebra.Group.Defs
Foundation.FirstOrder.Arith.PeanoMinus
Foundation.Vorspiel.Collection
Foundation.Modal.Hilbert.NNFormula
ProofWidgets.Component.Basic
Foundation.FirstOrder.Basic
Mathlib.Algebra.Group.Equiv.Basic
Mathlib.Tactic.Widget.SelectInsertParamsClass
Plausible.Gen
Foundation.Modal.Kripke.ExtendRoot
Mathlib.Algebra.Order.Sub.Unbundled.Basic
Mathlib.Order.SupClosed
Foundation.Modal.ModalCompanion.KC
Mathlib.Order.ConditionallyCompleteLattice.Indexed
Foundation.FirstOrder.Basic.Soundness
Mathlib.Order.Antisymmetrization
Mathlib.Tactic.ErwQuestion
Foundation.Modal.Hilbert.KP
Foundation.IntFO.Translation
ProofWidgets.Component.MakeEditLink
Foundation.Modal.Kripke.Hilbert.KB4
Mathlib.Data.Set.Sigma
Mathlib.Tactic.Hint
Foundation.Modal.Hilbert.Basic
Aesop.Tracing
Foundation.Modal.Hilbert.WellKnown
Foundation.Propositional.Kripke.Filteration
Foundation.Propositional.Tait.Calculus
Foundation.Incompleteness.Arith.DC
Aesop.Search.ExpandSafePrefix
Mathlib.Algebra.Group.Prod
Foundation.Arithmetization.Definability.Hierarchy
Mathlib.Order.Interval.Set.OrderEmbedding
Foundation.Modal.Kripke.Hilbert.KD5
Foundation.Modal.Kripke.Tree
Foundation.Modal.Entailment.KD
Foundation.FirstOrder.Basic.Calculus2
Mathlib.Data.List.Sublists
Mathlib.Tactic.CongrExclamation
Mathlib.Algebra.Group.Commute.Basic
Mathlib.Data.Set.Finite.Lattice
Mathlib.Data.Bracket
Mathlib.Data.Finset.Piecewise
Foundation.Propositional.Kripke.Rooted
Foundation.Modal.Kripke.Hilbert.K4Point3
Mathlib.Logic.Equiv.Nat
Aesop.Tree.UnsafeQueue
Mathlib.Util.SynthesizeUsing
Foundation.Modal.Kripke.Hilbert.S5
Aesop.Main
Mathlib.Data.Vector.Defs
Batteries.CodeAction.Basic
Mathlib.Data.List.Lex
Mathlib.Tactic.NormNum.Inv
Mathlib.Tactic.IrreducibleDef
Mathlib.Data.Rat.Cast.Defs
Mathlib.Data.Nat.BitIndices
Batteries.Util.LibraryNote
Batteries.Linter
Foundation.Modal.NNFormula
Foundation.Logic.HilbertStyle.Lukasiewicz
Mathlib.Order.Filter.Tendsto
Mathlib.Algebra.Order.Group.OrderIso
LeanSearchClient.LoogleSyntax
Mathlib.Order.Filter.Bases.Basic
Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas
Foundation.ProvabilityLogic.GL.Completeness
Batteries.Lean.Meta.Expr
Mathlib.Algebra.GroupWithZero.Units.Lemmas
Mathlib.Data.Nat.Prime.Defs
Mathlib.Tactic.Linter.UnusedTacticExtension
Mathlib.Algebra.Group.Action.Faithful
Foundation.Propositional.Hilbert.Glivenko
Mathlib.Data.Finset.Disjoint
Foundation.Modal.Entailment.Triv
Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Foundation.Modal.Kripke.Hilbert.K
Mathlib.Data.Rat.Cast.CharZero
Foundation.FirstOrder.Arith.StrictHierarchy
Mathlib.Data.List.Pairwise
Mathlib.Data.Set.Operations
Mathlib.Tactic.Abel
Foundation.Modal.Hilbert.GL.Independency
Mathlib.Data.Nat.Factorial.Basic
Aesop.RuleTac.ElabRuleTerm
Foundation.Modal.Boxdot.GLPoint3_GrzPoint3
Batteries.Data.Rat.Lemmas
Mathlib.Tactic.NormNum.Basic
Mathlib.Tactic.Simps.NotationClass
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Data.Finset.Max
Mathlib.Data.Bool.Set
Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Foundation.Propositional.Entailment.KC
Mathlib.Data.Finset.Lattice.Union
Batteries.Tactic.Congr
Mathlib.Algebra.Ring.InjSurj
Mathlib.Tactic.CC.Addition
Foundation.Arithmetization.ISigmaOne.HFS.Vec
Mathlib.Tactic.NormNum.Eq
Mathlib.Algebra.Order.Ring.Canonical
Foundation.Modal.Hilbert.Maximal.Basic
Mathlib.Order.ULift
Mathlib.Util.Tactic
Mathlib.Logic.IsEmpty
Mathlib.Order.Directed
Mathlib.Data.Sigma.Basic
Foundation.Modal.Logic.Sublogic.ModalCube
Mathlib.Order.ConditionallyCompleteLattice.Finset
Mathlib.Tactic.NthRewrite
Mathlib.Tactic.ExistsI
Mathlib.Tactic.Lemma
Mathlib.Logic.Equiv.Basic
Mathlib.Data.Finset.Powerset
Mathlib.Algebra.Order.BigOperators.Group.Finset
Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Aesop.Util.Tactic
Mathlib.Data.Int.Sqrt
Mathlib.Data.Finset.Sigma
Mathlib.Order.TypeTags
Foundation.Modal.Kripke.Rooted
Batteries.CodeAction
Mathlib.Algebra.Order.Positive.Ring
Mathlib.Order.SymmDiff
Foundation.Modal.Entailment.KP
Batteries.Tactic.Lint.Frontend
Mathlib.Algebra.Order.Group.Defs
Aesop.BuiltinRules.ApplyHyps
Mathlib.Data.Option.Defs
Batteries.Lean.HashSet
Mathlib.Tactic.Attr.Core
Mathlib.Algebra.Order.BigOperators.Ring.Finset
Batteries.Linter.UnreachableTactic
Mathlib.Tactic.Lift
Foundation.ProvabilityLogic.N.Soundness
Batteries.Data.RBMap.WF
Foundation.Incompleteness.ToFoundation.Basic
Mathlib.Tactic.Check
Mathlib.Tactic.Constructor
Aesop.RPINF
Foundation.Modal.Entailment.S4
Mathlib.Algebra.Group.Semiconj.Units
Mathlib.Algebra.Ring.Parity
Mathlib.Tactic.ExtractGoal
Mathlib.Algebra.NeZero
Foundation.Vorspiel.NotationClass
Foundation.Modal.PLoN.Hilbert.Soundness
Foundation.Incompleteness.Arith.D1
Mathlib.Util.MemoFix
Mathlib.Algebra.GroupWithZero.NeZero
Batteries.Tactic.OpenPrivate
Foundation.Propositional.Logic.Sublogic
Foundation.Arithmetization.Definability.Absoluteness
Mathlib.Order.Monotone.Defs
Aesop.Script.TacticState
Batteries.Tactic.Init
Foundation.Arithmetization.ISigmaOne.Metamath.CodedTheory
Foundation.Modal.Hilbert.Maximal.Unprovability
Mathlib.Algebra.Order.Group.Unbundled.Int
Foundation.Init
Mathlib.Algebra.Field.Basic
Foundation.Arithmetization.ISigmaOne.HFS.Seq
Mathlib.Data.Finset.BooleanAlgebra
Aesop.Tree.Data.ForwardRuleMatches
Foundation.FirstOrder.Order.Le
Aesop.Script.UScriptToSScript
Mathlib.Tactic.Linarith.Preprocessing
Mathlib.Control.Basic
Mathlib.Tactic.NormNum.Result
Mathlib.Data.Finite.Sum
Foundation.Incompleteness.Arith.D3
Foundation.Incompleteness.Arith.ConsistencyPredicate
Foundation.Propositional.Entailment.LC
Aesop.Script.Tactic
Mathlib.Data.Fintype.Sum
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Tactic.Attr.Register
Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Mathlib.Combinatorics.Colex
Mathlib.Tactic.CongrM
Foundation.Arithmetization.Basic.Ind
Batteries.Tactic.Exact
Mathlib.Tactic.Finiteness.Attr
Foundation.Modal.Kripke.KH_Incompleteness
Mathlib.Data.Nat.Cast.Basic
Mathlib.Tactic.TryThis
Mathlib.Tactic.Simproc.ExistsAndEq
Foundation.Modal.Logic.Sublogic.S4
Aesop.Percent
Batteries.WF
Mathlib.Data.Finset.Option
Aesop.Forward.State.ApplyGoalDiff
Aesop.Frontend.Command
Foundation.Modal.Kripke.Basic
Aesop.Stats.Extension
Mathlib.Data.Finset.Empty
Mathlib.Algebra.Order.Ring.Int
Mathlib.Logic.OpClass
Mathlib.Order.Compare
Aesop.Search.RuleSelection
Mathlib.Algebra.Divisibility.Units
Foundation.ProvabilityLogic.Grz.Completeness
Aesop.RuleTac.Basic
Foundation.Propositional.ClassicalSemantics.Tait
Mathlib.Tactic.Linter.HashCommandLinter
Foundation.Modal.Boxdot.K4_S4
Foundation
Mathlib.Computability.Halting
ProofWidgets.Component.OfRpcMethod
Mathlib.Control.ULift
Mathlib.Tactic.Basic