left and right

If the goal is of the form P ∨ Q, then the left tactic changes the goal to P and the right tactic changes it to Q. Here is an example.

try it!

example (P Q : Prop) (HP : P) : P ∨ Q :=
begin
  -- goal is P ∨ Q
  left,
  -- goal now P
  exact HP
end

More generally if the goal is any inductive type with two constructors, then the left tactic changes the goal to the types needed for the first constructor, and the right tactic changes the goal to the types needed for the second constructor.