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, ask in each case which side of the goal you can now prove. If P holds, Q cannot also hold without contradicting h. If P fails, the context already says so.

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.