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 1.

unfold injective might help; unfold injective at hf also works.

You can use intro a to make progress on a goal which starts ∀ a, .... This translates to "let a be an arbitrary element of (whatever)".

I try to explain apply in Proposition World in the natural number game, but some people find it hard.