right
Summary
There are two ways to prove ⊢ P ∨ Q
; you can either prove P
or you can prove Q
. If you want to change the goal to Q
then use the right
tactic.
Details
It’s a theorem in Lean that Q → P ∨ Q
, and the right
tactic applies this theorem.
Further notes
See also left
. More generally, if your goal is an inductive type with two constructors, left
applies the first constructor, and right
applies the second one.