Logic in Lean, example sheet 6 : "or" (∨`) #
We learn about how to manipulate P ∨ Q in Lean.
Tactics #
You'll need to know about the tactics from the previous sheets, and also the following tactics
leftandrightcases(new functionality)
The left and right tactics. #
If your goal is ⊢ P ∨ Q then left, will change it to ⊢ P
and right, will change it to ⊢ Q.
The cases tactic again #
If we have h : P ∨ Q as a hypothesis then cases h with hP hQ
will turn your goal into two goals, one with hP : P as a hypothesis
and the other with hQ : Q.