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