Lean summary theorem: generate minimal imports from theorem names

A summary theorem that cites hundreds of lemmas (e.g. a table of values, one lemma per cell) is tempting to write with import Club / the whole project root. Then it breaks whenever any unrelated WIP file in the project fails to build. Fix: grep for ^(public )?theorem <name>\b for each cited name, take the unique defining files, and import exactly those. For 276 cells this came to 21 modules. Rebuilding the summary file then took 6 s, and it no longer depends on other people's in-progress files.