1051.lean:10:4-10:11: warning: declaration uses `sorry`
1051.lean:10:4-10:11: warning: declaration uses `sorry`
1051.lean:10:4-10:11: warning: declaration uses `sorry`
1051.lean:17:4-17:12: warning: declaration uses `sorry`
1051.lean:17:4-17:12: warning: declaration uses `sorry`
1051.lean:17:4-17:12: warning: declaration uses `sorry`