mathlib3

9a019fc3 - Merge branch 'alexjbest/cleanup_by_cases' into alexjbest/unnecessary_by_cases