right

ゴールが ⊢ P ∨ Q であるとき、right はゴールを ⊢ Q に変えます。類似のタクティクに left があります。

variable (P Q : Prop)

example (hQ : Q) : P ∨ Q := by
  right

  -- ゴールが変わる
  guard_target =ₛ Q

  assumption

left, right を使わない方法

以下に示すように、Or.inl は a から a ∨ b を得る関数です。また Or.inr は b から a ∨ b を得る関数です。これを使うことで left や right を使わずに証明できます。

#check (Or.inl : P → P ∨ Q)

#check (Or.inr : Q → P ∨ Q)

example (hP: P) : P ∨ Q := by
  apply Or.inl
  exact hP