mathlib3

d7a4f727 - feat(norm_cast): dite_cast to match ite_cast (#6092)

feat(norm_cast): dite_cast to match ite_cast (#6092) There's already an `ite_cast` lemma, for pushing a cast inside an `ite`. This adds the analogous `dite_cast`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>