Right, but without Lean the "insert unlimited sampling" doesn't work.