std4#160 case : t => tac tactic to search for goals by type

Stream: PR reviews

[Kyle Miller]

std4#160 is introducing a version of case where you can select a goal by unifying against a type, for example case : Injective _ => assumption. Mentioning it here in case any mathlib meta reviewers might take a look at this std PR.