> your Lean files are full of `sorry`s

You meant this literally, but this such a beautiful insult.