`/Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.28.0-rc1/bin/lake setup-file /Users/stepannesterov/Lean/mathlib4/Mathlib.lean -` failed:

stderr:
✔ [2/20] Built Batteries.Lean.TagAttribute (818ms)
✔ [3/20] Built Batteries.Classes.RatCast (623ms)
✔ [4/22] Built Batteries.Tactic.Unreachable (936ms)
✔ [5/22] Built Batteries.Util.ProofWanted (894ms)
✔ [6/25] Built Batteries.Tactic.SeqFocus (1.2s)
✔ [7/25] Built Batteries.Lean.EStateM (971ms)
✔ [8/29] Built Batteries.Util.LibraryNote (1.3s)
✔ [9/29] Built Batteries.Lean.Except (592ms)
✔ [10/29] Built Batteries.Lean.AttributeExtra (651ms)
✔ [11/30] Built Batteries.Tactic.Init (1.7s)
✔ [12/30] Built Batteries.Lean.Position (643ms)
✔ [13/30] Built Batteries.Data.List.ArrayMap (526ms)
✔ [14/33] Built Batteries.Classes.Cast (725ms)
✔ [15/36] Built Batteries.Data.List.Count (452ms)
✔ [16/37] Built Batteries.CodeAction.Attr (1.4s)
✔ [17/37] Built Batteries.Data.List.Init.Lemmas (502ms)
✔ [18/43] Built Batteries.Linter.UnreachableTactic (1.5s)
✔ [19/46] Built Batteries.Control.ForInStep.Basic (536ms)
✔ [20/47] Built Batteries.Classes.SatisfiesM (1.5s)
✔ [21/47] Built Batteries.CodeAction.Deprecated (1.7s)
✔ [22/47] Built Batteries.Control.Lemmas (639ms)
✔ [23/48] Built Batteries.Control.ForInStep.Lemmas (609ms)
✔ [24/48] Built Batteries.Data.Array.Match (1.3s)
✔ [25/52] Built Batteries.Control.ForInStep (375ms)
✔ [26/54] Built Batteries.Data.List.Monadic (711ms)
✔ [27/55] Built Batteries.Linter.UnnecessarySeqFocus (2.2s)
✔ [28/57] Built Batteries.CodeAction.Basic (1.8s)
✔ [29/57] Built Batteries.Data.List.Matcher (690ms)
✔ [30/62] Built Batteries.Data.Array.Basic (774ms)
✔ [31/62] Built Batteries.Data.Array.Init.Lemmas (630ms)
✔ [32/65] Built Batteries.Control.LawfulMonadState (1.9s)
✔ [33/65] Built Batteries.Linter (840ms)
✔ [34/66] Built Batteries.Tactic.Lint.Basic (1.5s)
✔ [35/66] Built Batteries.Data.BitVec.Basic (520ms)
✔ [36/66] Built Batteries.Tactic.Basic (771ms)
✔ [37/66] Built Batteries.Control.OptionT (959ms)
✔ [38/69] Built Batteries.CodeAction.Misc (4.1s)
✔ [39/69] Built Batteries.Tactic.Alias (3.2s)
✔ [40/72] Built Batteries.Data.Array.Merge (2.4s)
✔ [41/72] Built Batteries.Classes.Order (1.6s)
✔ [42/74] Built Batteries.Control.AlternativeMonad (1.8s)
✔ [43/74] Built Batteries.Control.Monad (1.4s)
✔ [44/74] Built Batteries.Tactic.Lint.Misc (2.3s)
✔ [45/74] Built Batteries.Data.Array.Monadic (3.3s)
✔ [46/74] Built Batteries.Data.Array.Pairwise (1.6s)
✔ [47/77] Built Batteries.Data.Nat.Basic (1.3s)
✔ [48/77] Built Batteries.Data.Char.AsciiCasing (960ms)
✔ [49/80] Built Batteries.Data.ByteSlice (1.7s)
✔ [50/81] Built Batteries.Data.BinaryHeap.Basic (5.3s)
✔ [51/85] Built Batteries.Classes.Deprecated (2.1s)
✔ [52/88] Built Batteries.Data.ByteArray (2.2s)
✔ [53/89] Built Batteries.Data.MLList.Basic (2.5s)
✔ [54/93] Built Batteries.Data.BinaryHeap (599ms)
✔ [55/93] Built Batteries.Data.DList.Basic (806ms)
✔ [56/93] Built Batteries.Data.FloatArray (599ms)
✔ [57/93] Built Batteries.Lean.HashMap (535ms)
✔ [58/95] Built Batteries.Data.Nat.Lemmas (1.6s)
✔ [59/95] Built Batteries.Data.DList.Lemmas (685ms)
✔ [60/95] Built Batteries.Data.MLList.Heartbeats (910ms)
✔ [61/95] Built Batteries.Lean.System.IO (814ms)
✔ [62/95] Built Batteries.Data.NameSet (704ms)
✔ [63/95] Built Batteries.Control.Nondet.Basic (1.5s)
✔ [64/96] Built Batteries.Data.DList (542ms)
✔ [65/98] Built Batteries.Data.Fin.OfBits (1.3s)
✔ [66/98] Built Batteries.Data.Int (1.4s)
✔ [67/98] Built Batteries.Data.HashMap.Basic (1.9s)
✔ [68/99] Built Batteries.Data.MLList.IO (622ms)
✔ [69/99] Built Batteries.Data.Nat.Bitwise (811ms)
✔ [70/99] Built Batteries.Data.List.Basic (7.4s)
✔ [71/99] Built Batteries.Data.Fin.Basic (3.1s)
✔ [72/99] Built Batteries.Data.Nat.Digits (1.7s)
✔ [73/99] Built Batteries.Data.Nat.Gcd (1.3s)
✔ [74/99] Built Batteries.Data.HashMap (1.4s)
✔ [75/99] Built Batteries.Data.MLList (820ms)
✔ [76/99] Built Batteries.Data.BitVec.Lemmas (2.3s)
✔ [77/103] Built Batteries.Data.Nat.Bisect (4.2s)
✔ [78/103] Built Batteries.Data.List.Pairwise (1.3s)
✔ [79/103] Built Batteries.Data.PairingHeap (2.3s)
✔ [80/107] Built Batteries.Data.BitVec (1.8s)
✔ [81/109] Built Batteries.Data.Fin.Lemmas (3.4s)
✔ [82/109] Built Batteries.Data.Fin.Fold (3.1s)
✔ [83/113] Built Batteries.Data.AssocList (4.4s)
✔ [84/113] Built Batteries.Data.Nat (2.1s)
✔ [85/116] Built Batteries.Data.Fin (861ms)
✔ [86/116] Built Batteries.Data.Range.Lemmas (1.1s)
✔ [87/116] Built Batteries.Data.RunningStats (870ms)
✔ [88/117] Built Batteries.Lean.Float (1.3s)
✔ [89/118] Built Batteries.Data.String.AsciiCasing (870ms)
✔ [90/118] Built Batteries.Data.Stream (1.4s)
✔ [91/121] Built Batteries.Data.Range (1.4s)
✔ [92/123] Built Batteries.Data.String.Basic (1.2s)
✔ [93/125] Built Batteries.Data.Rat.Float (970ms)
✔ [94/125] Built Batteries.Data.BinomialHeap.Basic (14s)
✔ [95/125] Built Batteries.Data.Random.MersenneTwister (4.5s)
✔ [96/126] Built Batteries.Data.String.Matcher (859ms)
✔ [97/127] Built Batteries.Util.Panic (509ms)
✔ [98/129] Built Batteries.Data.Rat (866ms)
✔ [99/129] Built Batteries.Data.UInt (1.8s)
✔ [100/130] Built Batteries.Data.Vector.Basic (725ms)
✔ [101/131] Built Batteries.Data.Random (1.1s)
✔ [102/132] Built Batteries.Data.String.Legacy (2.9s)
✔ [103/133] Built Batteries.Data.BinomialHeap.Lemmas (1.5s)
✔ [104/134] Built Batteries.Data.RBMap.Basic (7.8s)
✔ [105/134] Built Batteries.Lean.HashSet (753ms)
✔ [106/135] Built Batteries.Data.Vector.Monadic (1.3s)
✔ [107/135] Built Batteries.Data.Vector.Lemmas (1.5s)
✔ [108/135] Built Batteries.Lean.IO.Process (965ms)
✔ [109/136] Built Batteries.Lean.Expr (1.7s)
✔ [110/136] Built Batteries.Lean.Json (1.1s)
✔ [111/136] Built Batteries.Data.BinomialHeap (1.4s)
✔ [112/136] Built Batteries.Lean.LawfulMonad (1.3s)
✔ [113/140] Built Batteries.Data.Vector (1.3s)
✔ [114/141] Built Batteries.Lean.LawfulMonadLift (2.1s)
✔ [115/143] Built Batteries.Lean.Meta.Expr (1.5s)
✔ [116/145] Built Batteries.Data.List.Lemmas (12s)
✔ [117/145] Built Batteries.Lean.Meta.Basic (2.5s)
✔ [118/145] Built Batteries.Lean.PersistentHashMap (1.9s)
✔ [119/145] Built Batteries.Lean.MonadBacktrack (1.4s)
✔ [120/146] Built Batteries.Lean.Meta.Inaccessible (1.9s)
✔ [121/147] Built Batteries.Data.List.Perm (1.7s)
✔ [122/147] Built Batteries.Data.Char.Basic (2.5s)
✔ [123/147] Built Batteries.Lean.Meta.InstantiateMVars (1.2s)
✔ [124/147] Built Batteries.Tactic.OpenPrivate (2.8s)
✔ [125/148] Built Batteries.Lean.Meta.DiscrTree (982ms)
✔ [126/149] Built Batteries.Lean.Meta.SavedState (874ms)
✔ [127/149] Built Batteries.Data.UnionFind.Basic (9.2s)
✔ [128/149] Built Batteries.Lean.Meta.UnusedNames (785ms)
✔ [129/150] Built Batteries.Lean.NameMapAttribute (826ms)
✔ [130/150] Built Batteries.Data.Char (823ms)
✔ [131/151] Built Batteries.Data.Array.Lemmas (4.3s)
✔ [132/152] Built Batteries.Lean.PersistentHashSet (716ms)
✔ [133/152] Built Batteries.Lean.SatisfiesM (961ms)
✔ [134/153] Built Batteries.Lean.Syntax (713ms)
✔ [135/154] Built Batteries.Lean.Util.EnvSearch (998ms)
✔ [136/155] Built Batteries.Lean.Meta.Simp (2.2s)
✔ [137/157] Built Batteries.Data.Array (1.0s)
✔ [138/157] Built Batteries.Data.RBMap.WF (9.7s)
✔ [139/157] Built Batteries.Logic (1.2s)
✔ [140/158] Built Batteries.Data.UnionFind.Lemmas (2.1s)
✔ [141/159] Built Batteries.Data.String.Lemmas (11s)
✔ [142/159] Built Batteries.Tactic.Exact (1.0s)
✔ [143/159] Built Batteries.Data.RBMap.Depth (1.0s)
✔ [144/159] Built Batteries.Tactic.Congr (1.0s)
✔ [145/159] Built Batteries.Data.UnionFind (1.0s)
✔ [146/159] Built Batteries.Data.RBMap.Alter (2.1s)
✔ [147/161] Built Batteries.Data.String (950ms)
✔ [148/161] Built Batteries.Tactic.Case (3.2s)
✔ [149/164] Built Batteries.Tactic.Instances (1.6s)
✔ [150/165] Built Batteries.Tactic.Lemma (1.2s)
✔ [151/166] Built Batteries.Tactic.Lint.TypeClass (997ms)
✔ [152/167] Built Batteries.Tactic.NoMatch (1.3s)
✔ [153/168] Built Batteries.Tactic.PermuteGoals (1.0s)
✔ [154/169] Built Batteries.Tactic.Lint.Simp (2.4s)
✔ [155/169] Built Batteries.Data.List.Scan (12s)
✔ [156/170] Built Batteries.Tactic.Lint.Frontend (3.2s)
✔ [157/171] Built Batteries.Tactic.GeneralizeProofs (6.7s)
✔ [158/171] Built Batteries.Tactic.PrintDependents (2.2s)
✔ [159/172] Built Batteries.Tactic.PrintOpaques (2.0s)
✔ [160/173] Built Batteries.Tactic.PrintPrefix (2.3s)
✔ [161/175] Built Batteries.Data.List (1.2s)
✔ [162/175] Built Batteries.Tactic.Lint (1.0s)
✔ [163/175] Built Batteries.Tactic.ShowUnused (1.9s)
✔ [164/194] Built Batteries.Util.Cache (1.1s)
✔ [165/194] Built Batteries.Util.Pickle (457ms)
✔ [167/220] Built Batteries.Util.ExtendedBinder (1.3s)
✔ [169/220] Built Batteries.Tactic.SqueezeScope (2.4s)
✔ [170/223] Built Batteries.Tactic.HelpCmd (8.5s)
✔ [171/225] Built Batteries.CodeAction.Match (2.1s)
✔ [172/226] Built ImportGraph.RequiredModules (1.5s)
✔ [173/229] Built Batteries.CodeAction (795ms)
✔ [174/229] Built Mathlib.Tactic.Linter.DirectoryDependency (2.3s)
✔ [175/229] Built Batteries.Tactic.Trans (4.1s)
✔ [176/245] Built ImportGraph.Imports (1.1s)
✔ [177/292] Built Batteries.Data.RBMap.Lemmas (8.5s)
✔ [179/295] Built Qq.SortLocalDecls (797ms)
✔ [180/297] Built Qq.ForLean.ToExpr (2.5s)
✔ [181/297] Built Qq.Typ (2.2s)
✔ [182/298] Built Qq.ForLean.ReduceEval (3.1s)
✔ [183/299] Built Batteries.Data.RBMap (939ms)
✔ [184/299] Built Aesop.Check (977ms)
✔ [185/300] Built Qq.ForLean.Do (1.6s)
✔ [186/303] Built Aesop.Forward.PremiseIndex (732ms)
✔ [187/306] Built Aesop.Forward.SlotIndex (775ms)
✔ [188/306] Built Aesop.Forward.LevelIndex (691ms)
✔ [189/311] Built Aesop.Nanos (639ms)
✔ [190/315] Built Aesop.Util.UnorderedArraySet (707ms)
✔ [191/319] Built Batteries (1.1s)
✔ [192/319] Built Mathlib.Tactic.Linter.Header (2.5s)
✔ [193/319] Built Aesop.Options.Public (2.1s)
✔ [194/319] Built Aesop.Rule.Name (1.1s)
✔ [195/319] Built Aesop.Index.DiscrTreeConfig (1.6s)
✔ [196/319] Built Aesop.Percent (701ms)
✔ [197/319] Built Aesop.Util.UnionFind (985ms)
✔ [198/319] Built Mathlib.Util.ParseCommand (1.0s)
✔ [199/319] Built Mathlib.Lean.Elab.Tactic.Meta (938ms)
✔ [200/319] Built Mathlib.Lean.Environment (997ms)
✔ [201/319] Built Aesop.RuleTac.FVarIdSubst (1.8s)
✔ [202/319] Built Mathlib.Tactic.MinImports (2.2s)
✔ [203/319] Built Mathlib.Tactic.Linter.TacticDocumentation (1.3s)
✔ [204/319] Built Mathlib.Tactic.Linter.UnusedTacticExtension (1.4s)
✔ [205/319] Built Mathlib.Tactic.Linter.OldObtain (1.1s)
✔ [206/319] Built Mathlib.Tactic.Linter.PrivateModule (1.3s)
✔ [207/319] Built Mathlib.Lean.Expr.Basic (2.2s)
✔ [208/319] Built Mathlib.Tactic.Linter.Whitespace (2.9s)
✔ [209/319] Built Mathlib.Tactic.Linter.Multigoal (1.4s)
✔ [210/319] Built Mathlib.Tactic.DeclarationNames (1.3s)
✔ [211/320] Built Mathlib.Tactic.Linter.GlobalAttributeIn (1.2s)
✔ [212/321] Built Mathlib.Tactic.Linter.HashCommandLinter (1.7s)
✔ [213/321] Built Mathlib.Tactic.Linter.EmptyLine (1.8s)
✔ [214/321] Built Mathlib.Lean.Linter (1.1s)
✔ [215/321] Built Mathlib.Tactic.Linter.DocString (2.1s)
✔ [216/321] Built Aesop.RuleTac.RuleTerm (1.0s)
✔ [217/321] Built Mathlib.Tactic.Linter.DeprecatedSyntaxLinter (2.3s)
✔ [218/321] Built Aesop.Options.Internal (1.8s)
✔ [219/321] Built Mathlib.Tactic.Linter.DocPrime (2.7s)
✔ [220/321] Built Mathlib.Tactic.Linter.FlexibleLinter (4.2s)
✔ [221/321] Built Mathlib.Lean.ContextInfo (1.6s)
✔ [222/321] Built Mathlib.Lean.Elab.InfoTree (1.7s)
✔ [223/321] Built Mathlib.Tactic.Linter.Lint (2.6s)
✔ [224/323] Built Mathlib.Tactic.Linter.UnusedTactic (3.5s)
✔ [225/326] Built Mathlib.Tactic.ExtractGoal (4.0s)
✔ [226/326] Built Aesop.Script.Tactic (2.8s)
✔ [227/332] Built Aesop.Options (1.2s)
✔ [228/334] Built Mathlib.Tactic.Linter.UnusedInstancesInType (2.0s)
✔ [229/339] Built Mathlib.Tactic.TacticAnalysis (2.4s)
✔ [230/342] Built Mathlib.Tactic.Linter.Style (5.0s)
✔ [231/342] Built Aesop.Util.EqualUpToIds (5.3s)
✔ [232/344] Built Qq.Macro (13s)
✔ [233/344] Built Aesop.Script.GoalWithMVars (2.3s)
✔ [234/345] Built Aesop.Util.Basic (7.6s)
✔ [235/346] Built Aesop.ElabM (2.3s)
✔ [236/346] Built Aesop.Util.OrderedHashSet (1.2s)
✔ [237/346] Built Aesop.Util.Tactic (2.0s)
✔ [238/346] Built Aesop.RuleSet.Name (1.7s)
✔ [239/346] Built Aesop.Script.TacticState (2.4s)
✔ [240/346] Built Aesop.Util.Unfold (2.7s)
✔ [241/348] Built Aesop.RuleTac.Forward.Basic (2.1s)
✔ [242/348] Built Aesop.Script.Util (2.0s)
✔ [243/356] Built Aesop.Script.CtorNames (2.7s)
✔ [244/367] Built Aesop.RuleSet.Filter (2.1s)
✔ [245/367] Built Mathlib.Tactic.TacticAnalysis.Declarations (4.0s)
✔ [246/368] Built Aesop.Tracing (2.0s)
✔ [247/368] Built Aesop.RuleTac.ElabRuleTerm (2.9s)
✔ [248/368] Built Qq.Delab (5.4s)
✔ [249/368] Built Aesop.Search.Expansion.Simp (1.2s)
✔ [250/371] Built Aesop.Util.Tactic.Unfold (2.9s)
✔ [251/371] Built Aesop.Forward.Substitution (3.8s)
✔ [252/372] Built Mathlib.Init (1.8s)
✔ [253/376] Built Aesop.Script.OptimizeSyntax (2.4s)
✔ [254/376] Built Aesop.Constants (721ms)
✔ [255/376] Built Aesop.EMap (2.6s)
✔ [256/376] Built Mathlib.Tactic.Substs (1.4s)
✔ [257/376] Built Aesop.Util.Tactic.Ext (2.7s)
✔ [258/376] Built Mathlib.Util.WithWeakNamespace (1.7s)
✔ [259/376] Built Aesop.RulePattern.Cache (1.0s)
✔ [260/376] Built Aesop.Script.Step (3.7s)
✔ [261/376] Built Qq.MetaM (3.2s)
✔ [262/376] Built Mathlib.Lean.PrettyPrinter.Delaborator (2.4s)
✔ [263/376] Built Aesop.Stats.Basic (4.2s)
✔ [264/376] Built Mathlib.Tactic.SimpRw (3.1s)
✔ [265/376] Built Mathlib.Tactic.Core (3.9s)
✔ [266/376] Built Mathlib.Tactic.Use (4.3s)
✔ [267/376] Built Mathlib.Tactic.AdaptationNote (3.3s)
✔ [268/376] Built Mathlib.Tactic.Push.Attr (3.7s)
✔ [269/376] Built Mathlib.Tactic.Attr.Register (3.2s)
✔ [270/376] Built Mathlib.Data.Nat.Notation (2.0s)
✔ [271/376] Built Mathlib.Util.CompileInductive (4.7s)
✔ [272/376] Built Mathlib.Tactic.OfNat (1.3s)
✔ [273/376] Built Mathlib.Lean.Name (1.3s)
✔ [274/376] Built Mathlib.Data.Nat.BinaryRec (1.4s)
✔ [275/376] Built Mathlib.Data.Int.Notation (1.3s)
✔ [276/376] Built Mathlib.Lean.Meta (1.6s)
✔ [277/376] Built Mathlib.Util.MemoFix (1.5s)
✔ [278/376] Built Mathlib.Data.Set.Defs (4.7s)
✔ [279/376] Built Mathlib.Data.String.Defs (1.6s)
✔ [280/376] Built Mathlib.Tactic.Eqns (1.6s)
✔ [281/376] Built Mathlib.Tactic.Simps.NotationClass (2.1s)
✔ [282/379] Built Mathlib.Tactic.ExtendDoc (1.7s)
✔ [283/379] Built Mathlib.Data.Array.Defs (1.4s)
✔ [284/379] Built Mathlib.Tactic.PPWithUniv (1.8s)
✔ [285/379] Built Mathlib.Lean.Elab.Term (1.7s)
✔ [286/379] Built Mathlib.Lean.Meta.Simp (1.0s)
✔ [287/379] Built Mathlib.Util.AddRelatedDecl (2.5s)
✔ [288/379] Built Mathlib.Tactic.Lemma (1.7s)
✔ [289/379] Built Aesop.Script.SScript (1.7s)
✔ [290/380] Built Aesop.Script.UScript (1.8s)
✔ [291/380] Built Qq.MatchImpl (2.0s)
✔ [292/380] Built Aesop.BaseM (1.8s)
✔ [293/382] Built Qq.Simp (2.0s)
✔ [294/382] Built Mathlib.Tactic.SplitIfs (1.0s)
✔ [295/382] Built Mathlib.Tactic.TypeStar (1.3s)
✔ [296/382] Built Qq.AssertInstancesCommute (3.3s)
✔ [297/382] Built Mathlib.Tactic.ScopedNS (3.9s)
✔ [298/382] Built Mathlib.Tactic.Translate.GuessName (2.0s)
✔ [299/382] Built Aesop.Script.Check (2.5s)
✔ [300/382] Built Aesop.Script.ScriptM (2.8s)
✔ [301/382] Built Aesop.Script.UScriptToSScript (3.0s)
✔ [302/382] Built Mathlib.Logic.Function.Defs (2.7s)
✔ [303/382] Built Mathlib.Tactic.Inhabit (2.0s)
✔ [304/382] Built Aesop.RulePattern (4.4s)
✔ [305/384] Built Mathlib.Logic.Nontrivial.Defs (2.0s)
✔ [306/384] Built Mathlib.Logic.Nonempty (2.0s)
✔ [307/384] Built Mathlib.Logic.ExistsUnique (3.0s)
✔ [308/384] Built Mathlib.Tactic.MkIffOfInductiveProp (5.3s)
✔ [309/384] Built Aesop.RuleTac.GoalDiff (6.3s)
✔ [310/384] Built Qq.Commands (4.8s)
✔ [311/409] Built Mathlib.Logic.Relator (2.7s)
✔ [312/409] Built Aesop.Script.StructureStatic (4.7s)
✔ [313/410] Built Aesop.Script.StructureDynamic (6.9s)
✔ [314/413] Built Aesop.Exception (3.3s)
✔ [315/416] Built Aesop.Stats.Extension (2.6s)
✔ [316/416] Built Aesop.Forward.RuleInfo (5.5s)
✔ [317/428] Built Aesop.Script.SpecificTactics (7.0s)
✔ [318/439] Built Aesop.Stats.File (1.9s)
✔ [319/440] Built Aesop.Frontend.Basic (1.6s)
✔ [320/441] Built Aesop.Script.Main (2.1s)
✔ [321/452] Built Mathlib.Control.Combinators (1.3s)
✔ [322/454] Built Aesop.Rule.Forward (1.9s)
✔ [323/454] Built Aesop.Stats.Report (2.5s)
✔ [324/458] Built Mathlib.Data.Option.Defs (1.4s)
✔ [325/463] Built Mathlib.Tactic.Spread (2.5s)
✔ [326/463] Built Mathlib.Data.Ordering.Basic (1.2s)
✔ [327/469] Built Qq.Match (16s)
✔ [328/472] Built Mathlib.Logic.Function.ULift (1.3s)
✔ [329/472] Built Mathlib.Tactic.GCongr.ForwardAttr (1.6s)
✔ [330/490] Built Mathlib.Data.Set.CoeSort (1.2s)
✔ [331/494] Built Aesop.Forward.Match.Types (2.1s)
✔ [332/497] Built Mathlib.Util.AtLocation (1.7s)
✔ [333/497] Built Mathlib.Tactic.ToExpr (1.5s)
✔ [334/499] Built Qq (2.4s)
✔ [335/517] Built Mathlib.Tactic.Coe (2.2s)
✔ [336/522] Built Mathlib.Tactic.Monotonicity.Attr (1.6s)
✔ [337/533] Built Mathlib.Tactic.Conv (3.2s)
✔ [338/533] Built Aesop.Index.Basic (3.0s)
✔ [339/536] Built Mathlib.Tactic.CasesM (3.5s)
✔ [340/536] Built Mathlib.Tactic.Attr.Core (2.3s)
✔ [341/538] Built Mathlib.Tactic.Set (3.5s)
✔ [343/544] Built Mathlib.Data.Int.Init (3.9s)
✔ [344/548] Built Mathlib.Tactic.FBinop (5.1s)
✔ [345/550] Built Plausible.Attr (754ms)
✔ [347/552] Built Aesop.RuleTac.Basic (2.0s)
✔ [348/553] Built Plausible.Random (1.4s)
✔ [349/553] Built Aesop.Index.Forward (2.7s)
✔ [350/553] Built Mathlib.Util.Notation3 (19s)
✔ [351/553] Built LeanSearchClient.Basic (788ms)
✔ [352/553] Built Aesop.Index.RulePattern (3.2s)
✔ [353/553] Built Mathlib.Data.SProd (1.7s)
✔ [354/553] Built Mathlib.Tactic.Simproc.ExistsAndEq (6.9s)
✔ [355/553] Built Aesop.Search.Expansion.Basic (2.2s)
✔ [356/555] Built Aesop.RuleTac.Preprocess (2.2s)
✔ [357/556] Built Plausible.Gen (1.6s)
✔ [358/556] Built Aesop.RuleTac.Tactic (2.7s)
✔ [359/557] Built Aesop.RuleTac.Descr (1.0s)
✔ [360/558] Built Aesop.RuleTac.Cases (2.8s)
✔ [361/558] Built Aesop.RuleTac.Apply (2.6s)
✔ [362/559] Built Mathlib.Tactic.ApplyCongr (1.8s)
✔ [363/560] Built Plausible.Arbitrary (1.2s)
✔ [364/561] Built Mathlib.Tactic.ApplyWith (1.4s)
✔ [365/561] Built Mathlib.Lean.Meta.Basic (1.9s)
✔ [366/561] Built Mathlib.Tactic.Check (1.9s)
✔ [367/562] Built Mathlib.Tactic.ClearExclamation (1.4s)
✔ [368/563] Built Plausible.ArbitraryFueled (799ms)
✔ [369/565] Built Aesop.Rule.Basic (2.1s)
✔ [370/565] Built Mathlib.Tactic.ClearExcept (1.4s)
✔ [371/565] Built LeanSearchClient.Syntax (3.8s)
✔ [372/566] Built Plausible.Sampleable (1.9s)
✔ [373/566] Built Mathlib.Tactic.Basic (3.9s)
✔ [374/567] Built Mathlib.Tactic.Clear_ (1.5s)
✔ [375/567] Built Mathlib.Tactic.Constructor (1.2s)
✔ [376/568] Built Mathlib.Tactic.ApplyAt (1.6s)
✔ [377/568] Built Aesop.Rule (1.9s)
✔ [378/568] Built Mathlib.Tactic.DeprecateTo (2.6s)
✔ [379/568] Built Mathlib.Tactic.ExistsI (1.6s)
✔ [380/568] Built Mathlib.Tactic.ErwQuestion (2.1s)
✔ [381/568] Built Plausible.DeriveArbitrary (3.5s)
✔ [382/568] Built LeanSearchClient.LoogleSyntax (3.0s)
✔ [383/568] Built Plausible.Testable (3.6s)
✔ [384/568] Built Mathlib.Tactic.DefEqTransformations (3.9s)
✔ [385/568] Built Mathlib.Tactic.Find (3.0s)
✔ [386/569] Built Mathlib.Tactic.FailIfNoProgress (4.3s)
✔ [387/569] Built Mathlib.Logic.Basic (5.3s)
✔ [388/569] Built Mathlib.Tactic.Lift (5.7s)
✔ [389/569] Built Aesop.Tree.UnsafeQueue (3.3s)
✔ [390/570] Built LeanSearchClient (904ms)
✔ [391/570] Built Mathlib.Data.Nat.Init (6.1s)
✔ [392/570] Built Aesop.RuleSet.Member (2.3s)
✔ [393/572] Built Plausible.Functions (1.7s)
✔ [394/572] Built Plausible.Tactic (2.1s)
✔ [395/572] Built Aesop.Forward.Match (5.8s)
✔ [396/572] Built Mathlib.Tactic.FunProp.Decl (2.8s)
✔ [397/574] Built Mathlib.Tactic.FunProp.Mor (1.8s)
✔ [398/574] Built Aesop.Builder.Basic (1.9s)
✔ [399/574] Built Plausible (882ms)
✔ [400/574] Built Mathlib.Tactic.Subsingleton (3.0s)
✔ [401/575] Built Mathlib.Tactic.FunProp.ToBatteries (3.1s)
✔ [402/575] Built Aesop.Tree.Data.ForwardRuleMatches (2.1s)
✔ [403/575] Built Mathlib.Tactic.Tauto (5.6s)
✔ [404/575] Built Mathlib.Tactic.Simps.Basic (11s)
✔ [405/575] Built Mathlib.Tactic.Push (6.2s)
✔ [406/575] Built Mathlib.Lean.Meta.RefinedDiscrTree.Basic (2.1s)
✔ [407/575] Built Aesop.RuleTac.Forward (4.4s)
✔ [408/575] Built Aesop.Index (3.4s)
✔ [409/578] Built Aesop.Builder.Apply (1.8s)
✔ [410/578] Built Aesop.Builder.Unfold (2.1s)
✔ [411/578] Built Aesop.Builder.NormSimp (1.7s)
✔ [412/578] Built Aesop.Builder.Tactic (1.9s)
✔ [413/578] Built Aesop.Builder.Forward (2.9s)
✔ [414/578] Built Aesop.Builder.Constructors (2.1s)
✔ [415/578] Built Aesop.Builder.Cases (2.3s)
✔ [416/578] Built Mathlib.Tactic.FunProp.FunctionData (2.3s)
✔ [417/579] Built Mathlib.Tactic.ByCases (2.3s)
✔ [418/579] Built Mathlib.Tactic.ByContra (2.5s)
✔ [419/580] Built Mathlib.Tactic.Contrapose (2.0s)
✔ [420/586] Built Aesop.RuleTac (2.3s)
✔ [421/587] Built Mathlib.Lean.Meta.RefinedDiscrTree.Initialize (2.0s)
✔ [422/588] Built Aesop.Builder.Default (2.4s)
✔ [423/589] Built Mathlib.Tactic.GuardGoalNums (1.5s)
✔ [424/589] Built Aesop.Forward.State (10s)
✔ [425/589] Built Mathlib.Lean.Meta.RefinedDiscrTree.Encode (3.1s)
✔ [426/589] Built Mathlib.Tactic.FunProp.Types (2.9s)
✔ [427/591] Built Mathlib.Tactic.GuardHypNums (1.3s)
✔ [428/591] Built Mathlib.Tactic.Hint (3.4s)
✔ [429/592] Built Aesop.RuleSet (5.5s)
✔ [430/593] Built Mathlib.Tactic.HigherOrder (1.9s)
✔ [431/593] Built Mathlib.Tactic.InferParam (1.5s)
✔ [432/593] Built Mathlib.Lean.Meta.RefinedDiscrTree.Lookup (1.9s)
✔ [433/594] Built Mathlib.Util.TermReduce (1.7s)
✔ [434/595] Built Aesop.Tree.Data (3.1s)
✔ [435/595] Built Aesop.Frontend.Extension.Init (1.9s)
✔ [436/595] Built Aesop.Forward.State.ApplyGoalDiff (2.3s)
✔ [437/595] Built Aesop.Forward.State.Initial (2.1s)
✔ [438/595] Built Mathlib.Tactic.Linter.DeprecatedModule (1.7s)
✔ [439/595] Built Mathlib.Tactic.Linter.HaveLetLinter (1.1s)
✔ [440/595] Built Aesop.Frontend.RuleExpr (4.5s)
✔ [441/595] Built Mathlib.Tactic.Linter.MinImports (1.0s)
✔ [442/598] Built Aesop.Search.Queue.Class (1.5s)
✔ [443/599] Built Aesop.Tree.Traversal (1.7s)
✔ [444/599] Built Aesop.Frontend.Extension (2.3s)
✔ [445/599] Built Mathlib.Tactic.Translate.Core (12s)
✔ [446/599] Built Aesop.Tree.RunMetaM (1.9s)
✔ [447/599] Built Mathlib.Tactic.IrreducibleDef (3.2s)
✔ [448/600] Built Mathlib.Tactic.FunProp.Theorems (3.4s)
✔ [449/600] Built Mathlib.Tactic.Linter.PPRoundtrip (1.5s)
✔ [450/600] Built ImportGraph.Meta (2.1s)
✔ [451/601] Built Aesop.Tree.TreeM (2.4s)
✔ [452/601] Built Aesop.Tree.State (2.4s)
✔ [453/601] Built Mathlib.Tactic.NthRewrite (1.3s)
✔ [454/601] Built Aesop.Frontend.Tactic (2.0s)
✔ [455/601] Built Aesop.Frontend.Attribute (2.5s)
✔ [456/602] Built Aesop.Frontend.Command (3.6s)
✔ [457/602] Built Mathlib.Tactic.Translate.ToDual (2.4s)
✔ [458/602] Built Mathlib.Tactic.Translate.ToAdditive (2.4s)
✔ [459/602] Built Aesop.Tree.Tracing (2.9s)
✔ [460/602] Built Mathlib.Tactic.Observe (2.2s)
✔ [461/602] Built Mathlib.Tactic.FunProp.Attr (2.5s)
✔ [462/602] Built Aesop.Saturate (6.3s)
✔ [463/602] Built Mathlib.Tactic.Linter.UpstreamableDecl (2.1s)
✔ [464/602] Built Mathlib.Tactic.RSuffices (2.4s)
✔ [465/602] Built Aesop.Tree.Stats (2.5s)
✔ [466/603] Built Aesop.Tree.Free (1.9s)
✔ [467/603] Built Aesop.Search.SearchM (2.5s)
✔ [468/603] Built Aesop.Forward.State.UpdateGoal (2.0s)
✔ [469/603] Built Aesop.Tree.ExtractProof (2.6s)
✔ [470/603] Built Aesop.Tree.ExtractScript (3.2s)
✔ [471/603] Built Mathlib.Tactic.FunProp.Core (6.9s)
✔ [472/603] Built Aesop.BuiltinRules.Split (1.6s)
✔ [473/603] Built Aesop.BuiltinRules.Subst (2.0s)
✔ [474/603] Built Aesop.Tree.Check (2.8s)
✔ [475/603] Built Aesop.Tree.AddRapp (4.7s)
✔ [476/604] Built Aesop.BuiltinRules.Rfl (1.8s)
✔ [477/604] Built Aesop.BuiltinRules.Intros (1.9s)
✔ [478/604] Built Aesop.BuiltinRules.Ext (1.8s)
✔ [479/604] Built Aesop.BuiltinRules.DestructProducts (2.1s)
✔ [480/604] Built Mathlib.Tactic.Recover (1.7s)
✔ [481/604] Built Aesop.BuiltinRules.ApplyHyps (2.0s)
✔ [482/604] Built Aesop.BuiltinRules.Assumption (2.1s)
✔ [483/604] Built Mathlib.Tactic.ToDual (2.3s)
✔ [484/606] Built Mathlib.Tactic.Linter (1.6s)
✔ [485/606] Built Mathlib.Tactic.Relation.Rfl (1.3s)
✔ [486/606] Built Mathlib.Tactic.ToAdditive (2.2s)
✔ [487/607] Built Aesop.Tree (1.8s)
✔ [488/608] Built Aesop.Search.RuleSelection (2.2s)
✔ [489/608] Built Aesop.Frontend.Saturate (3.1s)
✔ [490/608] Built Mathlib.Tactic.Rename (1.7s)
✔ [491/608] Built Aesop.BuiltinRules (1.7s)
✔ [492/609] Built Mathlib.Tactic.FunProp.Elab (3.3s)
✔ [493/609] Built Mathlib.Util.Tactic (1.7s)
✔ [494/609] Built Mathlib.Order.Notation (2.9s)
✔ [495/610] Built Mathlib.Order.Defs.PartialOrder (3.0s)
✔ [496/610] Built Aesop.Search.Queue (2.4s)
✔ [497/611] Built Mathlib.Algebra.Notation.Defs (3.4s)
✔ [498/611] Built Mathlib.Order.Defs.Unbundled (3.4s)
✔ [499/611] Built Aesop.Frontend (1.9s)
✔ [500/612] Built Mathlib.Tactic.Says (3.1s)
✔ [501/612] Built Mathlib.Tactic.SimpIntro (1.0s)
✔ [502/612] Built Mathlib.Tactic.FunProp (1.9s)
✔ [503/612] Built Mathlib.Tactic.SuccessIfFailWithMsg (1.5s)
✔ [504/613] Built Mathlib.Tactic.RenameBVar (1.3s)
✔ [505/613] Built Mathlib.Tactic.SudoSetOption (1.6s)
✔ [506/613] Built Mathlib.Tactic.SwapVar (1.3s)
✔ [507/614] Built Mathlib.Order.Defs.LinearOrder (3.4s)
✔ [508/614] Built Aesop.Search.Expansion.Norm (6.3s)
✔ [509/615] Built Mathlib.Algebra.Regular.Defs (2.9s)
✔ [510/615] Built Mathlib.Logic.Relation (4.4s)
✔ [511/616] Built Mathlib.Algebra.Notation.Pi.Defs (3.9s)
✔ [512/616] Built Mathlib.Tactic.ToLevel (1.9s)
✔ [513/616] Built Mathlib.Logic.Function.Basic (5.2s)
✔ [514/617] Built Mathlib.Tactic.ToFun (3.5s)
✔ [515/617] Built Mathlib.Tactic.Trace (1.6s)
✔ [516/617] Built Mathlib.Tactic.TypeCheck (1.5s)
✔ [517/617] Built Mathlib.Tactic.UnsetOption (1.6s)
✔ [518/617] Built Mathlib.Data.Bool.Basic (3.2s)
✔ [519/617] Built Mathlib.Data.Int.Order.Basic (2.7s)
✔ [520/617] Built Mathlib.Tactic.GCongr.Core (6.0s)
✔ [521/617] Built Aesop.Search.Expansion (3.5s)
✔ [522/617] Built Mathlib.Algebra.Notation.Pi.Basic (2.2s)
✔ [523/617] Built Mathlib.Data.Sigma.Basic (1.9s)
✔ [524/619] Built Mathlib.Logic.Function.Conjugate (2.6s)
✔ [525/625] Built Mathlib.Data.Subtype (2.9s)
✔ [526/625] Built Mathlib.Data.Sum.Basic (3.1s)
✔ [527/625] Built Mathlib.Tactic.Choose (3.5s)
✔ [531/625] Built Mathlib.Logic.IsEmpty (3.0s)
✔ [532/625] Built Mathlib.Data.Nat.Basic (3.3s)
✔ [535/628] Built Mathlib.Tactic.GCongr.CoreAttrs (2.5s)
✔ [536/628] Built Mathlib.Tactic.GRewrite.Core (2.8s)
✔ [538/628] Built Mathlib.Tactic.Widget.SelectInsertParamsClass (1.5s)
✔ [539/637] Built Mathlib.Tactic.Variable (4.6s)
✖ [540/637] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.
✔ [552/640] Built Mathlib.Logic.Function.Iterate (2.9s)
✔ [553/640] Built Aesop.Search.ExpandSafePrefix (3.2s)
✔ [554/642] Built Mathlib.Lean.GoalsLocation (1.1s)
✔ [555/642] Built Mathlib.Lean.Meta.RefinedDiscrTree (1.4s)
✔ [557/644] Built Mathlib.Logic.Unique (2.4s)
✔ [558/644] Built Mathlib.Algebra.Group.Defs (9.7s)
✔ [559/644] Built Mathlib.Tactic.GCongr (2.4s)
✔ [560/645] Built Mathlib.Lean.Meta.KAbstractPositions (1.6s)
✔ [562/645] Built Mathlib.Lean.Meta.CongrTheorems (4.5s)
✔ [563/646] Built Mathlib.Data.Prod.Basic (3.0s)
✔ [564/646] Built Mathlib.Tactic.GRewrite.Elab (3.6s)
✔ [565/646] Built Mathlib.Data.FunLike.Basic (2.3s)
✔ [567/649] Built Mathlib.Tactic.WLOG (2.8s)
✔ [568/649] Built Mathlib.Util.CountHeartbeats (1.9s)
✔ [569/649] Built Aesop.Search.Main (3.8s)
✔ [570/649] Built Mathlib.Util.PrintSorries (1.5s)
✔ [571/649] Built Mathlib.Data.Quot (3.6s)
✔ [572/649] Built Mathlib.Algebra.Group.Semiconj.Defs (2.9s)
✔ [573/649] Built Mathlib.Util.TransImports (1.5s)
✔ [574/649] Built Mathlib.Algebra.Group.Pi.Basic (4.6s)
✔ [575/649] Built Mathlib.Logic.Nontrivial.Basic (2.8s)
✔ [576/649] Built Mathlib.Tactic.GRewrite (2.4s)
✔ [577/649] Built Mathlib.Algebra.Notation.Prod (3.4s)
✔ [578/655] Built Mathlib.Algebra.Group.InjSurj (5.7s)
✔ [579/658] Built Mathlib.Data.FunLike.Embedding (2.2s)
✔ [580/658] Built Mathlib.Util.WhatsNew (1.7s)
✔ [581/658] Built Mathlib.Tactic.CongrExclamation (5.5s)
✔ [582/658] Built Mathlib.Tactic.TermCongr (6.8s)
✔ [583/663] Built Mathlib.Algebra.Group.Commute.Defs (2.0s)
✔ [584/663] Built Aesop.Main (3.2s)
✔ [585/663] Built Mathlib.Algebra.GroupWithZero.Defs (3.2s)
✔ [586/663] Built Mathlib.Algebra.NeZero (2.5s)
✔ [587/663] Built Mathlib.Data.FunLike.Equiv (2.7s)
✔ [588/664] Built Mathlib.Tactic.CongrM (2.4s)
✔ [589/666] Built Mathlib.Tactic.Convert (3.3s)
✔ [590/666] Built Mathlib.Tactic.StacksAttribute (1.9s)
✔ [591/668] Built Aesop (1.9s)
✔ [593/668] Built Mathlib.Data.Nat.Cast.Defs (3.1s)
✔ [594/668] Built Mathlib.Algebra.GroupWithZero.NeZero (2.3s)
✔ [595/668] Built Mathlib.Algebra.Group.Hom.Defs (9.1s)
✔ [596/668] Built Mathlib.Algebra.Group.Int.Defs (1.0s)
✔ [597/668] Built Mathlib.Data.Int.Basic (2.0s)
✔ [598/668] Built Mathlib.Data.Option.Basic (3.4s)
✔ [599/673] Built Mathlib.Algebra.Group.Units.Defs (6.7s)
✔ [600/675] Built Mathlib.Tactic.Finiteness.Attr (2.9s)
✔ [601/678] Built Mathlib.Logic.Equiv.Defs (6.9s)
✔ [602/678] Built Mathlib.Data.Set.Operations (4.6s)
✔ [603/678] Built Mathlib.Data.Int.Cast.Defs (2.8s)
✔ [604/678] Built Mathlib.Algebra.Group.Nat.Defs (2.3s)
✔ [605/678] Built Mathlib.Order.Basic (7.8s)
✔ [606/678] Built Mathlib.Algebra.GroupWithZero.InjSurj (3.4s)
✔ [607/678] Built Mathlib.Data.Nat.Sqrt (4.2s)
✔ [608/678] Built Mathlib.Control.EquivFunctor (3.4s)
✔ [609/678] Built Mathlib.Algebra.CharZero.Defs (3.2s)
✔ [610/678] Built Mathlib.Algebra.Opposites (5.1s)
✔ [611/680] Built Mathlib.Order.Synonym (3.4s)
✔ [612/680] Built Mathlib.Algebra.Ring.Defs (4.7s)
✔ [614/680] Built Mathlib.Algebra.Group.Basic (11s)
✔ [615/680] Built Mathlib.Order.Monotone.Defs (3.6s)
✔ [617/680] Built Mathlib.Algebra.Group.Equiv.Defs (7.6s)
✔ [618/681] Built Mathlib.Order.ULift (2.8s)
✔ [619/681] Built Mathlib.Order.RelClasses (3.9s)
✔ [621/681] Built Mathlib.Tactic.FastInstance (2.1s)
✔ [622/681] Built Mathlib.Logic.Equiv.Option (3.8s)
✔ [623/681] Built Mathlib.Order.Compare (4.2s)
✔ [624/685] Built Mathlib.Data.Int.Cast.Basic (4.8s)
✔ [625/685] Built Mathlib.Order.Max (5.4s)
✔ [626/685] Built Mathlib.Algebra.GroupWithZero.Basic (5.6s)
✔ [627/685] Built Mathlib.Algebra.Group.Action.Defs (7.0s)
✔ [628/688] Built Mathlib.Algebra.Group.Torsion (4.7s)
✔ [629/688] Built Mathlib.Data.List.TFAE (1.7s)
✔ [630/688] Built Mathlib.Util.AtomM (2.9s)
✔ [631/688] Built Mathlib.Algebra.Ring.Int.Defs (2.8s)
✔ [632/688] Built Mathlib.Algebra.Group.Units.Basic (7.7s)
✔ [633/688] Built Mathlib.Algebra.Group.Hom.Basic (5.0s)
✔ [634/688] Built Mathlib.Algebra.GroupWithZero.Nat (2.7s)
✔ [635/688] Built Mathlib.Algebra.Group.Action.Faithful (3.3s)
✔ [636/688] Built Mathlib.Order.Monotone.Basic (5.3s)
✔ [637/688] Built Mathlib.Order.BoundedOrder.Basic (5.4s)
✔ [638/688] Built Mathlib.Algebra.Group.Opposite (5.5s)
✔ [639/691] Built Mathlib.Algebra.Group.TypeTags.Basic (6.1s)
✔ [640/693] Built Mathlib.Algebra.Group.Units.Hom (4.9s)
✔ [641/693] Built Mathlib.Algebra.Ring.Nat (3.3s)
✔ [642/693] Built Mathlib.Algebra.GroupWithZero.Hom (4.5s)
✔ [643/693] Built Mathlib.Tactic.TFAE (7.4s)
✔ [644/695] Built Mathlib.Algebra.Group.Hom.Instances (7.3s)
✔ [645/695] Built Mathlib.Order.GaloisConnection.Defs (3.9s)
✔ [646/696] Built Mathlib.Algebra.GroupWithZero.Opposite (3.5s)
✔ [647/696] Built Mathlib.Algebra.Group.Action.Opposite (5.1s)
✔ [648/704] Built Mathlib.Logic.Equiv.Prod (28s)
✔ [649/704] Built Mathlib.Algebra.Group.TypeTags.Hom (4.5s)
✔ [650/704] Built Mathlib.Algebra.Ring.Semiconj (2.4s)
✔ [651/704] Built Mathlib.Order.Lattice (7.8s)
✔ [652/704] Built Mathlib.Algebra.Group.Semiconj.Units (3.4s)
✔ [653/704] Built Mathlib.Tactic.Nontriviality.Core (4.3s)
✔ [654/704] Built Mathlib.Algebra.Ring.Basic (3.9s)
✔ [655/704] Built Mathlib.Data.Bracket (1.6s)
✔ [656/704] Built Mathlib.Algebra.Group.Nat.Hom (3.2s)
✔ [657/704] Built Mathlib.Algebra.GroupWithZero.Action.Defs (5.9s)
✔ [658/704] Built Mathlib.Order.BoundedOrder.Lattice (3.0s)
✔ [659/704] Built Mathlib.Logic.Equiv.Sum (5.1s)
✔ [660/704] Built Mathlib.Tactic.Nontriviality (3.2s)
✔ [661/704] Built Mathlib.Algebra.Group.Equiv.TypeTags (5.7s)
✔ [662/705] Built Mathlib.Algebra.Group.Commute.Units (4.0s)
✔ [663/710] Built Mathlib.Algebra.Ring.InjSurj (8.6s)
✔ [664/719] Built Mathlib.Algebra.Module.Defs (4.3s)
✔ [665/723] Built Mathlib.Logic.OpClass (2.3s)
✔ [666/723] Built Mathlib.Algebra.Group.Prod (10s)
✔ [667/727] Built Mathlib.Algebra.Order.Monoid.Unbundled.Defs (5.1s)
✔ [668/727] Built Mathlib.Data.Prod.PProd (2.2s)
✔ [669/730] Built Mathlib.Order.Disjoint (6.6s)
✔ [670/731] Built Mathlib.Algebra.GroupWithZero.Units.Basic (6.5s)
✔ [671/734] Built Mathlib.Algebra.Ring.Hom.Defs (7.2s)
✔ [672/734] Built Mathlib.Order.MinMax (3.3s)
✔ [673/737] Built Mathlib.Algebra.Order.ZeroLEOne (2.4s)
✔ [674/737] Built Mathlib.Tactic.Bound.Init (2.5s)
✔ [675/739] Built Mathlib.Logic.Equiv.Basic (9.3s)
✔ [676/739] Built Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (4.1s)
✔ [677/739] Built Mathlib.Algebra.GroupWithZero.Semiconj (3.1s)
✔ [678/739] Built Mathlib.Order.PropInstances (3.4s)
✔ [679/742] Built Mathlib.Algebra.Order.Group.Synonym (6.4s)
✔ [680/742] Built Mathlib.Algebra.Ring.Units (3.3s)
✔ [681/742] Built Mathlib.Algebra.Ring.GrindInstances (2.8s)
✔ [682/742] Built Mathlib.Order.Bounds.Defs (2.7s)
✔ [683/742] Built Mathlib.Tactic.Bound.Attribute (4.6s)
✔ [685/742] Built Mathlib.Logic.Embedding.Basic (5.7s)
✔ [686/742] Built Mathlib.Algebra.GroupWithZero.Commute (5.7s)
✔ [687/742] Built Mathlib.Data.Nat.Cast.NeZero (5.1s)
✔ [688/748] Built Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual (6.0s)
✔ [690/748] Built Mathlib.Algebra.Group.Equiv.Basic (9.0s)
✔ [691/750] Built Mathlib.Data.Option.NAry (3.1s)
✔ [693/750] Built Mathlib.Algebra.Ring.Commute (8.6s)
✔ [694/750] Built Mathlib.Algebra.GroupWithZero.Regular (4.5s)
✔ [695/750] Built Mathlib.Data.Set.Basic (12s)
✔ [696/750] Built Mathlib.Algebra.Order.Monoid.Unbundled.Basic (16s)
✔ [697/750] Built Mathlib.Order.Heyting.Basic (14s)
✔ [698/750] Built Mathlib.Algebra.GroupWithZero.Equiv (3.4s)
✔ [700/750] Built Mathlib.Data.Set.Inclusion (3.4s)
✔ [701/750] Built Mathlib.Data.Nat.Cast.Commute (4.2s)
✔ [702/750] Built Mathlib.Order.RelIso.Basic (9.7s)
✔ [703/750] Built Mathlib.Algebra.Group.Equiv.Opposite (7.0s)
✔ [704/750] Built Mathlib.Algebra.Group.Units.Equiv (6.6s)
✔ [705/750] Built Mathlib.Data.Set.Disjoint (5.3s)
✔ [707/750] Built Mathlib.Algebra.Order.Monoid.NatCast (4.7s)
✔ [708/754] Built Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (5.8s)
✔ [709/754] Built Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE (5.2s)
✔ [710/754] Built Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (17s)
✔ [711/756] Built Mathlib.Algebra.Order.Monoid.Defs (5.3s)
✔ [712/758] Built Mathlib.Algebra.Order.Sub.Defs (5.5s)
✔ [713/758] Built Mathlib.Algebra.Order.Monoid.Unbundled.Pow (7.8s)
✔ [714/758] Built Mathlib.Order.BooleanAlgebra.Defs (5.2s)
✔ [715/758] Built Mathlib.Order.TypeTags (3.1s)
✔ [716/759] Built Mathlib.Algebra.Regular.Basic (4.0s)
✔ [717/759] Built Mathlib.Algebra.Group.Even (5.8s)
✔ [719/763] Built Mathlib.Algebra.Order.Group.Int (3.5s)
✔ [720/763] Built Mathlib.Data.Set.Insert (6.8s)
✔ [721/768] Built Mathlib.Algebra.Order.Monoid.Canonical.Defs (5.4s)
✔ [722/770] Built Mathlib.Algebra.Order.Monoid.OrderDual (3.7s)
✔ [723/770] Built Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags (3.0s)
✔ [724/770] Built Mathlib.Algebra.Group.Nat.Even (5.1s)
✔ [725/770] Built Mathlib.Data.Set.Subsingleton (4.6s)
✔ [726/770] Built Mathlib.Order.BooleanAlgebra.Basic (8.8s)
✔ [729/770] Built Mathlib.Algebra.Order.Group.Unbundled.Basic (9.9s)
✔ [733/771] Built Mathlib.Algebra.Order.Group.Nat (3.7s)
✔ [734/771] Built Mathlib.Order.Hom.Basic (13s)
✔ [736/771] Built Mathlib.Order.Interval.Set.Defs (2.4s)
✔ [737/771] Built Mathlib.Algebra.Order.Sub.Unbundled.Basic (4.0s)
✔ [738/771] Built Mathlib.Algebra.Order.Monoid.TypeTags (3.1s)
✔ [739/772] Built Mathlib.Util.AtomM.Recurse (2.9s)
✔ [740/773] Built Mathlib.Algebra.Order.Group.Defs (4.5s)
✔ [741/773] Built Mathlib.Order.BooleanAlgebra.Set (6.0s)
✔ [742/774] Built Mathlib.Order.SymmDiff (7.1s)
✔ [743/774] Built Mathlib.Algebra.Order.Group.OrderIso (5.3s)
✔ [744/774] Built Mathlib.Algebra.Order.Monoid.Units (5.0s)
✔ [745/774] Built Mathlib.Tactic.HaveI (2.3s)
✔ [746/776] Built Mathlib.Algebra.Order.Sub.Basic (4.9s)
✔ [747/785] Built Mathlib.Algebra.Group.Invertible.Defs (4.4s)
✔ [748/785] Built Mathlib.Lean.Expr.Rat (1.0s)
✔ [749/787] Built Mathlib.Algebra.Order.Ring.Unbundled.Basic (10s)
✔ [750/787] Built Mathlib.Data.Rat.Init (1.0s)
✔ [751/787] Built Mathlib.Data.Set.SymmDiff (3.9s)
✔ [752/787] Built Mathlib.Algebra.Order.Group.Units (3.1s)
✔ [753/787] Built Mathlib.Util.Qq (2.3s)
✔ [754/787] Built Mathlib.Algebra.Order.Group.Lattice (4.2s)
✔ [755/790] Built Mathlib.Tactic.TryThis (1.7s)
✔ [756/792] Built Mathlib.Order.WithBot (20s)
✔ [757/792] Built Mathlib.Algebra.Group.Invertible.Basic (3.5s)
✔ [759/797] Built Mathlib.Algebra.Field.Defs (3.0s)
✔ [760/797] Built Mathlib.Data.Nat.Find (3.3s)
✔ [761/802] Built Mathlib.Algebra.Order.Ring.Defs (3.8s)
✔ [763/805] Built Mathlib.Algebra.GroupWithZero.Units.Lemmas (2.9s)
✔ [764/805] Built Mathlib.Algebra.GroupWithZero.Invertible (2.0s)
✔ [765/809] Built Mathlib.Util.PPOptions (1.3s)
✔ [766/809] Built Mathlib.Algebra.Group.Nat.Units (2.6s)
✔ [767/809] Built Mathlib.Algebra.Order.Group.Unbundled.Abs (5.6s)
✔ [768/809] Built Mathlib.Data.Int.LeastGreatest (3.4s)
✔ [769/810] Built Mathlib.Order.BoundedOrder.Monotone (3.6s)
✔ [770/810] Built Mathlib.Data.Set.Image (9.1s)
✔ [771/810] Built Mathlib.Algebra.Ring.Invertible (5.1s)
✔ [772/812] Built Mathlib.Algebra.Group.Int.Units (4.1s)
✔ [773/812] Built Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (10s)
✔ [774/812] Built Mathlib.Tactic.NormNum.Result (6.6s)
✔ [775/812] Built Mathlib.Order.Interval.Set.Basic (7.0s)
✔ [776/812] Built Mathlib.Control.Basic (1.8s)
✔ [777/815] Built Mathlib.Algebra.Order.Group.Unbundled.Int (3.7s)
✔ [778/815] Built Mathlib.Data.Set.Restrict (3.3s)
✔ [780/816] Built Mathlib.Algebra.Order.Group.Abs (6.5s)
✔ [781/817] Built Mathlib.Algebra.Ring.Int.Units (3.2s)
✔ [782/819] Built Mathlib.Data.Ineq (1.6s)
✔ [783/820] Built Mathlib.Tactic.FieldSimp.Attr (1.0s)
✔ [784/823] Built Mathlib.Algebra.Order.Monoid.WithTop (4.2s)
✔ [785/823] Built Mathlib.Util.DischargerAsTactic (1.0s)
✔ [786/826] Built Mathlib.Util.Delaborators (12s)
✔ [787/826] Built Mathlib.Tactic.NormNum.Core (6.4s)
✔ [790/829] Built Mathlib.Algebra.GroupWithZero.Units.Equiv (5.0s)
✔ [792/833] Built Mathlib.Control.Functor (2.2s)
✔ [794/833] Built Mathlib.Data.List.Monad (1.5s)
✔ [795/836] Built Mathlib.Algebra.Field.Basic (8.8s)
✔ [798/850] Built Mathlib.Algebra.BigOperators.Group.List.Defs (3.7s)
✔ [805/853] Built Mathlib.Data.Set.Prod (9.0s)
✔ [806/853] Built Mathlib.Util.SynthesizeUsing (1.9s)
✔ [808/853] Built Mathlib.Order.Directed (3.9s)
✔ [809/853] Built Mathlib.Algebra.Order.AddGroupWithTop (4.8s)
✔ [810/853] Built Mathlib.Data.PNat.Notation (1.0s)
✔ [811/860] Built Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (3.5s)
✔ [812/861] Built Mathlib.Data.List.Defs (2.9s)
✔ [819/865] Built Mathlib.Algebra.Group.Semiconj.Basic (3.7s)
✔ [820/865] Built Mathlib.Order.Nat (4.9s)
✔ [821/865] Built Mathlib.Lean.Meta.Tactic.Rewrite (4.3s)
✔ [822/869] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (5.7s)
✔ [823/869] Built Mathlib.Data.PNat.Defs (8.3s)
✔ [824/869] Built Mathlib.Data.Set.NAry (9.5s)
✔ [826/869] Built Mathlib.Data.Tree.Basic (5.0s)
✔ [827/872] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm (4.7s)
✔ [829/873] Built Mathlib.Algebra.Group.Commute.Basic (9.1s)
✔ [833/874] Built Mathlib.Tactic.Zify (6.5s)
✔ [835/880] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss (3.0s)
✔ [836/880] Built Mathlib.Util.ElabWithoutMVars (3.2s)
✔ [837/886] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector (1.6s)
✔ [838/886] Built Mathlib.Control.ULift (1.7s)
✔ [839/889] Built Mathlib.Logic.Pairwise (3.5s)
✔ [840/892] Built Mathlib.Data.Bool.Set (3.9s)
✔ [841/892] Built Mathlib.Data.Set.Function (14s)
✔ [845/892] Built Mathlib.Data.Nat.Set (3.7s)
✔ [846/892] Built Mathlib.Data.ULift (2.5s)
✔ [847/892] Built Mathlib.Data.Set.Order (3.2s)
✔ [852/894] Built Mathlib.Order.Bounds.Basic (17s)
✔ [855/894] Built Mathlib.Tactic.CancelDenoms.Core (8.2s)
✔ [856/894] Built Mathlib.Order.WellFounded (4.5s)
✔ [865/895] Built Mathlib.Order.Interval.Set.Image (5.0s)
✔ [869/895] Built Mathlib.Lean.Expr.ExtraRecognizers (1.5s)
✔ [870/902] Built Mathlib.Data.Set.Monotone (5.0s)
✔ [872/902] Built Mathlib.Data.Set.Piecewise (5.1s)
✔ [873/905] Built Mathlib.Order.SetNotation (8.8s)
✔ [874/905] Built Mathlib.Order.Interval.Set.LinearOrder (8.0s)
✔ [876/905] Built Mathlib.Order.LatticeIntervals (6.3s)
✔ [877/907] Built Mathlib.Order.Bounds.Image (5.2s)
✔ [879/910] Built Mathlib.Logic.Equiv.Set (8.6s)
✔ [880/911] Built Mathlib.Data.Set.Notation (3.4s)
✔ [881/911] Built Mathlib.Tactic.SetLike (3.2s)
✔ [883/914] Built Mathlib.Data.Set.Pairwise.Basic (4.9s)
✔ [888/919] Built Mathlib.Algebra.Group.Action.Pi (4.3s)
✔ [890/921] Built Mathlib.Order.ConditionallyCompleteLattice.Defs (3.6s)
✔ [891/929] Built Mathlib.Order.CompleteLattice.Defs (4.0s)
✔ [892/929] Built Mathlib.Algebra.Order.Monoid.Basic (3.3s)
✔ [893/929] Built Mathlib.Algebra.Notation (2.5s)
✔ [894/929] Built Mathlib.Algebra.Order.Positive.Ring (3.8s)
✔ [895/935] Built Mathlib.Data.Int.Cast.Pi (1.6s)
✔ [896/939] Built Mathlib.Data.SetLike.Basic (3.7s)
✔ [898/940] Built Mathlib.Order.Hom.Set (4.2s)
✔ [899/940] Built Mathlib.Data.Int.Cast.Field (3.0s)
✔ [900/940] Built Mathlib.Data.PNat.Equiv (2.4s)
✔ [901/940] Built Mathlib.Algebra.Notation.Support (4.6s)
✔ [902/944] Built Mathlib.Algebra.Order.Ring.InjSurj (3.1s)
✔ [906/944] Built Mathlib.Algebra.Order.Hom.Basic (4.4s)
✔ [908/956] Built Mathlib.Algebra.Order.Group.Basic (3.6s)
✔ [918/957] Built Mathlib.Order.Preorder.Chain (4.2s)
✔ [919/957] Built Mathlib.Algebra.Order.Group.PosPart (5.6s)
✔ [920/959] Built Mathlib.Order.Bounds.OrderIso (3.9s)
✔ [930/991] Built Mathlib.Algebra.AddTorsor.Defs (3.9s)
✔ [931/1003] Built Mathlib.Data.Set.List (3.4s)
✔ [945/1007] Built Mathlib.Algebra.Group.Action.Units (5.0s)
✔ [946/1007] Built Mathlib.Data.Finset.Attr (2.9s)
✔ [953/1029] Built Mathlib.Data.Int.DivMod (2.4s)
✔ [973/1029] Built Mathlib.Algebra.Group.Pointwise.Set.Scalar (6.3s)
✔ [974/1033] Built Mathlib.Data.Finite.Defs (3.6s)
✔ [987/1037] Built Mathlib.Order.Antichain (5.2s)
✔ [990/1039] Built Mathlib.Data.List.Flatten (3.5s)
✔ [991/1046] Built Mathlib.Order.CompleteLattice.Basic (9.6s)
✔ [992/1049] Built Mathlib.Data.List.Pairwise (3.3s)
✔ [994/1049] Built Mathlib.Logic.Function.DependsOn (3.0s)
✔ [995/1053] Built Mathlib.Algebra.Group.Action.Basic (4.1s)
✔ [1006/1054] Built Mathlib.Algebra.Group.Action.TypeTags (2.8s)
✔ [1007/1058] Built Mathlib.Order.CompleteLattice.Lemmas (3.0s)
✔ [1008/1059] Built Mathlib.Order.GaloisConnection.Basic (4.4s)
✔ [1009/1064] Built Mathlib.Algebra.Group.Subsemigroup.Defs (4.6s)
✔ [1010/1064] Built Mathlib.Data.Countable.Defs (2.8s)
✔ [1012/1064] Built Mathlib.Algebra.Group.Action.Pretransitive (3.0s)
✔ [1014/1066] Built Mathlib.Tactic.ApplyFun (4.3s)
✔ [1015/1066] Built Mathlib.Data.Nat.Bits (2.9s)
✔ [1016/1068] Built Mathlib.Algebra.Group.Pi.Lemmas (7.0s)
✔ [1017/1076] Built Mathlib.Algebra.Group.Idempotent (3.0s)
✔ [1021/1076] Built Mathlib.Data.Sigma.Lex (2.1s)
✔ [1022/1089] Built Mathlib.Algebra.Group.Action.Hom (3.5s)
✔ [1029/1089] Built Mathlib.Data.Prod.Lex (5.1s)
✔ [1030/1093] Built Mathlib.Algebra.Group.Submonoid.Defs (6.7s)
✔ [1032/1093] Built Mathlib.Algebra.Group.Embedding (3.2s)
✔ [1033/1093] Built Mathlib.Logic.Embedding.Set (4.7s)
✔ [1034/1105] Built Mathlib.Algebra.Group.Pointwise.Set.Basic (14s)
✔ [1037/1112] Built Mathlib.Order.Hom.Bounded (6.8s)
✔ [1039/1113] Built Mathlib.Order.CompleteBooleanAlgebra (10s)
✔ [1040/1122] Built Mathlib.Order.Antisymmetrization (4.8s)
✔ [1041/1122] Built Mathlib.Order.Interval.Set.WithBotTop (3.6s)
✔ [1042/1129] Built Mathlib.Algebra.Group.Submonoid.MulAction (4.1s)
✔ [1045/1137] Built Mathlib.Order.RelIso.Set (3.5s)
✔ [1046/1137] Built Mathlib.Order.Hom.Lattice (7.3s)
✔ [1047/1139] Built Mathlib.Data.Nat.Order.Lemmas (3.3s)
✔ [1049/1141] Built Mathlib.Data.Set.BooleanAlgebra (3.9s)
✔ [1051/1141] Built Mathlib.Algebra.Group.Commute.Hom (3.6s)
✔ [1052/1145] Built Mathlib.Algebra.Group.Support (4.2s)
✔ [1054/1149] Built Mathlib.Order.Minimal (6.7s)
✔ [1056/1149] Built Mathlib.Algebra.Group.Commutator (3.1s)
✔ [1057/1151] Built Mathlib.Data.Setoid.Basic (5.8s)
✔ [1058/1152] Built Mathlib.GroupTheory.OreLocalization.OreSet (7.7s)
✔ [1060/1153] Built Mathlib.Data.Set.Sigma (12s)
✔ [1061/1153] Built Mathlib.Order.Hom.BoundedLattice (16s)
✔ [1065/1153] Built Mathlib.Algebra.Order.GroupWithZero.Synonym (4.8s)
✔ [1067/1153] Built Mathlib.Data.Set.Lattice (15s)
✔ [1068/1153] Built Mathlib.Data.ENat.Defs (2.9s)
✔ [1069/1153] Built Mathlib.Algebra.Order.Sub.WithTop (4.3s)
✔ [1070/1153] Built Mathlib.Algebra.Group.Center (21s)
✔ [1071/1161] Built Mathlib.GroupTheory.Congruence.Defs (15s)
✔ [1072/1161] Built Mathlib.Algebra.Order.Hom.Monoid (17s)
✔ [1074/1164] Built Mathlib.Algebra.Ring.Equiv (17s)
✔ [1076/1178] Built Mathlib.Order.Hom.WithTopBot (7.2s)
✔ [1084/1179] Built Mathlib.Data.Set.Pairwise.Lattice (5.7s)
✔ [1087/1186] Built Mathlib.GroupTheory.Subsemigroup.Center (4.5s)
✔ [1089/1190] Built Mathlib.Order.Iterate (4.7s)
✔ [1091/1190] Built Mathlib.Logic.Small.Defs (4.1s)
✔ [1092/1191] Built Mathlib.Control.Traversable.Basic (2.7s)
✔ [1093/1192] Built Mathlib.Control.Applicative (4.5s)
✔ [1098/1193] Built Mathlib.Logic.UnivLE (3.4s)
✔ [1099/1198] Built Mathlib.SetTheory.Cardinal.Defs (4.8s)
✔ [1100/1198] Built Mathlib.Order.ConditionallyCompleteLattice.Basic (10s)
✔ [1103/1198] Built Mathlib.GroupTheory.Congruence.Hom (8.8s)
✔ [1107/1198] Built Mathlib.Logic.Small.Basic (3.7s)
✔ [1111/1205] Built Mathlib.Control.Monad.Basic (2.3s)
✔ [1117/1205] Built Mathlib.Order.Hom.Order (3.9s)
✔ [1124/1205] Built Mathlib.Order.ScottContinuity (3.7s)
✔ [1129/1209] Built Mathlib.Logic.Small.Set (3.0s)
✔ [1130/1212] Built Mathlib.Data.Countable.Small (3.6s)
✔ [1131/1216] Built Mathlib.Data.Set.Lattice.Image (16s)
✔ [1135/1216] Built Mathlib.Data.Sum.Order (10s)
✔ [1136/1216] Built Mathlib.Order.CompleteLattice.Chain (4.1s)
✔ [1137/1216] Built Mathlib.Data.Part (6.1s)
✔ [1138/1216] Built Mathlib.Order.ConditionallyCompleteLattice.Indexed (6.7s)
✔ [1145/1216] Built Mathlib.Logic.Function.CompTypeclasses (1.8s)
✔ [1149/1216] Built Mathlib.Algebra.GroupWithZero.Action.Units (4.5s)
✔ [1150/1216] Built Mathlib.Algebra.Ring.CompTypeclasses (4.0s)
✔ [1154/1217] Built Mathlib.Algebra.Regular.SMul (3.8s)
✔ [1155/1219] Built Mathlib.Data.Nat.Pairing (3.9s)
✔ [1158/1219] Built Mathlib.Algebra.Group.Subsemigroup.Basic (5.2s)
✔ [1159/1220] Built Mathlib.Algebra.Group.Hom.CompTypeclasses (3.5s)
✔ [1161/1220] Built Mathlib.Order.Zorn (4.3s)
✔ [1162/1220] Built Mathlib.Algebra.Group.Pointwise.Set.Lattice (5.7s)
✔ [1163/1221] Built Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (7.2s)
✔ [1165/1224] Built Mathlib.Algebra.GroupWithZero.Action.End (3.6s)
✔ [1166/1224] Built Mathlib.Order.Hom.Lex (6.0s)
✔ [1167/1226] Built Mathlib.Logic.Equiv.Nat (2.0s)
✔ [1171/1226] Built Mathlib.Algebra.Group.Action.Prod (4.1s)
✔ [1176/1230] Built Mathlib.GroupTheory.Subsemigroup.Centralizer (2.9s)
✔ [1184/1236] Built Mathlib.Algebra.Group.Hom.End (3.3s)
✔ [1186/1236] Built Mathlib.Algebra.Ring.Action.Basic (3.3s)
✔ [1187/1236] Built Mathlib.Algebra.GroupWithZero.Action.Hom (3.5s)
✔ [1188/1238] Built Mathlib.Algebra.Group.Subsemigroup.MulOpposite (4.1s)
✔ [1189/1241] Built Mathlib.Algebra.GroupWithZero.Pi (2.4s)
✔ [1191/1241] Built Mathlib.Algebra.Module.RingHom (3.2s)
✔ [1192/1241] Built Mathlib.Algebra.Group.Submonoid.Basic (5.2s)
✔ [1194/1241] Built Mathlib.Algebra.GroupWithZero.Action.Opposite (2.4s)
✔ [1195/1246] Built Mathlib.Algebra.Regular.Opposite (2.4s)
✔ [1196/1246] Built Mathlib.Algebra.Ring.Opposite (5.3s)
✔ [1197/1246] Built Mathlib.Algebra.GroupWithZero.Action.Prod (3.0s)
✔ [1198/1253] Built Mathlib.Algebra.Group.Submonoid.MulOpposite (3.4s)
✔ [1201/1255] Built Mathlib.Algebra.Ring.Pi (4.1s)
✔ [1203/1259] Built Mathlib.GroupTheory.GroupAction.DomAct.Basic (4.9s)
✔ [1205/1264] Built Mathlib.Algebra.Group.Submonoid.DistribMulAction (2.7s)
✔ [1207/1268] Built Mathlib.Algebra.Module.Opposite (2.3s)
✔ [1211/1270] Built Mathlib.Algebra.Module.Prod (2.2s)
✔ [1212/1271] Built Mathlib.Algebra.Group.PUnit (2.2s)
✔ [1213/1272] Built Mathlib.Data.Nat.Cast.Prod (2.7s)
✔ [1214/1272] Built Mathlib.Algebra.Group.ULift (3.8s)
✔ [1215/1273] Built Mathlib.Algebra.Group.Subsemigroup.Membership (2.0s)
✔ [1217/1277] Built Mathlib.RingTheory.NonUnitalSubsemiring.Defs (4.6s)
✔ [1218/1277] Built Mathlib.Algebra.Ring.PUnit (2.4s)
✔ [1219/1277] Built Mathlib.Order.Hom.CompleteLattice (6.1s)
✔ [1221/1280] Built Mathlib.Algebra.GroupWithZero.Center (2.7s)
✔ [1222/1280] Built Mathlib.Data.Int.Cast.Prod (2.7s)
✔ [1223/1280] Built Mathlib.Algebra.GroupWithZero.ULift (2.5s)
✔ [1225/1282] Built Mathlib.Algebra.Ring.Centralizer (2.2s)
✔ [1226/1288] Built Mathlib.Algebra.Ring.Submonoid.Basic (2.5s)
✔ [1228/1297] Built Mathlib.Algebra.Ring.ULift (4.6s)
✔ [1232/1298] Built Mathlib.Algebra.Group.Submonoid.Operations (12s)
✔ [1245/1301] Built Mathlib.Algebra.Group.Subsemigroup.Operations (7.0s)
✔ [1248/1309] Built Mathlib.Algebra.Ring.Hom.InjSurj (2.1s)
✔ [1252/1360] Built Mathlib.Algebra.Module.PUnit (2.6s)
✔ [1274/1363] Built Mathlib.Algebra.Ring.Subsemiring.Defs (4.3s)
✔ [1276/1380] Built Mathlib.GroupTheory.GroupAction.Hom (16s)
✔ [1289/1380] Built Mathlib.Algebra.Group.Irreducible.Defs (2.4s)
✔ [1291/1381] Built Mathlib.Order.Interval.Set.OrderIso (2.7s)
✔ [1292/1392] Built Mathlib.Order.Closure (4.5s)
✔ [1304/1393] Built Mathlib.GroupTheory.Submonoid.Center (4.5s)
✔ [1313/1398] Built Mathlib.Algebra.Notation.Indicator (3.9s)
✔ [1330/1398] Built Mathlib.Algebra.EuclideanDomain.Defs (3.7s)
✔ [1337/1407] Built Mathlib.Algebra.Group.ModEq (4.0s)
✔ [1349/1413] Built Mathlib.Algebra.Group.Irreducible.Lemmas (3.2s)
✔ [1357/1422] Built Mathlib.Algebra.Order.Interval.Set.Monoid (2.6s)
✔ [1361/1487] Built Mathlib.GroupTheory.Congruence.Basic (5.3s)
✔ [1404/1487] Built Mathlib.RingTheory.Congruence.Defs (5.6s)
✔ [1406/1513] Built Mathlib.GroupTheory.Submonoid.Centralizer (3.3s)
✔ [1441/1515] Built Mathlib.Algebra.EuclideanDomain.Int (2.0s)
✔ [1442/1515] Built Mathlib.Algebra.GroupWithZero.Idempotent (2.8s)
✔ [1445/1517] Built Mathlib.Algebra.Group.Indicator (4.0s)
✔ [1489/1536] Built Mathlib.Algebra.Ring.Action.Rat (2.7s)
✔ [1492/1565] Built Mathlib.Order.Interval.Set.Disjoint (3.9s)
✔ [1493/1565] Built Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic (3.1s)
✔ [1515/1612] Built Mathlib.Algebra.Order.Group.Action (3.6s)
✔ [1547/1612] Built Mathlib.Order.Filter.Defs (5.3s)
✔ [1548/1646] Built Mathlib.Algebra.Ring.Idempotent (4.3s)
✔ [1588/1648] Built Mathlib.RingTheory.Congruence.Basic (5.7s)
✔ [1590/1651] Built Mathlib.Algebra.EuclideanDomain.Field (3.9s)
✔ [1591/1652] Built Mathlib.GroupTheory.Congruence.Opposite (2.9s)
✔ [1593/1653] Built Mathlib.Algebra.Order.GroupWithZero.Submonoid (2.9s)
✔ [1594/1679] Built Mathlib.Data.Set.UnionLift (3.6s)
✔ [1615/1709] Built Mathlib.Algebra.Group.Pi.Units (3.1s)
✔ [1628/1742] Built Mathlib.Tactic.ContinuousFunctionalCalculus (5.5s)
✔ [1631/1742] Built Mathlib.Tactic.Order.CollectFacts (10s)
✔ [1632/1742] Built Mathlib.Algebra.Notation.Lemmas (5.4s)
✔ [1633/1742] Built Mathlib.Data.Nat.Cast.WithTop (5.8s)
✔ [1634/1745] Built Mathlib.RingTheory.Congruence.Opposite (6.6s)
✔ [1635/1745] Built Mathlib.Algebra.Order.Group.Opposite (7.2s)
✔ [1660/1745] Built Mathlib.Algebra.Order.Monoid.Submonoid (6.6s)
✔ [1666/1747] Built Mathlib.Order.Filter.Basic (11s)
✔ [1667/1747] Built Mathlib.GroupTheory.GroupAction.Ring (4.5s)
✔ [1668/1762] Built Mathlib.Tactic.Order.Graph.Basic (3.9s)
✔ [1669/1762] Built Mathlib.Data.Nat.WithBot (3.6s)
✔ [1685/1803] Built Mathlib.Tactic.Order.Preprocessing (5.2s)
✔ [1702/1820] Built Mathlib.Tactic.Order.ToInt (6.2s)
✔ [1703/1820] Built Mathlib.Algebra.Order.Pi (5.0s)
✔ [1712/1825] Built Mathlib.Algebra.Ring.Subsemiring.Order (3.7s)
✔ [1716/1825] Built Mathlib.Order.Filter.AtTopBot.Defs (3.0s)
✔ [1717/1827] Built Mathlib.Tactic.Order.Graph.Tarjan (4.2s)
✔ [1719/1848] Built Mathlib.Data.Nat.Log (5.3s)
✔ [1734/1852] Built Mathlib.Algebra.Order.Group.MinMax (4.4s)
✔ [1740/1882] Built Mathlib.Order.Filter.Map (6.6s)
✔ [1741/1882] Built Mathlib.Order.Filter.AtTopBot.Disjoint (3.5s)
✔ [1742/1882] Built Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (4.5s)
✔ [1747/1882] Built Mathlib.Algebra.Order.Group.Pointwise.Bounds (5.2s)
✔ [1748/1882] Built Mathlib.Tactic.Continuity.Init (1.9s)
✔ [1749/1886] Built Mathlib.Tactic.ProxyType (5.9s)
✔ [1754/1906] Built Mathlib.Tactic.TautoSet (2.5s)
✔ [1759/1913] Built Mathlib.Tactic.Order (4.8s)
✔ [1770/1931] Built Mathlib.Order.Filter.Ker (3.2s)
✔ [1772/1935] Built Mathlib.Order.Filter.Tendsto (3.5s)
✔ [1774/1935] Built Mathlib.Tactic.Continuity (2.5s)
✔ [1775/1935] Built Mathlib.Data.Set.Functor (4.1s)
✔ [1779/1936] Built Mathlib.Data.Set.BoolIndicator (3.2s)
✔ [1780/1936] Built Mathlib.Order.Filter.Bases.Basic (5.7s)
✔ [1811/1942] Built Mathlib.Algebra.GroupWithZero.Indicator (3.1s)
✔ [1813/1998] Built Mathlib.Order.Filter.AtTopBot.Map (3.0s)
✔ [1819/1999] Built Mathlib.Order.Filter.AtTopBot.Tendsto (3.3s)
✔ [1820/1999] Built Mathlib.Topology.Defs.Basic (3.8s)
✔ [1822/1999] Built Mathlib.Tactic.SuppressCompilation (3.0s)
✔ [1823/1999] Built Mathlib.Order.OrdContinuous (3.7s)
✔ [1825/1999] Built Mathlib.Data.Set.Subset (4.2s)
✔ [1826/2002] Built Mathlib.Order.Filter.AtTopBot.CompleteLattice (3.4s)
✔ [1843/2022] Built Mathlib.Order.Filter.Prod (7.6s)
✔ [1844/2022] Built Mathlib.Order.Filter.AtTopBot.Monoid (3.5s)
✔ [1845/2022] Built Mathlib.Topology.ContinuousMap.Defs (3.1s)
✔ [1846/2034] Built Mathlib.Order.Filter.AtTopBot.Basic (3.9s)
✔ [1848/2034] Built Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice (12s)
✔ [1901/2035] Built Mathlib.Topology.Defs.Filter (4.3s)
✔ [1913/2039] Built Mathlib.Order.Filter.NAry (3.5s)
✔ [1915/2047] Built Mathlib.Data.Sym.Sym2.Init (2.7s)
✔ [1917/2047] Built Mathlib.Order.Filter.Curry (3.4s)
✔ [1924/2066] Built Mathlib.Order.Filter.Lift (4.2s)
✔ [1929/2066] Built Mathlib.Order.Interval.Basic (6.6s)
✔ [1960/2098] Built Mathlib.CategoryTheory.Category.Init (2.6s)
✔ [1961/2126] Built Mathlib.Data.Opposite (2.5s)
✔ [1962/2126] Built Mathlib.Tactic.CategoryTheory.CategoryStar (1.5s)
✔ [1963/2141] Built Mathlib.Order.Filter.AtTopBot.Group (4.3s)
✔ [1964/2150] Built Mathlib.CategoryTheory.ConcreteCategory.Bundled (1.3s)
✔ [1984/2226] Built Mathlib.Logic.Lemmas (2.6s)
✔ [1998/2266] Built Mathlib.Order.Filter.SmallSets (3.0s)
✔ [2041/2267] Built Mathlib.Combinatorics.Quiver.Basic (2.9s)
✔ [2044/2287] Built Mathlib.Order.Interval.Lex (3.7s)
✔ [2055/2402] Built Mathlib.Algebra.Group.Ext (3.4s)
✔ [2069/2402] Built Mathlib.Data.Rel (18s)
✔ [2070/2402] Built Mathlib.Order.Filter.AtTopBot.Ring (3.8s)
✔ [2071/2424] Built Mathlib.Data.List.Iterate (3.1s)
✔ [2080/2444] Built Mathlib.Tactic.CategoryTheory.Coherence.Datatypes (2.9s)
✔ [2081/2444] Built Mathlib.RingTheory.LocalRing.Defs (2.2s)
✔ [2082/2449] Built Mathlib.Combinatorics.Quiver.Prefunctor (2.8s)
✔ [2087/2449] Built Mathlib.Algebra.Homology.ComplexShape (2.2s)
✔ [2088/2449] Built Mathlib.Data.Rel.Separated (2.6s)
✔ [2097/2449] Built Mathlib.Topology.Defs.Sequences (2.9s)
✔ [2134/2528] Built Mathlib.Order.Heyting.Hom (5.9s)
✔ [2167/2532] Built Mathlib.Combinatorics.Quiver.Push (2.5s)
✔ [2168/2532] Built Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence (2.8s)
✔ [2172/2550] Built Mathlib.Order.Filter.AtTopBot.Field (4.8s)
✔ [2181/2551] Built Mathlib.Combinatorics.Quiver.Path (3.6s)
✔ [2182/2551] Built Mathlib.Data.Rel.Cover (2.9s)
✔ [2213/2600] Built Mathlib.Tactic.CategoryTheory.Coherence.Normalize (5.8s)
✔ [2259/2661] Built Mathlib.Algebra.Homology.Embedding.Basic (4.2s)
✔ [2283/2697] Built Mathlib.Algebra.Group.Units.Opposite (2.8s)
✔ [2314/2711] Built Mathlib.Order.Circular (3.7s)
✔ [2325/2720] Built Mathlib.Combinatorics.Quiver.Cast (2.4s)
✔ [2328/2721] Built Mathlib.Algebra.Ring.Regular (2.8s)
✔ [2329/2733] Built Mathlib.Algebra.Order.Interval.Set.Group (5.0s)
✔ [2334/2734] Built Mathlib.Combinatorics.Quiver.Symmetric (3.7s)
✔ [2359/2742] Built Mathlib.Data.Matrix.DMatrix (3.4s)
✔ [2643/2912] Built Mathlib.Logic.Equiv.PartialEquiv (6.2s)
✔ [2921/3075] Built Mathlib.Order.Cofinal (3.3s)
✔ [2960/3089] Built Mathlib.Combinatorics.Quiver.SingleObj (2.4s)
✔ [2967/3091] Built Mathlib.RingTheory.OreLocalization.OreSet (3.1s)
✔ [2972/3110] Built Mathlib.Order.Copy (4.5s)
✔ [3046/3117] Built Mathlib.Algebra.Order.Ring.Idempotent (5.5s)
✔ [3056/3118] Built Mathlib.Algebra.Order.Hom.TypeTags (3.5s)
✔ [3057/3123] Built Mathlib.Data.Stream.Defs (1.0s)
✔ [3072/3125] Built Mathlib.Algebra.PEmptyInstances (2.2s)
✔ [3080/3143] Built Mathlib.Tactic.Monotonicity.Basic (1.8s)
✔ [3096/3146] Built Mathlib.Tactic.Peel (3.9s)
✔ [3122/3147] Built Mathlib.Algebra.Expr (2.1s)
✔ [3126/3149] Built Mathlib.Tactic.Monotonicity.Lemmas (2.4s)
✔ [3132/3150] Built Mathlib.Algebra.Group.MinimalAxioms (2.5s)
✔ [3136/3153] Built Mathlib.Algebra.Field.ModEq (2.9s)
✔ [3139/3155] Built Mathlib.Algebra.Group.Action.Option (2.3s)
✔ [3141/3159] Built Mathlib.Algebra.Group.Action.Sigma (2.4s)
✔ [3149/3170] Built Mathlib.Algebra.Field.ULift (3.4s)
✔ [3157/3182] Built Mathlib.Tactic.Monotonicity (2.9s)
✔ [3161/3182] Built Mathlib.Algebra.Group.Action.Sum (3.0s)
✔ [3170/3183] Built Mathlib.Algebra.Ring.MinimalAxioms (2.7s)
✔ [3172/3183] Built Mathlib.Algebra.Group.Int.TypeTags (2.6s)
✔ [3173/3183] Built Mathlib.Algebra.Group.Nat.TypeTags (2.7s)
✔ [3174/3227] Built Mathlib.Algebra.GroupWithZero.Action.Faithful (3.7s)
✔ [3222/3268] Built Mathlib.Algebra.Group.Pointwise.Set.Small (4.2s)
✔ [3375/3420] Built Mathlib.Algebra.HierarchyDesign (4.7s)
✔ [3381/3466] Built Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero (5.4s)
✔ [3407/3468] Built Mathlib.Algebra.Field.MinimalAxioms (4.9s)
✔ [3409/3498] Built Mathlib.Algebra.Free (9.0s)
✔ [3440/3502] Built Mathlib.Algebra.Homology.HasNoLoop (3.7s)
✔ [3444/3506] Built Mathlib.Combinatorics.Matroid.Init (3.3s)
✔ [3447/3518] Built Mathlib.Algebra.GroupWithZero.Submonoid.Instances (7.7s)
✔ [3458/3526] Built Mathlib.Util.Superscript (6.8s)
✔ [3486/3652] Built Mathlib.Algebra.Ring.Torsion (3.0s)
✔ [3547/3652] Built Mathlib.Tactic.Measurability.Init (3.4s)
✔ [3548/3711] Built Mathlib.Algebra.Module.MinimalAxioms (4.6s)
✔ [3575/3734] Built Mathlib.Algebra.Module.PointwisePi (5.1s)
✔ [3576/3736] Built Mathlib.GroupTheory.GroupAction.IterateAct (5.3s)
✔ [3577/3740] Built Mathlib.Data.Nat.NthRoot.Defs (3.2s)
✔ [3578/3750] Built Mathlib.Order.ConditionallyCompleteLattice.Group (6.2s)
✔ [3610/3813] Built Mathlib.Algebra.Order.Group.Indicator (7.9s)
✔ [3612/3822] Built Mathlib.Data.Int.ConditionallyCompleteOrder (6.3s)
✔ [3708/3971] Built Mathlib.Tactic.Measurability (6.0s)
✔ [3805/3980] Built Mathlib.Algebra.Order.Ring.Synonym (4.8s)
✔ [3809/3991] Built Mathlib.LinearAlgebra.AffineSpace.Defs (4.4s)
✔ [3849/3994] Built Mathlib.GroupTheory.GroupAction.Pointwise (8.1s)
✔ [3857/4000] Built Mathlib.Data.Int.NatAbs (4.7s)
✔ [3863/4002] Built Mathlib.Logic.Equiv.Embedding (5.4s)
✔ [3865/4003] Built Mathlib.Algebra.Order.Interval.Set.Instances (11s)
✔ [3867/4004] Built Mathlib.Order.Monotone.Monovary (6.8s)
✔ [3986/4006] Built Mathlib.Algebra.Order.AddTorsor (5.4s)
✔ [3987/4006] Built Mathlib.Tactic.ArithMult.Init (4.1s)
✔ [3992/4008] Built Mathlib.Algebra.Order.Field.Defs (3.5s)
✔ [3993/4011] Built Mathlib.Algebra.Order.Field.Pointwise (3.7s)
✔ [3997/4014] Built Mathlib.Algebra.Order.Group.End (3.1s)
✔ [3998/4015] Built Mathlib.Algebra.Order.Group.Action.Synonym (3.6s)
✔ [3999/4017] Built Mathlib.Algebra.Order.Group.Bounds (3.2s)
✔ [4001/4018] Built Mathlib.Tactic.ArithMult (3.9s)
✔ [4006/4024] Built Mathlib.Algebra.Order.Group.Equiv (3.7s)
✔ [4014/4040] Built Mathlib.Algebra.Order.Group.CompleteLattice (4.5s)
✔ [4030/4043] Built Mathlib.Algebra.Order.GroupWithZero.Bounds (3.1s)
✔ [4031/4044] Built Mathlib.Algebra.Order.Group.Action.End (3.0s)
✔ [4033/4045] Built Mathlib.Algebra.Order.Group.DenselyOrdered (5.4s)
✔ [4034/4046] Built Mathlib.Order.Prod.Lex.Hom (3.1s)
✔ [4035/4046] Built Mathlib.Algebra.Order.Hom.Submonoid (3.5s)
✔ [4037/4049] Built Mathlib.Algebra.Order.Hom.Units (3.1s)
✔ [4040/4058] Built Mathlib.Algebra.Order.Monoid.Unbundled.Units (3.4s)
✔ [4045/4066] Built Mathlib.Algebra.Order.Monoid.Prod (3.7s)
✔ [4054/4067] Built Mathlib.Algebra.Order.PUnit (3.2s)
✔ [4055/4069] Built Mathlib.Algebra.Order.Group.Action.Flag (3.4s)
✔ [4057/4093] Built Mathlib.Algebra.Order.Positive.Field (3.6s)
✔ [4079/4109] Built Mathlib.Algebra.Order.Ring.Opposite (2.9s)
✔ [4095/4109] Built Mathlib.Algebra.Order.Quantale (4.5s)
✔ [4096/4111] Built Mathlib.Algebra.Ring.Action.Field (2.9s)
✔ [4099/4115] Built Mathlib.Algebra.Order.Sub.Prod (2.7s)
✔ [4103/4118] Built Mathlib.Algebra.Order.Sum (2.4s)
✔ [4105/4137] Built Mathlib.Algebra.Order.Monoid.Lex (4.8s)
✔ [4125/4145] Built Mathlib.Algebra.Order.Sub.Unbundled.Hom (3.0s)
✔ [4130/4145] Built Mathlib.Data.List.GetD (3.3s)
✔ [4147/4210] Built Mathlib.Algebra.Regular.Pi (3.0s)
✔ [4157/4295] Built Mathlib.Algebra.Regular.Prod (2.9s)
✔ [4207/4388] Built Mathlib.Algebra.Regular.ULift (2.8s)
✔ [4383/4578] Built Mathlib.Logic.Function.Coequalizer (1.3s)
✔ [4455/4653] Built Mathlib.Algebra.Ring.Pointwise.Set (2.9s)
✔ [4527/4718] Built Mathlib.Topology.Sheaves.Init (2.6s)
✔ [4877/4941] Built Mathlib.Algebra.Ring.Ext (4.3s)
✔ [5069/5186] Built Mathlib.Order.SetIsMax (2.6s)
✔ [5078/5186] Built Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note (2.0s)
✔ [5100/5190] Built Mathlib.Algebra.Tropical.Basic (5.5s)
✔ [5103/5203] Built Mathlib.Order.Monotone.Extension (3.2s)
✔ [5106/5203] Built Mathlib.Order.CompleteLattice.Group (3.1s)
✔ [5182/5315] Built Mathlib.Data.Bundle (3.2s)
✔ [5617/5697] Built Mathlib.Order.Monotone.Union (2.9s)
✔ [5619/5700] Built Mathlib.Data.List.Triplewise (3.3s)
✔ [5621/5860] Built Mathlib.Tactic.DepRewrite (7.4s)
✔ [5874/5916] Built Mathlib.Data.PEquiv (4.4s)
✔ [5882/6014] Built Mathlib.Data.Int.Range (3.3s)
✔ [6032/6104] Built Mathlib.Order.Monotone.Odd (3.2s)
✔ [6043/6106] Built Mathlib.Tactic.MoveAdd (4.4s)
✔ [6056/6117] Built Mathlib.Data.TwoPointing (2.8s)
✔ [6073/6174] Built Mathlib.GroupTheory.EckmannHilton (2.5s)
✔ [6088/6181] Built Mathlib.Data.PFun (5.4s)
✔ [6096/6185] Built Mathlib.Combinatorics.SimpleGraph.Init (2.8s)
✔ [6108/6186] Built Mathlib.Combinatorics.Quiver.Subquiver (2.8s)
✔ [6110/6186] Built Mathlib.Combinatorics.Quiver.Path.Decomposition (3.3s)
✔ [6132/6200] Built Mathlib.Combinatorics.Quiver.Path.Weight (3.4s)
✔ [6215/6274] Built Mathlib.Algebra.Tropical.Lattice (9.3s)
✔ [6216/6274] Built Mathlib.Data.Nat.PSub (2.7s)
✔ [6220/6274] Built Mathlib.Data.Num.Basic (2.3s)
✔ [6261/6292] Built Mathlib.Combinatorics.Quiver.ConnectedComponent (2.6s)
✔ [6262/6292] Built Mathlib.Data.Nat.Size (3.1s)
✔ [6269/6294] Built Mathlib.Order.Booleanisation (4.9s)
✔ [6272/6297] Built Mathlib.Combinatorics.Quiver.Arborescence (2.9s)
✔ [6273/6297] Built Mathlib.Logic.Function.FiberPartition (2.3s)
✔ [6292/6312] Built Mathlib.Data.Array.Extract (1.4s)
✔ [6293/6328] Built Mathlib.Control.Lawful (1.0s)
✔ [6306/6330] Built Mathlib.Control.Traversable.Lemmas (2.4s)
✔ [6310/6355] Built Mathlib.Data.Nat.Upto (2.6s)
✔ [6311/6355] Built Mathlib.Data.Bool.AllAny (1.4s)
✔ [6335/6356] Built Mathlib.Control.Monad.Writer (2.6s)
✔ [6336/6356] Built Mathlib.Data.List.Lookmap (1.6s)
✔ [6337/6361] Built Mathlib.Data.Char (2.5s)
✔ [6346/6367] Built Mathlib.Data.Erased (2.7s)
✔ [6352/6381] Built Mathlib.Data.List.Indexes (1.4s)
✔ [6366/6399] Built Mathlib.Control.Traversable.Equiv (2.5s)
✔ [6386/6399] Built Mathlib.Data.Semiquot (3.3s)
✔ [6387/6401] Built Mathlib.Data.List.TakeWhile (2.6s)
✔ [6389/6414] Built Mathlib.Data.List.ModifyLast (1.6s)
✔ [6400/6447] Built Mathlib.Control.Fix (2.0s)
✔ [6434/6448] Built Mathlib.Data.Ordering.Lemmas (1.5s)
✔ [6435/6451] Built Mathlib.Data.Nat.Cast.Synonym (2.2s)
✔ [6437/6455] Built Mathlib.Control.Monad.Cont (3.0s)
✔ [6440/6455] Built Mathlib.Data.List.SplitLengths (2.6s)
✔ [6443/6457] Built Mathlib.Data.Set.Opposite (2.5s)
✔ [6445/6458] Built Mathlib.Data.FP.Basic (3.6s)
✔ [6446/6459] Built Mathlib.Data.Set.Pairwise.Chain (2.5s)
✔ [6447/6470] Built Mathlib.Data.PSigma.Order (3.7s)
✔ [6459/6473] Built Mathlib.Data.String.Lemmas (2.9s)
✔ [6460/6475] Built Mathlib.Data.Tree.Get (1.8s)
✔ [6461/6477] Built Mathlib.Data.Tree.RBMap (1.9s)
✔ [6463/6479] Built Mathlib.Deprecated.Aliases (1.6s)
✔ [6465/6482] Built Mathlib.Data.Sigma.Order (4.4s)
✔ [6683/6701] Built Mathlib.Lean.Thunk (1.5s)
✔ [6688/6701] Built Mathlib.Data.Ordmap.Ordnode (6.3s)
✔ [6691/6715] Built Mathlib.Data.Tree.Traversable (3.0s)
✔ [6699/6748] Built Mathlib.Deprecated.Sort (1.4s)
✔ [6729/6749] Built Mathlib.Deprecated.Order (2.3s)
✔ [6730/6750] Built Mathlib.Data.Sum.Lattice (5.5s)
✔ [6731/6750] Built Mathlib.Lean.CoreM (1.2s)
✔ [6732/6753] Built Mathlib.Order.SemiconjSup (2.7s)
✔ [6734/6754] Built Mathlib.Lean.Elab.Tactic.Basic (1.6s)
✔ [6735/6755] Built Mathlib.GroupTheory.GroupAction.Embedding (3.1s)
✔ [6738/6756] Built Mathlib.Lean.EnvExtension (3.3s)
✔ [6739/6757] Built Mathlib.GroupTheory.GroupAction.DomAct.ActionHom (4.7s)
✔ [6746/6762] Built Mathlib.Lean.Exception (2.7s)
✔ [6858/6870] Built Mathlib.Lean.Expr.ReplaceRec (3.1s)
✔ [6859/6871] Built Mathlib.Lean.Json (3.3s)
✔ [6862/7037] Built Mathlib.Lean.LocalContext (2.8s)
✔ [7249/7263] Built Mathlib.GroupTheory.GroupAction.Support (6.2s)
✔ [7250/7263] Built Mathlib.Lean.Message (2.5s)
✔ [7259/7269] Built Mathlib.Lean.Meta.DiscrTree (2.8s)
✔ [7261/7273] Built Mathlib.Lean.Expr (1.7s)
✔ [7264/7280] Built Mathlib.Logic.Equiv.Pairwise (2.6s)
✔ [7270/7283] Built Mathlib.Deprecated.Estimator (7.7s)
✔ [7274/7285] Built Mathlib.Logic.Equiv.Bool (3.2s)
✔ [7276/7287] Built Mathlib.Order.Bounded (3.9s)
✔ [7278/7289] Built Mathlib.Order.Bounds.Lattice (3.8s)
✔ [7280/7297] Built Mathlib.Order.Comparable (4.3s)
✔ [7281/7297] Built Mathlib.Order.Extension.Linear (3.9s)
✔ [7287/7298] Built Mathlib.Order.Interval.Set.SurjOn (3.0s)
✔ [7288/7304] Built Mathlib.Order.Concept (5.3s)
✔ [7294/7350] Built Mathlib.Order.Filter.Partial (5.3s)
✔ [7601/7653] Built Mathlib.Order.Heyting.Regular (6.3s)
✔ [7640/7664] Built Mathlib.Order.Lattice.Congruence (4.4s)
✔ [7643/7676] Built Mathlib.Order.Rel.GaloisConnection (3.7s)
✔ [7651/7681] Built Mathlib.Order.Set (3.2s)
✔ [7652/7682] Built Mathlib.Order.UpperLower.Relative (3.5s)
✔ [7653/7683] Built Mathlib.Order.ScottContinuity.Prod (5.2s)
✔ [7654/7687] Built Mathlib.Std.Data.HashMap (1.3s)
✔ [7655/7688] Built Mathlib.RingTheory.RingInvo (3.7s)
✔ [7656/7688] Built Mathlib.Order.Nucleus (7.1s)
✔ [7659/7692] Built Mathlib.Tactic.CC.Lemmas (1.0s)
✔ [7661/7693] Built Mathlib.Tactic.Relation.Symm (1.9s)
✔ [7662/7694] Built Mathlib.SetTheory.ZFC.PSet (4.6s)
✔ [7669/7696] Built Mathlib.Tactic.Change (1.0s)
✔ [7671/7696] Built Mathlib.Order.ScottContinuity.Complete (3.7s)
✔ [7672/7699] Built Mathlib.Tactic.Clean (1.6s)
✔ [7673/7701] Built Mathlib.SetTheory.PGame.Basic (6.6s)
✔ [7677/7702] Built Mathlib.Tactic.Cases (3.9s)
✔ [7680/7703] Built Mathlib.Tactic.Explode.Datatypes (1.2s)
✔ [7682/7704] Built Mathlib.SetTheory.Lists (7.6s)
✔ [7687/7704] Built Mathlib.Tactic.Eval (2.1s)
✔ [7690/7705] Built Mathlib.Tactic.Generalize (1.3s)
✔ [7692/7706] Built Mathlib.Tactic.Ext (2.4s)
✔ [7693/7708] Built Mathlib.Tactic.FindSyntax (2.1s)
✔ [7696/7710] Built Mathlib.Tactic.Explode.Pretty (1.7s)
✔ [7697/7710] Built Mathlib.Tactic.GeneralizeProofs (1.8s)
✔ [7698/7713] Built Mathlib.Tactic.DeriveCountable (5.7s)
✔ [7699/7713] Built Mathlib.Tactic.Linter.CommandRanges (1.6s)
✔ [7700/7713] Built Mathlib.Tactic.Linter.CommandStart (1.5s)
✔ [7701/7725] Built Mathlib.Tactic.Have (2.6s)
✔ [7716/7730] Built Mathlib.Tactic.Linter.TextBased.UnicodeLinter (1.4s)
✔ [7717/7731] Built Mathlib.Tactic.DeriveTraversable (6.7s)
✔ [7718/7731] Built Mathlib.Tactic.Polyrith (1.1s)
✔ [7719/7731] Built Mathlib.Tactic.Explode (2.0s)
✔ [7720/7733] Built Mathlib.Tactic.CC.Datatypes (10s)
✔ [7721/7733] Built Mathlib.Tactic.Linter.ValidatePRTitle (2.8s)
✔ [7722/7734] Built Mathlib.Tactic.Linter.FindDeprecations (2.0s)
✔ [7723/7736] Built Mathlib.Tactic.Propose (1.5s)
✔ [7724/7737] Built Mathlib.Tactic.ReduceModChar.Ext (1.4s)
✔ [7726/7749] Built Mathlib.Tactic.Recall (2.4s)
✔ [7737/7751] Built Mathlib.Tactic.Replace (1.7s)
✔ [7739/7752] Built Mathlib.Tactic.RewriteSearch (1.0s)
✔ [7740/7768] Built Mathlib.Tactic.ProdAssoc (4.6s)
✔ [7882/7895] Built Mathlib.Tactic.WithoutCDot (2.2s)
✔ [7883/7896] Built Mathlib.Tactic.Linter.TextBased (5.0s)
✔ [7884/7898] Built Mathlib.Tactic.ITauto (9.5s)
✔ [7885/7898] Built Mathlib.Testing.Plausible.Testable (2.6s)
✔ [7886/7899] Built Mathlib.Util.AssertExistsExt (1.4s)
✔ [7887/7900] Built Mathlib.Util.AliasIn (1.0s)
✔ [7888/7900] Built Mathlib.Testing.Plausible.Sampleable (3.7s)
✔ [7890/7902] Built Mathlib.Util.AssertNoSorry (1.5s)
✔ [7891/7902] Built Mathlib.Util.GetAllModules (1.3s)
✔ [7892/7902] Built Mathlib.Util.FormatTable (1.0s)
✔ [7893/7902] Built Mathlib.Util.LongNames (1.6s)
✔ [7894/7902] Built Mathlib.Util.SleepHeartbeats (1.1s)
✔ [7895/7902] Built Mathlib.Tactic.Sat.FromLRAT (6.0s)
✔ [7896/7902] Built Mathlib.Util.Simp (1.0s)
✔ [7897/7902] Built Mathlib.Util.Export (3.1s)
✔ [7898/7902] Built Mathlib.Tactic.CC.MkProof (9.5s)
✔ [7899/7902] Built Mathlib.Tactic.CC.Addition (5.9s)
✔ [7900/7902] Built Mathlib.Tactic.CC (1.8s)
Some required targets logged failures:
- proofwidgets/widgetJsAll
Failed to build module dependencies.