Mathematics in Lean