Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Hints for challenge 4.

If you've done inequality world in the natural number game then you'll know about the use tactic and you shouldn't have too much trouble with this level. If you're not sure how surjective is defined in Lean then unfold surjective will tell you.