3965.lean:8:4-8:15: warning: declaration uses `sorry`
3965.lean:12:8-12:30: warning: declaration uses `sorry`
3965.lean:20:18-20:26: warning: declaration uses `sorry`
3965.lean:35:8-35:22: warning: declaration uses `sorry`
3965.lean:41:8-41:16: warning: declaration uses `sorry`
3965.lean:60:4-60:8: warning: declaration uses `sorry`
3965.lean:75:9-75:29: warning: declaration uses `sorry`
3965.lean:79:0-79:8: warning: declaration uses `sorry`
3965.lean:83:4-83:10: warning: declaration uses `sorry`
3965.lean:85:9-85:21: warning: declaration uses `sorry`
3965.lean:87:8-87:22: warning: declaration uses `sorry`
3965.lean:90:0-90:8: warning: declaration uses `sorry`
3965.lean:112:4-112:10: warning: declaration uses `sorry`
3965.lean:112:4-112:10: warning: declaration uses `sorry`
3965.lean:112:4-112:10: warning: declaration uses `sorry`
3965.lean:116:8-116:17: warning: declaration uses `sorry`
3965.lean:151:8-151:14: warning: declaration uses `sorry`
3965.lean:170:8-170:28: warning: declaration uses `sorry`
3965.lean:189:8-189:29: warning: declaration uses `sorry`