`auto` should use `induction`

[TOTBWF]

This should be pretty straightforward. However, it may be about time to figure out a good strategy for implementing the regular and hypothesis searching versions of each tactic.