fixes sorries

[arademaker]

Can we fix the sorries in the main @derik713 ?

ar@Recreio fad % lake build
⚠ [8680/8694] Replayed Fad.«Chapter5-Ex»
warning: Fad/Chapter5-Ex.lean:148:0: declaration uses `sorry`
warning: Fad/Chapter5-Ex.lean:284:8: declaration uses `sorry`
⚠ [8686/8694] Built Fad.«Chapter7-Ex»
warning: Fad/Chapter7-Ex.lean:57:0: declaration uses `sorry`
⚠ [8688/8694] Built Fad.Chapter8
warning: Fad/Chapter8.lean:97:0: declaration uses `sorry`
⚠ [8691/8694] Built Fad.Chapter12
warning: Fad/Chapter12.lean:48:4: declaration uses `sorry`
warning: Fad/Chapter12.lean:48:4: declaration uses `sorry`
warning: Fad/Chapter12.lean:48:0: declaration uses `sorry`
info: Fad/Chapter12.lean:142:0: 7
info: Fad/Chapter12.lean:143:0: 7
⚠ [8692/8694] Built Fad.«Chapter12-Ex»
warning: Fad/Chapter12-Ex.lean:12:0: declaration uses `sorry`
warning: Fad/Chapter12-Ex.lean:24:0: declaration uses `sorry`
warning: Fad/Chapter12-Ex.lean:60:0: declaration uses `sorry`
warning: Fad/Chapter12-Ex.lean:90:0: declaration uses `sorry`
Build completed successfully (8694 jobs).