In Game/Levels/L10Levels/L09_Subseq.lean I don't think I would have guessed that the line change |a (2 * n) - 1| < ε was needed without a hint about it.