1026.lean:1:4-1:7: warning: declaration uses `sorry`
1026.lean:1:0-7:19: warning: declaration uses `sorry`
1026.lean:9:8-9:10: warning: declaration uses `sorry`