grind_split_issue.lean:37:0-37:7: warning: declaration uses `sorry`