A list of suggested lemmata based on set.mm analysis. First column is score, second is the number of essential hyps, third is the proof skeleton.

lemmata_suggestions_hyps

791	1	["fvex","eqeltri"]
515	3	["rspcev","syl2anc"]
363	4	["syl2anc","mpbird"]
348	3	["syl","mpbird"]
341	1	["hllat","syl"]
330	5	["anbi12d","rspcev","syl12anc"]
315	4	["syl2anc","mpbid"]
306	1	["ffn","syl"]
304	1	["frn","syl"]
286	1	["fdm","syl"]
282	1	["fvex","eqeltri","a1i"]
274	3	["syl","mpbid"]
268	3	["eqeq2d","rspcev","syl2anc"]
268	2	["syl","adantr"]
247	1	["ne0i","syl"]
244	2	["oveq2d","eqtrd"]
242	3	["ralbidv","rspcev","syl2anc"]
234	2	["eqeltri","a1i"]
234	5	["syl3anc","mpbid"]
230	2	["anbi12d","rspcev"]
229	3	["syl","eqtrd"]
223	1	["eqid","fmptd"]
223	0	["oveq1","fveq2d"]
217	2	["jca","ex"]
172	1	["fvex","eqeltri","mptex"]
162	2	["breq2","ralbidv","rspcev","syl2anc"]
140	0	["breq2","ralbidv","rspcev"]
138	3	["fvex","eqeltri","mptex","fvmpt"]
136	9	["latjle12","syl13anc","mpbi2and"]
130	2	["fdm","syl","syl5sseq"]
124	3	["eqeq1d","rspcev","syl2anc"]
124	2	["restid","ax-mp","eqcomi"]
120	4	["fvex","eqeltri","mptex","fvmpt","syl"]
120	0	["2re","2pos","pm3.2i"]
116	2	["ex","reximdva","mpd"]
112	3	["rspcev","syl2anc","ex"]
108	3	["imbi1d","ralbidv","rspcev","syl2anc"]
106	3	["ovex","fvmpt","syl"]
104	2	["ex","ssrdv","eqssd"]
98	1	["imbi1d","ralbidv","rspcev"]
96	2	["eqeq2d","anbi12d","rspcev"]
93	2	["toponunii","restid","ax-mp","eqcomi"]
92	4	["eqeltri","mptex","fvmpt"]
90	5	["eqeltri","mptex","fvmpt","syl"]
90	4	["sseq1","anbi12d","rspcev","syl12anc"]
90	4	["eqtr4d","pm2.61i","eqtri"]
88	0	["0re","1re","elicc2i"]
87	0	["2re","2pos","pm3.2i","a1i"]
84	5	["eqeq2d","anbi12d","rspcev","syl12anc"]
75	3	["eqeq12d","syl5ibr","expcom","a2d"]
69	2	["fveq2","eqeq2d","rspcev","syl2anc"]
64	2	["breq2","imbi1d","ralbidv","rspcev","syl2anc"]
60	9	["a2d","syld","expcom","a2d","uzind4","mpcom","mpd"]
60	2	["expr","a2d","syld","expcom","a2d"]
60	1	["oveq2","oveq1d","fveq2d","oveq1d","oveq12d"]
60	4	["imbi12d","rspcv","syl","mpid"]
60	2	["oveq1","eqeq2d","rspcev","syl2anc"]
60	1	["oveq2","eqeq1d","anbi12d","ralbidv"]
57	2	["elrnmpt","ax-mp","biimpi","adantl"]
57	2	["fveq2","eqeq1d","rspcev","syl2anc"]
57	1	["fvex","eqeltri","mptex","a1i"]
57	3	["jca","ex","reximdv2","mpd"]
57	0	["oveq1","0p1e1","syl6eq","fveq2d"]
57	4	["restid","ax-mp","eqcomi","cncfcn"]
57	5	["sseq1d","anbi12d","rspcev","syl12anc"]
56	4	["toponunii","restid","ax-mp","eqcomi","cncfcn"]
54	8	["expr","a2d","syld","expcom","a2d","uzind4","mpcom"]
50	8	["a2d","syld","expcom","a2d","uzind4","mpcom"]
50	1	["oveq2","oveq1d","fveq2d","oveq1d","oveq12d","cbvmptv"]
50	9	["syld","expcom","a2d","uzind4","mpcom","mpd"]
48	4	["imaeq1d","xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv"]
48	4	["xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv","eqeq2d"]
48	8	["eqeq12d","syl5ibr","expcom","a2d","nn0ind"]
45	2	["breq2","anbi2d","imbi1d","ralbidv","rspcev","syl2anc"]
45	7	["expr","a2d","syld","expcom","a2d","uzind4"]
44	4	["fvprc","syl5eq","fveq2d","3eqtr4a","pm2.61i"]
44	1	["fvprc","syl5eq","rneqd","rn0","syl6eq"]
44	3	["fzsn","syl","eqtrd","uneq2d","eqtrd"]
44	5	["ovex","fvmpt","oveqan12d","adantl","3eqtr4d"]
42	4	["eqeq12d","syl5ibr","expr","a2d","syld","expcom","a2d"]
40	4	["imaeq1d","xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd"]
40	6	["toponunii","restid","ax-mp","eqcomi","cncfcn","mp2an"]
40	4	["uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv","eqeq2d"]
40	4	["xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv"]
40	7	["a2d","syld","expcom","a2d","uzind4"]
40	2	["breq1","imbi1d","ralbidv","rspcev","syl2anc"]
40	0	["breq2","anbi2d","imbi1d","ralbidv","rspcev"]
40	2	["cnfldtopon","toponunii","restid","ax-mp","eqcomi"]
40	8	["expcom","a2d","uzind4","mpcom","mpd"]
40	1	["fveq2","oveq1d","fveq2d","breq1d","imbi12d"]
40	0	["oveq1","eleq1d","rexbidv","cbvrabv","uneq2i"]
40	8	["syld","expcom","a2d","uzind4","mpcom"]
36	8	["a2d","syl5","expcom","a2d","adantl","findcard2s","mpcom"]
36	6	["oveq1","oveq2d","oveq2d","eqeq1d","anbi12d","rspc2ev","syl112anc"]
36	9	["syl5","expcom","a2d","adantl","findcard2s","mpcom","mpi"]
36	2	["oveq1d","fveq2d","oveq1d","oveq12d","cbvmptv"]
36	2	["sylan2","anassrs","ralbidva","rexbidva","ralbidv"]
35	3	["breq2","anbi12d","imbi1d","2ralbidv","rspcev","syl2anc"]
35	2	["breq2","imbi1d","ralbidv","rspcev","syl2anc","ralrimivva"]
35	5	["cbvral","a1i","bitrd","cbvrexv","a1i","bitrd"]
35	4	["eqeq12d","syl5ibr","expr","a2d","syld","expcom"]
35	2	["fvprc","syl5eq","rneqd","rn0","syl6eq","nsyl2"]
35	4	["ltle","syl2anc","sylbid","impr","sylan2b","ralrimiva"]
35	0	["reex","reex","xpex","inex2","nnex","elmap"]
35	3	["syl5ibr","expr","a2d","syld","expcom","a2d"]
30	5	["cbvrex","a1i","bitrd","cbvralv","a1i","bitrd","cbvrexv"]
30	0	["elequ2","anbi1d","exbidv","bibi2d","albidv","imbi2d","exbidv"]
30	5	["fveq2","sseq1d","anbi12d","rspcev","syl12anc","rexlimddv","ralrimivva"]
30	7	["nfop","nfcxfr","nffv","nfop","nfsn","nfun","nfcxfr"]
30	7	["nfres","nfop","nfcxfr","nffv","nfop","nfsn","nfun"]
30	5	["releldm","ex","syl","sylbird","mpan2i","impbid","bitrd"]
30	8	["syl5ibr","expr","a2d","syld","expcom","a2d","uzind4"]
30	7	["oveq2d","oveq2d","eqeq1d","anbi12d","rspc2ev","syl112anc"]
30	5	["ovex","fvmpt","oveqan12d","adantl","3eqtr4d","ralrimivva"]
30	8	["syl5","expcom","a2d","adantl","findcard2s","mpcom"]
24	7	["rexeqbidv","rexeqbidv","rexeqbidv","rspcev","syl2anc","ex","impbid"]
24	7	["rexeqbidv","rexeqbidv","rspcev","syl2anc","ex","impbid","syl5bb"]
24	5	["syl","eleq2d","biimpa","sylbi","a1i","rexlimi","syl"]
24	9	["syl5","expcom","adantl","a2d","findcard2s","mpcom","mpi"]
24	4	["syl6eq","eleq1d","syl5ibrcom","expimpd","rexlimdvva","syl5bi","ralrimiv"]

Theorems which were added to set.mm or discarded are collected in the issue metamath/set.mm#2710

Side remark: the second column in the list is an upper bound on the number of essential hypotheses. It is often the exact value but may differ from it if an essential hypothesis is used multiple times, as demonstrated by line 42, whose second column indicates "2" whereas http://us2.metamath.org/mpeuni/toponrestid.html has one essential hypothesis.

Side remark: the second column in the list is an upper bound on the number of essential hypotheses.

A nice remark, but I believe it is not correct :-) If you take a look at the original post, you'll see that line 42 proof sequence ["toponunii","restid","ax-mp","eqcomi"] does generate a theorem with two hypotheses:

${
  test3.1 $e |- A e. C $.
  test3.2 $e |- A e. ( TopOn ` B ) $.
  test3 $p |- A = ( A |`t B ) $=
    ( crest co wcel wceq toponunii restid ax-mp eqcomi ) ABFGZAACHNAIDACBBAEJKLM $.
$}

Theorem toponrestid from set.mm uses a variant of this proof, which is named test4 in the post. In theory one could detect if one hypothesis is a special case of the other, but in all suggested lemmata in the table it should be assumed that proofs are constructed using a "greedy" strategy described in the google group post. This method of reconstructing lemmata statements should always produce a correct number of essential hypotheses, so the table should be right.

@savask : actually, I thought of that just after hitting the "comment" button ! Yes, the most general proof built on the given proof skeleton will use that number of hypotheses, but the theorem that will shorten proofs by the largest amount may, as in the case of http://us2.metamath.org/mpeuni/toponrestid.html, be a special case and have fewer hypotheses. I should have phrased it that way indeed.

(Indeed, you made more or less that remark in the original thread you linked to... I had forgotten about it.)