ruc-ai4math/mathlib_handler_benchmark_410

1{2    ".lake/packages/aesop/Aesop/Constants.lean": [],3    ".lake/packages/aesop/Aesop/Percent.lean": [],4    "Cache/Main.lean": [],5    ".lake/packages/aesop/Aesop/Nanos.lean": [],6    "Cache/Hashing.lean": [],7    ".lake/packages/aesop/Aesop/Tree.lean": [],8    "Cache/Requests.lean": [],9    ".lake/packages/aesop/Aesop/RuleTac.lean": [],10    ".lake/packages/aesop/Aesop/Tree/UnsafeQueue.lean": [],11    ".lake/packages/aesop/Aesop/RuleTac/Apply.lean": [],12    ".lake/packages/aesop/Aesop/ElabM.lean": [],13    ".lake/packages/aesop/Aesop/Index/Basic.lean": [],14    ".lake/packages/aesop/Aesop/RuleTac/Preprocess.lean": [],15    ".lake/packages/aesop/Aesop/RuleTac/Tactic.lean": [],16    ".lake/packages/aesop/Aesop.lean": [],17    ".lake/packages/aesop/Aesop/Tree/TreeM.lean": [],18    ".lake/packages/aesop/Aesop/Exception.lean": [],19    ".lake/packages/aesop/Aesop/RuleTac/Forward/Basic.lean": [],20    ".lake/packages/aesop/Aesop/Tree/RunMetaM.lean": [],21    ".lake/packages/aesop/Aesop/RuleTac/Cases.lean": [],22    ".lake/packages/aesop/Aesop/RuleTac/Basic.lean": [],23    ".lake/packages/aesop/Aesop/Tree/Free.lean": [],24    ".lake/packages/aesop/Aesop/RuleTac/ElabRuleTerm.lean": [],25    ".lake/packages/aesop/Aesop/Tree/Traversal.lean": [],26    ".lake/packages/aesop/Aesop/Tree/ExtractScript.lean": [],27    ".lake/packages/aesop/Aesop/RuleTac/Forward.lean": [],28    ".lake/packages/aesop/Aesop/Tree/Tracing.lean": [],29    ".lake/packages/aesop/Aesop/Tree/ExtractProof.lean": [],30    "Cache/IO.lean": [],31    ".lake/packages/aesop/Aesop/Tree/AddRapp.lean": [],32    ".lake/packages/aesop/Aesop/Tree/Data.lean": [],33    ".lake/packages/aesop/Aesop/Tree/Check.lean": [],34    ".lake/packages/aesop/Aesop/BuiltinRules/ApplyHyps.lean": [],35    ".lake/packages/aesop/Aesop/Tree/State.lean": [],36    ".lake/packages/aesop/Aesop/BuiltinRules/Intros.lean": [],37    ".lake/packages/aesop/Aesop/BuiltinRules/Ext.lean": [],38    ".lake/packages/aesop/Aesop/BuiltinRules/Assumption.lean": [],39    ".lake/packages/aesop/Aesop/Script/UScript.lean": [],40    ".lake/packages/aesop/Aesop/Script/Main.lean": [],41    ".lake/packages/aesop/Aesop/Script/Tactic.lean": [],42    ".lake/packages/aesop/Aesop/Main.lean": [],43    ".lake/packages/aesop/Aesop/Script/SScript.lean": [],44    ".lake/packages/aesop/Aesop/BuiltinRules/Split.lean": [],45    ".lake/packages/aesop/Aesop/Script/OptimizeSyntax.lean": [],46    ".lake/packages/aesop/Aesop/Builder.lean": [],47    ".lake/packages/aesop/Aesop/Script/Check.lean": [],48    ".lake/packages/aesop/Aesop/Script/StructureStatic.lean": [],49    ".lake/packages/aesop/Aesop/Script/Util.lean": [],50    ".lake/packages/aesop/Aesop/BuiltinRules/Subst.lean": [],51    ".lake/packages/aesop/Aesop/Script/GoalWithMVars.lean": [],52    ".lake/packages/aesop/Aesop/Script/ScriptM.lean": [],53    ".lake/packages/aesop/Aesop/Script/TacticState.lean": [],54    ".lake/packages/aesop/Aesop/BuiltinRules/DestructProducts.lean": [],55    ".lake/packages/aesop/Aesop/Stats/Basic.lean": [],56    ".lake/packages/aesop/Aesop/Script/CtorNames.lean": [],57    ".lake/packages/aesop/Aesop/Rule.lean": [],58    ".lake/packages/aesop/Aesop/Script/UScriptToSScript.lean": [],59    ".lake/packages/aesop/Aesop/Script/Step.lean": [60        061    ],62    ".lake/packages/aesop/Aesop/Stats/Report.lean": [],63    ".lake/packages/aesop/Aesop/Stats/Extension.lean": [],64    ".lake/packages/aesop/Aesop/Options/Internal.lean": [],65    ".lake/packages/aesop/Aesop/Script/StructureDynamic.lean": [],66    ".lake/packages/aesop/Aesop/Script/SpecificTactics.lean": [],67    ".lake/packages/aesop/Aesop/Options/Public.lean": [],68    ".lake/packages/aesop/Aesop/Builder/Unfold.lean": [],69    ".lake/packages/aesop/Aesop/Builder/Basic.lean": [],70    ".lake/packages/aesop/Aesop/Builder/Cases.lean": [],71    ".lake/packages/aesop/Aesop/Builder/Constructors.lean": [],72    ".lake/packages/aesop/Aesop/Builder/Apply.lean": [],73    ".lake/packages/aesop/Aesop/Index.lean": [],74    ".lake/packages/aesop/Aesop/Builder/NormSimp.lean": [],75    ".lake/packages/aesop/Aesop/Frontend.lean": [],76    ".lake/packages/aesop/Aesop/Builder/Tactic.lean": [],77    ".lake/packages/aesop/Aesop/Builder/Default.lean": [],78    ".lake/packages/aesop/Aesop/BuiltinRules.lean": [79        1,80        2,81        3,82        483    ],84    ".lake/packages/aesop/Aesop/Search/Queue/Class.lean": [],85    ".lake/packages/aesop/Aesop/Builder/Forward.lean": [],86    ".lake/packages/aesop/Aesop/Search/Expansion/Simp.lean": [],87    ".lake/packages/aesop/Aesop/Search/ExpandSafePrefix.lean": [],88    ".lake/packages/aesop/Aesop/Saturate.lean": [],89    ".lake/packages/aesop/Aesop/Search/RuleSelection.lean": [],90    ".lake/packages/aesop/Aesop/Frontend/Basic.lean": [],91    ".lake/packages/aesop/Aesop/Search/Expansion/Basic.lean": [],92    ".lake/packages/aesop/Aesop/Frontend/Extension/Init.lean": [],93    ".lake/packages/aesop/Aesop/RulePattern.lean": [],94    ".lake/packages/aesop/Aesop/Search/Queue.lean": [],95    ".lake/packages/aesop/Aesop/Search/SearchM.lean": [],96    ".lake/packages/aesop/Aesop/Frontend/Attribute.lean": [],97    ".lake/packages/aesop/Aesop/Tracing.lean": [],98    ".lake/packages/aesop/Aesop/Search/Expansion/Norm.lean": [],99    ".lake/packages/aesop/Aesop/Frontend/Command.lean": [],100    ".lake/packages/aesop/Aesop/Frontend/Saturate.lean": [],101    ".lake/packages/aesop/Aesop/Frontend/Tactic.lean": [],102    ".lake/packages/aesop/Aesop/Search/Expansion.lean": [],103    ".lake/packages/aesop/Aesop/Util/Tactic.lean": [],104    ".lake/packages/aesop/Aesop/Util/UnorderedArraySet.lean": [],105    ".lake/packages/aesop/Aesop/Frontend/Extension.lean": [],106    ".lake/packages/aesop/Aesop/Check.lean": [],107    ".lake/packages/batteries/Batteries/Control/ForInStep/Basic.lean": [],108    ".lake/packages/batteries/Batteries/Control/ForInStep/Lemmas.lean": [109        5,110        6,111        7,112        8,113        9,114        10,115        11,116        12,117        13,118        14,119        15120    ],121    ".lake/packages/aesop/Aesop/Util/Tactic/Ext.lean": [],122    ".lake/packages/aesop/Aesop/Rule/Basic.lean": [],123    ".lake/packages/aesop/Aesop/RuleSet/Filter.lean": [],124    ".lake/packages/aesop/Aesop/Options.lean": [],125    ".lake/packages/batteries/Batteries/CodeAction.lean": [],126    ".lake/packages/aesop/Aesop/Frontend/RuleExpr.lean": [],127    ".lake/packages/aesop/Aesop/RuleSet/Name.lean": [],128    ".lake/packages/aesop/Aesop/Util/Tactic/Unfold.lean": [],129    ".lake/packages/aesop/Aesop/Rule/Name.lean": [],130    ".lake/packages/aesop/Aesop/Util/UnionFind.lean": [],131    ".lake/packages/batteries/Batteries/Logic.lean": [132        16,133        17,134        18,135        19,136        20,137        21,138        22,139        23,140        24,141        25,142        26,143        27,144        28,145        29,146        30,147        31,148        32,149        33,150        34,151        35,152        36,153        37,154        38,155        39,156        40,157        41,158        42159    ],160    ".lake/packages/aesop/Aesop/RuleSet/Member.lean": [],161    ".lake/packages/batteries/Batteries/Control/Nondet/Basic.lean": [],162    ".lake/packages/batteries/Batteries/WF.lean": [163        43,164        44,165        45,166        46,167        47,168        48169    ],170    ".lake/packages/aesop/Aesop/Util/Basic.lean": [171        49172    ],173    ".lake/packages/aesop/Aesop/Util/EqualUpToIds.lean": [],174    ".lake/packages/batteries/Batteries/Linter/UnnecessarySeqFocus.lean": [],175    ".lake/packages/batteries/Batteries/Classes/BEq.lean": [176        50,177        51178    ],179    ".lake/packages/aesop/Aesop/RuleSet.lean": [180        52,181        53182    ],183    ".lake/packages/aesop/Aesop/Search/Main.lean": [],184    ".lake/packages/batteries/Batteries/Linter/UnreachableTactic.lean": [],185    ".lake/packages/batteries/Batteries/Classes/RatCast.lean": [],186    ".lake/packages/batteries/Batteries/Tactic/Basic.lean": [],187    ".lake/packages/batteries/Batteries/Tactic/Lint/Basic.lean": [],188    ".lake/packages/batteries/Batteries/Classes/SatisfiesM.lean": [189        54,190        55,191        56,192        57,193        58,194        59,195        60,196        61,197        62,198        63,199        64,200        65,201        66,202        67,203        68,204        69,205        70,206        71,207        72,208        73,209        74,210        75,211        76212    ],213    ".lake/packages/batteries/Batteries/Tactic/Lint/TypeClass.lean": [],214    ".lake/packages/batteries/Batteries/Tactic/Alias.lean": [],215    ".lake/packages/batteries/Batteries/Tactic/Lint/Simp.lean": [],216    ".lake/packages/batteries/Batteries/Tactic/Exact.lean": [],217    ".lake/packages/batteries/Batteries/Classes/Order.lean": [218        77,219        78,220        79,221        80,222        81,223        82,224        83,225        84,226        85,227        86,228        87,229        88,230        89,231        90,232        91,233        92,234        93,235        94,236        95,237        96,238        97,239        98,240        99,241        100,242        101,243        102,244        103,245        104,246        105,247        106,248        107,249        108,250        109,251        110,252        111,253        112,254        113,255        114,256        115,257        116,258        117,259        118,260        119,261        120,262        121,263        122,264        123,265        124,266        125267    ],268    ".lake/packages/batteries/Batteries/Tactic/Congr.lean": [],269    ".lake/packages/batteries/Batteries/Tactic/Unreachable.lean": [],270    ".lake/packages/batteries/Batteries/Tactic/Where.lean": [],271    ".lake/packages/batteries/Batteries/Tactic/Lint/Frontend.lean": [],272    ".lake/packages/batteries/Batteries/Tactic/Lint.lean": [],273    ".lake/packages/batteries/Batteries/Tactic/SeqFocus.lean": [],274    ".lake/packages/batteries/Batteries/Tactic/Lint/Misc.lean": [],275    ".lake/packages/batteries/Batteries/Linter.lean": [],276    ".lake/packages/batteries/Batteries/Tactic/Classical.lean": [],277    ".lake/packages/batteries/Batteries/Tactic/PermuteGoals.lean": [],278    ".lake/packages/batteries/Batteries/Tactic/Init.lean": [],279    ".lake/packages/batteries/Batteries/Util/ProofWanted.lean": [],280    ".lake/packages/batteries/Batteries/Lean/Except.lean": [],281    ".lake/packages/batteries/Batteries/CodeAction/Attr.lean": [],282    ".lake/packages/batteries/Batteries/Tactic/OpenPrivate.lean": [],283    ".lake/packages/batteries/Batteries/Util/Cache.lean": [],284    ".lake/packages/batteries/Batteries/Tactic/SqueezeScope.lean": [],285    ".lake/packages/batteries/Batteries/Lean/Syntax.lean": [],286    ".lake/packages/batteries/Batteries/CodeAction/Deprecated.lean": [],287    ".lake/packages/batteries/Batteries/Util/LibraryNote.lean": [],288    ".lake/packages/batteries/Batteries/CodeAction/Basic.lean": [],289    ".lake/packages/batteries/Batteries/Util/ExtendedBinder.lean": [],290    ".lake/packages/batteries/Batteries/Lean/MonadBacktrack.lean": [],291    ".lake/packages/batteries/Batteries/Lean/AttributeExtra.lean": [],292    ".lake/packages/batteries/Batteries/CodeAction/Misc.lean": [],293    ".lake/packages/batteries/Batteries/Lean/TagAttribute.lean": [],294    ".lake/packages/batteries/Batteries/Lean/PersistentHashSet.lean": [],295    ".lake/packages/batteries/Batteries/Lean/NameMapAttribute.lean": [],296    ".lake/packages/batteries/Batteries/Lean/HashSet.lean": [],297    ".lake/packages/batteries/Batteries/Lean/NameMap.lean": [],298    ".lake/packages/batteries/Batteries/Lean/PersistentHashMap.lean": [],299    ".lake/packages/batteries/Batteries/Lean/SMap.lean": [],300    ".lake/packages/batteries/Batteries/Lean/Position.lean": [],301    ".lake/packages/batteries/Batteries/Lean/Expr.lean": [],302    ".lake/packages/batteries/Batteries/Lean/Meta/Basic.lean": [],303    ".lake/packages/batteries/Batteries/Lean/Meta/Clear.lean": [],304    ".lake/packages/batteries/Batteries/Lean/Meta/UnusedNames.lean": [],305    ".lake/packages/batteries/Batteries/Lean/Meta/InstantiateMVars.lean": [],306    ".lake/packages/batteries/Batteries/Lean/Meta/DiscrTree.lean": [],307    ".lake/packages/batteries/Batteries/Lean/Meta/Expr.lean": [],308    ".lake/packages/batteries/Batteries/Lean/Meta/Inaccessible.lean": [],309    ".lake/packages/batteries/Batteries/Lean/Float.lean": [],310    ".lake/packages/batteries/Batteries/Data/MLList/Heartbeats.lean": [],311    ".lake/packages/batteries/Batteries/Data/Sum/Basic.lean": [312        126,313        127,314        128,315        129,316        130,317        131,318        132,319        133,320        134,321        135,322        136,323        137,324        138,325        139,326        140,327        141,328        142,329        143,330        144,331        145,332        146,333        147,334        148335    ],336    ".lake/packages/batteries/Batteries/Lean/Meta/SavedState.lean": [],337    ".lake/packages/batteries/Batteries/Lean/Meta/AssertHypotheses.lean": [],338    ".lake/packages/batteries/Batteries/Data/String.lean": [],339    ".lake/packages/batteries/Batteries/Data/List/Init/Lemmas.lean": [],340    ".lake/packages/batteries/Batteries/Data/Int/DivMod.lean": [],341    ".lake/packages/batteries/Batteries/Data/Int/Order.lean": [],342    ".lake/packages/batteries/Batteries/Data/MLList/Basic.lean": [],343    ".lake/packages/batteries/Batteries/Data/List/Init/Attach.lean": [344        149,345        150346    ],347    ".lake/packages/batteries/Batteries/Data/List/EraseIdx.lean": [348        151,349        152,350        153,351        154,352        155,353        156,354        157,355        158,356        159,357        160,358        161,359        162360    ],361    ".lake/packages/batteries/Batteries/Data/Sum/Lemmas.lean": [362        163,363        164,364        165,365        166,366        167,367        168,368        169,369        170,370        171,371        172,372        173,373        174,374        175,375        176,376        177,377        178,378        179,379        180,380        181,381        182,382        183,383        184,384        185,385        186,386        187,387        188,388        189,389        190,390        191,391        192,392        193,393        194,394        195,395        196,396        197,397        198,398        199,399        200,400        201,401        202,402        203,403        204,404        205,405        206,406        207,407        208,408        209,409        210,410        211,411        212,412        213,413        214,414        215,415        216,416        217,417        218,418        219,419        220,420        221,421        222,422        223423    ],424    ".lake/packages/batteries/Batteries/Data/Fin/Basic.lean": [],425    ".lake/packages/batteries/Batteries/Data/DList.lean": [426        224427    ],428    ".lake/packages/batteries/Batteries/Data/Nat/Basic.lean": [],429    ".lake/packages/batteries/Batteries/Data/UInt.lean": [430        225,431        226,432        227,433        228,434        229,435        230,436        231,437        232,438        233,439        234,440        235,441        236,442        237,443        238,444        239,445        240,446        241,447        242,448        243,449        244,450        245,451        246,452        247,453        248,454        249,455        250,456        251,457        252,458        253,459        254,460        255,461        256,462        257,463        258,464        259,465        260,466        261,467        262,468        263,469        264,470        265,471        266,472        267,473        268,474        269,475        270,476        271,477        272,478        273,479        274,480        275,481        276,482        277,483        278,484        279,485        280,486        281,487        282,488        283,489        284,490        285,491        286,492        287,493        288,494        289,495        290,496        291,497        292,498        293,499        294,500        295,501        296,502        297,503        298,504        299,505        300,506        301,507        302,508        303,509        304,510        305,511        306,512        307,513        308,514        309,515        310,516        311,517        312,518        313,519        314,520        315,521        316522    ],523    ".lake/packages/batteries/Batteries/Data/Array/Init/Lemmas.lean": [],524    ".lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean": [525        317,526        318,527        319,528        320,529        321,530        322,531        323,532        324,533        325,534        326,535        327,536        328,537        329,538        330,539        331,540        332,541        333,542        334,543        335,544        336,545        337,546        338,547        339,548        340,549        341,550        342551    ],552    ".lake/packages/batteries/Batteries/Data/Array/Match.lean": [553        343554    ],555    ".lake/packages/batteries/Batteries/Data/Array/Basic.lean": [],556    ".lake/packages/batteries/Batteries/Data/List/Count.lean": [557        344,558        345,559        346,560        347,561        348,562        349,563        350,564        351,565        352,566        353,567        354,568        355,569        356,570        357,571        358,572        359,573        360,574        361,575        362,576        363,577        364,578        365,579        366,580        367,581        368,582        369,583        370,584        371,585        372,586        373,587        374,588        375,589        376,590        377,591        378,592        379,593        380,594        381,595        382,596        383,597        384,598        385,599        386,600        387,601        388,602        389,603        390,604        391,605        392606    ],607    ".lake/packages/batteries/Batteries/Data/Nat/Gcd.lean": [608        393,609        394,610        395,611        396,612        397,613        398,614        399,615        400,616        401,617        402,618        403,619        404,620        405,621        406,622        407,623        408,624        409,625        410,626        411,627        412,628        413,629        414,630        415,631        416,632        417,633        418,634        419,635        420,636        421,637        422,638        423,639        424,640        425,641        426,642        427,643        428,644        429,645        430,646        431,647        432,648        433,649        434,650        435651    ],652    ".lake/packages/batteries/Batteries/Data/String/Matcher.lean": [],653    ".lake/packages/batteries/Batteries/Data/Thunk.lean": [654        436655    ],656    ".lake/packages/batteries/Batteries/Data/String/Basic.lean": [657        437658    ],659    ".lake/packages/batteries/Batteries/Data/HashMap/Basic.lean": [660        438,661        439,662        440,663        441,664        442665    ],666    ".lake/packages/batteries/Batteries/Data/Char.lean": [667        443,668        444,669        445,670        446671    ],672    ".lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean": [673        447,674        448,675        449,676        450,677        451,678        452,679        453,680        454,681        455,682        456,683        457,684        458,685        459,686        460,687        461,688        462,689        463,690        464,691        465,692        466,693        467,694        468,695        469,696        470,697        471,698        472,699        473,700        474,701        475702    ],703    ".lake/packages/batteries/Batteries/Data/RBMap/Basic.lean": [704        476,705        477,706        478,707        479,708        480,709        481,710        482711    ],712    ".lake/packages/batteries/Batteries/Data/Array/Merge.lean": [],713    ".lake/packages/batteries/Batteries/Data/RBMap/Alter.lean": [714        483,715        484,716        485,717        486,718        487,719        488,720        489,721        490,722        491,723        492,724        493,725        494,726        495,727        496,728        497,729        498,730        499,731        500,732        501,733        502,734        503,735        504,736        505,737        506,738        507739    ],740    ".lake/packages/proofwidgets/ProofWidgets/Presentation/Expr.lean": [],741    ".lake/packages/proofwidgets/ProofWidgets/Component/Basic.lean": [],742    ".lake/packages/batteries/Batteries/Data/List/Pairwise.lean": [743        508,744        509,745        510,746        511,747        512,748        513,749        514,750        515,751        516,752        517,753        518,754        519,755        520,756        521,757        522,758        523,759        524,760        525,761        526,762        527,763        528,764        529,765        530,766        531,767        532,768        533,769        534,770        535,771        536,772        537,773        538,774        539,775        540,776        541,777        542,778        543,779        544,780        545,781        546,782        547,783        548,784        549,785        550786    ],787    ".lake/packages/batteries/Batteries/Data/AssocList.lean": [788        551,789        552,790        553,791        554,792        555,793        556,794        557,795        558,796        559,797        560,798        561,799        562,800        563,801        564,802        565,803        566,804        567,805        568,806        569,807        570,808        571,809        572,810        573,811        574,812        575,813        576,814        577,815        578,816        579,817        580,818        581,819        582,820        583,821        584,822        585823    ],824    ".lake/packages/proofwidgets/ProofWidgets/Component/Recharts.lean": [],825    ".lake/packages/batteries/Batteries/Data/Rat/Basic.lean": [826        586,827        587,828        588,829        589,830        590,831        591,832        592833    ],834    ".lake/packages/batteries/Batteries/Data/Array/Lemmas.lean": [835        593,836        594,837        595,838        596,839        597,840        598,841        599,842        600,843        601,844        602,845        603,846        604,847        605,848        606,849        607850    ],851    ".lake/packages/proofwidgets/ProofWidgets/Component/Panel/GoalTypePanel.lean": [],852    ".lake/packages/proofwidgets/ProofWidgets/Component/HtmlDisplay.lean": [],853    ".lake/packages/proofwidgets/ProofWidgets/Component/Panel/Basic.lean": [],854    ".lake/packages/proofwidgets/ProofWidgets/Component/Panel/SelectionPanel.lean": [],855    ".lake/packages/proofwidgets/ProofWidgets/Component/InteractiveSvg.lean": [],856    ".lake/packages/proofwidgets/ProofWidgets/Component/PenroseDiagram.lean": [],857    ".lake/packages/proofwidgets/ProofWidgets/Component/OfRpcMethod.lean": [],858    ".lake/packages/proofwidgets/ProofWidgets/Component/FilterDetails.lean": [],859    ".lake/packages/batteries/Batteries/Data/LazyList.lean": [860        608,861        609,862        610,863        611,864        612,865        613866    ],867    ".lake/packages/proofwidgets/ProofWidgets/Component/MakeEditLink.lean": [],868    ".lake/packages/proofwidgets/ProofWidgets/Demos/Plot.lean": [],869    ".lake/packages/proofwidgets/ProofWidgets/Demos/LazyComputation.lean": [],870    ".lake/packages/proofwidgets/ProofWidgets/Demos/InteractiveSvg.lean": [],871    ".lake/packages/proofwidgets/ProofWidgets/Demos/Venn.lean": [872        614873    ],874    ".lake/packages/proofwidgets/ProofWidgets/Demos/ExprPresentation.lean": [],875    ".lake/packages/proofwidgets/ProofWidgets/Demos/Dynkin.lean": [],876    ".lake/packages/batteries/Batteries/Data/Array/Monadic.lean": [877        615,878        616,879        617,880        618,881        619,882        620,883        621,884        622,885        623,886        624,887        625,888        626,889        627890    ],891    ".lake/packages/proofwidgets/ProofWidgets/Demos/Jsx.lean": [],892    ".lake/packages/proofwidgets/ProofWidgets/Demos/Macro.lean": [],893    ".lake/packages/proofwidgets/ProofWidgets/Compat.lean": [],894    ".lake/packages/batteries/Batteries/Data/List/Basic.lean": [895        628,896        629,897        630,898        631,899        632,900        633,901        634,902        635,903        636,904        637,905        638,906        639,907        640,908        641,909        642,910        643,911        644,912        645,913        646,914        647,915        648,916        649,917        650,918        651,919        652,920        653,921        654,922        655,923        656,924        657,925        658,926        659,927        660,928        661,929        662,930        663,931        664,932        665,933        666,934        667,935        668,936        669,937        670,938        671,939        672,940        673,941        674,942        675943    ],944    ".lake/packages/proofwidgets/ProofWidgets/Demos/Rubiks.lean": [],945    ".lake/packages/proofwidgets/ProofWidgets/Util.lean": [],946    ".lake/packages/proofwidgets/ProofWidgets/Demos/SelectInsertConv.lean": [],947    ".lake/packages/proofwidgets/ProofWidgets/Cancellable.lean": [],948    ".lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean": [949        676,950        677,951        678,952        679,953        680,954        681,955        682,956        683,957        684,958        685,959        686,960        687,961        688,962        689,963        690,964        691,965        692,966        693,967        694,968        695,969        696,970        697,971        698,972        699,973        700,974        701,975        702,976        703,977        704,978        705,979        706,980        707,981        708,982        709,983        710,984        711,985        712,986        713,987        714,988        715,989        716,990        717,991        718,992        719,993        720,994        721,995        722,996        723,997        724,998        725,999        726,1000        727,1001        728,1002        729,1003        730,1004        731,1005        732,1006        733,1007        734,1008        735,1009        736,1010        737,1011        738,1012        739,1013        740,1014        741,1015        742,1016        743,1017        744,1018        745,1019        746,1020        747,1021        748,1022        749,1023        750,1024        751,1025        752,1026        753,1027        754,1028        755,1029        756,1030        757,1031        758,1032        759,1033        760,1034        7611035    ],1036    ".lake/packages/proofwidgets/ProofWidgets/Demos/Svg.lean": [],1037    ".lake/packages/proofwidgets/ProofWidgets/Demos/Conv.lean": [],1038    ".lake/packages/proofwidgets/ProofWidgets.lean": [],1039    ".lake/packages/importGraph/ImportGraph/RequiredModules.lean": [],1040    ".lake/packages/batteries/Batteries/Data/List/Perm.lean": [1041        762,1042        763,1043        764,1044        765,1045        766,1046        767,1047        768,1048        769,1049        770,1050        771,1051        772,1052        773,1053        774,1054        775,1055        776,1056        777,1057        778,1058        779,1059        780,1060        781,1061        782,1062        783,1063        784,1064        785,1065        786,1066        787,1067        788,1068        789,1069        790,1070        791,1071        792,1072        793,1073        794,1074        795,1075        796,1076        797,1077        798,1078        799,1079        800,1080        801,1081        802,1082        803,1083        804,1084        805,1085        806,1086        807,1087        808,1088        809,1089        810,1090        811,1091        812,1092        813,1093        814,1094        815,1095        816,1096        817,1097        818,1098        819,1099        820,1100        821,1101        822,1102        823,1103        824,1104        825,1105        826,1106        827,1107        828,1108        829,1109        830,1110        831,1111        832,1112        833,1113        834,1114        835,1115        836,1116        837,1117        838,1118        839,1119        840,1120        841,1121        842,1122        843,1123        844,1124        845,1125        846,1126        847,1127        848,1128        849,1129        850,1130        851,1131        852,1132        853,1133        854,1134        855,1135        856,1136        857,1137        858,1138        859,1139        860,1140        861,1141        862,1142        863,1143        864,1144        865,1145        866,1146        867,1147        868,1148        869,1149        870,1150        871,1151        872,1152        8731153    ],1154    ".lake/packages/proofwidgets/ProofWidgets/Demos/Euclidean.lean": [1155        874,1156        875,1157        876,1158        877,1159        878,1160        879,1161        880,1162        8811163    ],1164    ".lake/packages/proofwidgets/ProofWidgets/Data/Svg.lean": [],1165    ".lake/packages/importGraph/ImportGraph/Imports.lean": [],1166    ".lake/packages/proofwidgets/ProofWidgets/Demos/RbTree.lean": [],1167    ".lake/packages/Qq/Qq.lean": [],1168    ".lake/packages/Qq/Qq/Typ.lean": [],1169    ".lake/packages/Qq/Qq/SortLocalDecls.lean": [],1170    ".lake/packages/lean4/src/lean/Init.lean": [],1171    ".lake/packages/lean4/src/lean/Init/Omega.lean": [],1172    ".lake/packages/Qq/Qq/ForLean/Do.lean": [],1173    ".lake/packages/Qq/Qq/MetaM.lean": [],1174    ".lake/packages/Qq/Qq/ForLean/ToExpr.lean": [],1175    ".lake/packages/proofwidgets/ProofWidgets/Data/Html.lean": [],1176    ".lake/packages/Qq/Qq/Delab.lean": [],1177    ".lake/packages/lean4/src/lean/Init/Control/Basic.lean": [],1178    ".lake/packages/lean4/src/lean/Init/Control/Except.lean": [1179        8821180    ],1181    ".lake/packages/lean4/src/lean/Init/Control/StateCps.lean": [1182        883,1183        884,1184        885,1185        886,1186        887,1187        888,1188        889,1189        890,1190        891,1191        892,1192        893,1193        894,1194        8951195    ],1196    ".lake/packages/lean4/src/lean/Init/Control/Id.lean": [],1197    ".lake/packages/Qq/Qq/ForLean/ReduceEval.lean": [],1198    ".lake/packages/lean4/src/lean/Init/Control/Reader.lean": [],1199    ".lake/packages/Qq/Qq/AssertInstancesCommute.lean": [],1200    ".lake/packages/lean4/src/lean/Init/Control/EState.lean": [],

Showing the first 1,200 of 159687 lines. Download the file for the rest.