I have some PRs marked as please-adopt here, here, and here, If you complete these lemmas and get the PRs merged, I will give you 1000 Mana.
proved https://github.com/leanprover-community/mathlib4/pull/7170 :-)
@SebastianZimmer are you the same person who completed the last PR on the list here?
1,000 to start trading!1,0001,000