grind_ring_1.lean:59:0-59:7: warning: declaration uses `sorry`
grind_ring_1.lean:72:0-72:7: warning: declaration uses `sorry`