Dealing with negation of a disjunction and conjunctions?

Stream: new members

[Greg Leo]

I am having trouble dealing with goal and hypotheses of the form ¬ (P ∧ Q) or ¬ (P ∨ Q). tauto seems to do what I want, but then I have trouble dealing with the result. For instance, when I use tauto on a ¬ (P ∨ Q)it gives me ¬ (P ) and ¬ (Q) as new hypotheses but I can't use the rw tactic on those new hypotheses... the seem kind of broken.

What tactics can I use to reliably split a ¬ (P ∨ Q) into ¬ (P ) and ¬ (Q) hypotheses? How can I reliably change ¬ (P ∧ Q) to ¬P ∨ ¬ Q)?

[Yaël Dillies]

tactic#push_neg

[Greg Leo]

Perfect! It doesn’t give what I expected, but I think this is because the definition of negation in lean.