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

  #eval List.map f (List.range 100)

  theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = "" := by
    unfold f
    split_ifs
    · 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));

    inductive FizzBuzz where
      | fizz
      | buzz
      | fizzBuzz
      | none
    
    def fizzBuzz (n : Nat) : FizzBuzz :=
      if n % 15 == 0 then .fizzBuzz
      else if n % 3 == 0 then .fizz
      else if n % 5 == 0 then .buzz
      else .none
    
    instance : ToString FizzBuzz where
    toString : FizzBuzz → String
      | .none => ""
      | .fizz => "Fizz"
      | .buzz => "Buzz"
      | .fizzBuzz => "FizzBuzz"
    
    def stringFizz (n : Nat) : String :=
      toString <| fizzBuzz n
    
    def printFizz (n : Nat) : IO Unit := do
      println! s!"{fizzBuzz n}"

  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))