3965_2.lean:11:8-11:19: warning: declaration uses `sorry`
3965_2.lean:32:12-32:18: warning: declaration uses `sorry`
3965_2.lean:34:28-34:33: warning: declaration uses `sorry`
3965_2.lean:41:18-41:27: warning: declaration uses `sorry`
3965_2.lean:43:18-43:27: warning: declaration uses `sorry`
3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
3965_2.lean:91:8-91:25: warning: declaration uses `sorry`