Here is a "nonsense" theorem that is provable in Lean:
“There exists a real number r such that 1/r = 0.”
If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.
In fact, there is also a type `enat` in mathlib. However, have `x/y` be a term of a type that is not the type of `x` and `y` comes with it's own sets of problems. It doesn't compose as smoothly as homogeneous division.
Note that https://leanprover.github.io is all about the frozen version of Lean 3, while the devs are working on Lean 4.
In the mean time, the community is maintaining a fork of Lean 3 with some nice features + lots of docs and other material. See https://leanprover-community.github.io/
Note that the levels are "fake", so if you lost your progress that's sad, but you can just skip ahead to where you left. (We're looking into adding localStorage or something like that... but we aren't really coders. PRs are welcome!)
“There exists a real number r such that 1/r = 0.”
If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.