By the way, 3 and 4 are pretty much the same in Lean, assuming you define "R\{0}" using complementation rather that somehow defining the nonzero reals from scratch.