Because Lean's constructor tactic cannot be applied to a goal containing a disjunction.

Because the negation of a conjunction is logically weaker than the negation of a disjunction in all logical systems

Because the truth table for De Morgan's Laws shows a contradiction in the second law when P and Q are both false.

Because it requires the principle that every proposition is either true or false to select a specific side of the disjunction.