Prove an or-statement

A proof of P ∨ Q is a proof of one side carrying a label that says which side it is. There is no way to prove a disjunction without committing. Lean has to record which half you established, because later proofs will ask.

In tactic mode you commit with left or right. left replaces the goal P ∨ Q by P; right replaces it by Q. The same two choices written as terms are Or.inl and Or.inr, and those names show up in proof terms and error messages, so it is worth knowing both spellings.

Pick the side you can actually prove. Choosing wrong gives no warning at the left or right line; it gives a type mismatch at the exact after it, naming the proposition you were supposed to produce. The commented block below shows the message.

The goal decides, not the hypothesis. In the worked example one proof ha : A is used on the left in the first conjunct and on the right in the second, because A sits in a different position each time. Read the goal before every left or right.

Worked example

example (A B : Prop) (ha : A) : (A ∨ B) ∧ (B ∨ A) := by
  constructor
  · left
    exact ha
  · right
    exact ha

-- Committing to a side you cannot prove fails at the next line, not at the choice:
--   example (A B : Prop) (hb : B) : A ∨ B := by
--     left
--     exact hb
--
--   Type mismatch
--     hb
--   has type
--     B
--   but is expected to have type
--     A

The same hypothesis answers both bullets, but the tactic differs because A is the left disjunct in one goal and the right disjunct in the other. Your exercise has only one disjunction, so there is only one correct choice.