The implication and non-implication graphs can be extracted from the current source state by making use of the extract_implications tool. See lake exe extract_implications -h for supported options.
The transitive closure of the implication graph calculates the maximum reachable set from a given node, and the transitive reduction calculates the minimal set of edges required to maintain reachability on the graph. Various implementations exist in Python (closure reduction), Ruby (closure reduction), and Lean (closure).
Only the minimal required set of proofs should be submitted upstream. The minimal set can be calculated by computing reduction(current implications ∪ new implications) - current implications. Look at Steps 1 and 3 here for an example.
TODO