timings=KeyMap[StringDrop[#,-5]&,Association["timings"/.Import["https://mathlib-bench.limperg.de/commit/10a620163757cd2cf745db99c686e9721a1d0d3b/json","JSON"]]];

dir="~/projects/lean/mathlib-2/src/";

takeUntilSecondBlank[L_]:=Module[{i=0},TakeWhile[L,If[#=="",(i+=1)<2,True]&]]

imports=Association[{#->DeleteCases[Flatten[StringCases[takeUntilSecondBlank[Import[dir<>#<>".lean","Lines"]],"import "~~f___:>StringReplace[f,"."->"/"]]],#]}&/@(StringDrop[StringDrop[#,StringLength[dir]],-5]&/@FileNames["*.lean",dir,10])];

longPole[S_]:=longPole[S]=Module[{t,i,p},
t=Lookup[timings,S,0];
i=Lookup[imports,S,{}];
p=SortBy[{#,longPole[#]}&/@i,#[[2,1]]&];
If[Length[p]==0,{t,{S}},{t+p[[-1,2,1]],{S}~Join~p[[-1,2,2]]}]]

results=Association[SortBy[#->longPole[#]&/@Keys[imports],-#[[2,1]]&]];

{#,timings[#]}&/@Normal[results][[1,2,2]]//TableForm

g=Graph[Cases[Normal[results],(a_->{_,{_,b_,___}}):>a\[UndirectedEdge] b]];

h=Subgraph[g,ConnectedComponents[g][[1]],VertexLabels->MapIndexed[#->Placed[{#},{Tooltip}]&,VertexList[g]],GraphLayout->{"LayeredEmbedding","RootVertex"->"tactic/fix_reflect_string"}]