to get well acquainted with these axioms, try playing the "natural number game": https://adam.math.hhu.de/#/g/leanprover-community/nng4
Some things that I think could be improved:
It tells you to click on "Tutorial world", but there is no such button. You have to click "Start" before you see it.
It doesn't tell you what "rfl" stands for.
It doesn't tell you where the "two_eq_succ_one" etc. come from. Are these axioms? Are there infinitely many of them? Are they always available in Lean or are they part of the tutorial world? Why refer to numbers with names instead of digits?
The thing where you have to type "\l" when you want a unicode arrow feels pointlessly obtuse. Why not make it "<-" or something? If humans are going to type it, it should be made out of characters typically found on keyboards.
And I stopped because I got annoyed with typing on my phone. Might try again when I get to a real computer.
EDIT: I just looked it up. "rfl" stands for "reflexivity". Also "rw" is meant to automatically do "rfl" but I think I found that I had to manually do "rfl" after "rw" in the tutorial. https://lovettsoftware.com/NaturalNumbers/Tactics.lean.html
And "two_eq_succ_one" is part of the tutorial world but there are only a small handful of them. In my opinion it is important to distinguish for newbies what is actually part of the system they're learning to use and what is merely part of their learning environment.