mathlib3

ff2639dc - feat(tactic/pretty_cases): provide a skeleton for a proof by induction / cases (#4093)