add patCases_on tactic

[mn200]

The quotation argument to this tactic specifies a pattern that will match one of the free case terms in the goal, and then do Cases_on that term. Avoids the need to write out entirety of large expressions.