tactic1.lean:59:0-59:7: warning: declaration uses `sorry`
tactic1.lean:62:0-62:7: warning: declaration uses `sorry`
tactic1.lean:68:0-68:7: warning: declaration uses `sorry`