mathlib

61fa4896 - feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses (#2368)

feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses (#2368) ``` /-- Perform case analysis on a `trunc` expression, preferentially using the recursor `trunc.rec_on_subsingleton` when the goal is a subsingleton, and using `trunc.rec` otherwise. Additionally, if the new hypothesis is a type class, reset the instance cache. -/ ```