trivially false

Stream: general

[Kevin Buzzard]

Am I supposed to resolve situations like

H : (1 / 2).denom = 1
⊢ false

with revert H,exact dec_trivial or is there some less clunky way where I apply something to H directly?

[Mario Carneiro]

I use absurd H dec_trivial for this kind of thing

[Kevin Buzzard]

Thanks

[Kenny Lau]

import data.rat

theorem test (H : (1 / 2 : ℚ).denom = 1) : false :=
nat.no_confusion (nat.succ_inj H)

[Kenny Lau]

@Mario Carneiro interestingly cases fails on H or on nat.succ_inj H, and so does injections with H

[Kevin Buzzard]

ha ha, I'll let you know the next time I'm in this situation Kenny and you can come up with some bespoke solution for me :-)

[Mario Carneiro]

I get timeouts on everything that does something equivalent to cases on H, even match H with end times out

[Mario Carneiro]

match (show 2 = 1, from H) with end works, and other equivalent things

[Mario Carneiro]

it must be unfolding things in a weird order