mathlib3

d001abfd - feat(tactic/basic): adds `contrapose` tactic (#1015)

feat(tactic/basic): adds `contrapose` tactic (#1015) * feat(tactic/basic): adds `contrapose` tactic * fix(tactic/push_neg): fix is_prop testing * Setup error message testing following Rob, add tests for `contrapose` * refactor(tactic/interactive): move noninteractive success_if_fail_with_msg to tactic/core