mathlib3

947f7bde - feat(tactic/assert_exists): user command for assertions about imports (#17416)

feat(tactic/assert_exists): user command for assertions about imports (#17416) I will defer actually using this to a later PR. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>