Oops! I checked the spec and it's supposed do something more like this:

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

Thank you. I must admit, I have trouble making sense of it.

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 "";
  }

The return type of this function will be inferred as "Fizz"|"Buzz"|"FizzBuzz"|"".

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

The type of fizzBuzz100 will be inferred as ("Fizz"|"Buzz"|"FizzBuzz")[];

Lean will not create a custom type to infer for each function; it will either infer an existing type or report failure; it will also not automatically coerce to String. What you see above is a proof in tactic mode of your specification as a theorem. If you want to guarantee the outputs of a function, you need to specify a custom type. For instance:

    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}"

Awesome! Where did the "split_ifs" tactic come from though? Mathlib? In your opinion does it make sense to do program verification without using Mathlib, or would you recommend just using it pretty much all the time?

Yes split_ifs is in Mathlib so I have replaced it with split (twice) which is in Core. I believe there is also an intermediate level Std. I'm not sure why you'd want to avoid Mathlib but I daresay it's possible for many types of problem.