Comment by alimw

Sure!

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