grind_usr.lean:9:15-9:19: warning: declaration uses `sorry`
grind_usr.lean:34:0-34:7: warning: declaration uses `sorry`
grind_usr.lean:60:0-60:7: warning: declaration uses `sorry`
grind_usr.lean:70:0-70:7: warning: declaration uses `sorry`