matchtac.lean:75:8-75:12: warning: declaration uses `sorry`
matchtac.lean:85:8-85:13: warning: declaration uses `sorry`
matchtac.lean:90:8-90:14: warning: declaration uses `sorry`