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