[Merged by Bors] - feat(tactic/by_contra): add by_contra' tactic

[jcommelin]

---

[robertylewis]

After reflecting for a second, it seems a little strange that only push_neg is being used to show equivalence in the h : t case. Why not a full simp? push_neg seems right in the case where t is omitted but too restrictive here. @digama0 was there a reason I'm overlooking?

You could even take a finishing tactic as an optional argument, although this is probably overkill.

[digama0]

@robertylewis I just implemented the tactic as specified by Johan. Maybe simp is better, although this will complicate the input since you will want a place to put the simp lemmas. Are all push_neg lemmas also simp lemmas?

[robertylewis]

Hmm, my guess about how push_neg is implemented was wrong, I figured it used a simp set. What it does now is better. If there are actual use cases using push_neg I don't think it's worth the effort to make up the difference -- this doesn't seem like a commonly used feature either way.

[robertylewis]

bors d+

[bors]

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed:

• Build mathlib

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests