more explicit contradiction than linarith

Stream: new members

[Siyuan Yan]

d : ℕ
a : ℤ
h : a.gcd ↑d ≠ 1
this : a.gcd ↑d = 1
⊢ false

instead of doing linarith to close the goal, is there a more explicit way of contradicting h and this?

[Yaël Dillies]

exact h this

[Yaël Dillies]

docs#ne is defined as a = b → false, so you can just apply such an hypothesis with a proof of a = b

[Kevin Buzzard]

This evil technique is called "abuse of definitional equality" and it still makes me feel a bit dirty.

[Siyuan Yan]

super cool! thanks!

[Kevin Buzzard]

contradiction might work. This tactic explicitly looks for two hypotheses of the form P and not P, but I don't know if it's clever enough to look through x \ne y and see that it's definitionally equal to \not (x = y)

[Adam Topaz]

contradiction should indeed work, but I think it would be slightly slower in this case than exact ....
If you have a large local context, contradiction can get fairly slow.

[Floris van Doorn]

Kevin Buzzard said:

This evil technique is called "abuse of definitional equality" and it still makes me feel a bit dirty.

If you want to make sure that Kevin is not feeling dirty, you can write h.elim this (docs#ne.elim & docs#not.elim), but h this is very much accepted in mathlib.

[Kyle Miller]

There's also exact absurd this h

[Eric Wieser]

Kevin could argue that absurd is still abusing definitional equality of ne, just not of not