1163.lean:6:8-6:15: warning: declaration uses `sorry`
1163.lean:11:8-11:15: warning: declaration uses `sorry`
1163.lean:25:8-25:15: warning: declaration uses `sorry`