def f (n : Nat) : String :=
    Option.getD
      (Option.merge String.append
        (if n % 3 = 0 then "Fizz" else none)
        (if n % 5 = 0 then "Buzz" else none))
      (toString n)

  #eval List.map (fun k => f (k + 1)) (List.range 100)

  theorem poop (n : Nat) :
      f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = toString n := by
    unfold f
    split <;> split
    · exact Or.inl rfl
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inl rfl))
    · exact Or.inr (Or.inr (Or.inr rfl))

Just for comparison, in Typescript you can write:

  function f(n:number){
    if (n%3==0 && n%5==0) return "FizzBuzz"
    if (n%3==0) return "Fizz"
    if (n%5==0) return "Buzz"
    return "";
  }

Then, I can write:

  function *iFizzBuzz(steps:number){
     for (let i=0; i<steps; i++){
        const fb = f(i); 
        if (fb) yield fb;
     }
  }

  const fizzBuzz100 = Array.from(iFizzBuzz(100));