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

This came up in the course I'm teaching this term. Recall that set.subset.antisymm is the theorem that if A ⊆ B and B ⊆ A then A = B. If you also prove (𝕀 (𝕍 (𝕀 W))) = 𝕀 W (and the proof is the same as the challenge of course) then you can deduce that the images of 𝕍 and 𝕀 biject with each other, which looks a bit like the Nullstellensatz in the context we're in, in my course. Why is it not the Nullstellensatz?