Identify good results to upstream to mathlib. Create PRs.
Identify good results to upstream to mathlib. Create PRs.