mathlib4#2204 port success_if_fail_with_msg

Stream: PR reviews

[Scott Morrison]

@Thomas Murrills, would you mind having a look at Mathlib/Tactic/Expect.lean and seeing if we can remove the duplication with your recent PR?

[Thomas Murrills]

Ah…will do.

[Thomas Murrills]

So a docstring in Mathlib/Tactic/Expect.lean says

expect_failure is similar to success_if_failure from core, except that success_if_failure omits withoutRecover. When this is fixed, expect_failure can be deprecated or turned into a macro.

Is this copypasta from lean3, given that the name success_if_failure is wrong?

If it's not copypasta and just accidentally misrefers to fail_if_success, it seems that fail_if_success now includes withoutRecover in core. It also looks like expect_fail and expect_fail_msg aren't currently used in any tests.

So, should we just remove Mathlib/Tactic/Expect.lean? (And its test file?)

[Thomas Murrills]

Here's a PR for that in case that's the right move: !4#3026 (If not, I'll just adjust that PR accordingly :) )

[Scott Morrison]

Looks reasonable to me.