The goal of Lean is to be a programming language used to prove math theorems. Looking at a FizzBuzz implementation and balking at the complexity is utterly missing the point.