mathlib3

debdd909 - feat(tactic/ext): support rintro patterns in `ext` (#12875)

feat(tactic/ext): support rintro patterns in `ext` (#12875) The change is actually quite simple, since `rintro_pat*` has approximately the same type as `rcases_pat*`.