474_lean3.lean:3:8-3:32: warning: declaration uses `sorry`
474_lean3.lean:7:8-7:32: warning: declaration uses `sorry`
474_lean3.lean:11:8-11:32: warning: declaration uses `sorry`