mathlib3

28775ced - feat(tactic/interactive): guard_{hyp,target}_mod_implicit (#12668)

feat(tactic/interactive): guard_{hyp,target}_mod_implicit (#12668) This adds two new tactics `guard_hyp_mod_implicit` and `guard_target_mod_implicit`, with the same syntax as `guard_hyp` and `guard_target`. While the `guard_*` tactics check for syntax equality, the `guard_*_mod_implicit` tactics check for definitional equality with the `none` transparency