Closing negated goals quickly

Stream: new members

[Eric Wieser]

I have left as my goal:

hnp : ¬p head,
hnq : ¬q head
⊢ ¬(p head ∨ q head)

Is there a quick tactic-mode incantation to finish off?

[Bhavik Mehta]

tactic#tautology

[Eric Wieser]

tauto by itself does not work

[Bhavik Mehta]

Or maybe tauto!

[Eric Wieser]

intro h, cases h, exact hnp h, exact hnq h does but feels clumsy.

[Bhavik Mehta]

If not finish should do it too

[Eric Wieser]

import tactic being missing strikes again. tauto worked after all
Thanks!

[Eric Wieser]

Another goal I'm struggling to close quickly:

hs : (filter (λ (x : α), p x ∨ q x) tail).length ≤ (filter p tail).length + (filter q tail).length,
⊢ (filter (λ (x : α), p x ∨ q x) tail).length + 1 ≤ (filter p tail).length + 1 + ((filter q tail).length + 1)

rw doesn't seem to work here, and finish works in my installation but not the codewars one.

[Reid Barton]

linarith should be smart enough for this one

[Eric Wieser]

Bingo, knew I'd seen this type of issue before.