Split on whether P holds

Every proof so far has been constructive. To prove P ∨ Q you picked a side, so the proof itself shows which side holds. Some true statements cannot be proved that way. The other De Morgan law, ¬(P ∧ Q) → ¬P ∨ ¬Q, is one of them: knowing that P and Q are not both true does not tell you which one fails.

Classical logic adds the law of the excluded middle: every proposition is either true or false. In Lean it is the theorem Classical.em P : P ∨ ¬P. It is part of the standard library, and Mathlib uses it freely.

The tactic by_cases hp : P uses it to split the proof in two. In the first goal you have hp : P; in the second you have hp : ¬P. You do not need to know which case is the real one, because you prove the goal in both.

In the exercise, suppose P holds. Then Q cannot, since together they would contradict h, so prove the right side ¬Q: introduce hq and build ⟨hp, hq⟩ : P ∧ Q for h. If P does not hold, the left side ¬P is exactly hp.

Worked example

example (P Q : Prop) (hpq : P → Q) (hnpq : ¬P → Q) : Q := by
  by_cases hp : P
  · exact hpq hp
  · exact hnpq hp

The example proves Q from two implications that together cover every case, one branch each. In your exercise the two branches prove different sides of a disjunction.