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.