Comment by mauricioc

Whoever wrote this was probably trying to showcase more of the language's functional features (or just trying to be clever). This works:

  def main :=
    for i in [1:101] do
      if i % 15 == 0 then
         IO.println "FizzBuzz"
      else if i % 3 == 0 then
         IO.println "Fizz"
      else if i % 5 == 0 then
         IO.println "Buzz"
      else
         IO.println s!"{i}"

You can run it with `lean --run FizzBuzz.lean`, and you can read more about programming in Lean 4 at https://leanprover.github.io/functional_programming_in_lean/.