grind_assoc.lean:2:4-2:5: warning: declaration uses `sorry`
grind_assoc.lean:3:0-3:8: warning: declaration uses `sorry`
grind_assoc.lean:5:21-5:26: warning: declaration uses `sorry`