left

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

variable (P Q : Prop)

example (hP : P) : P ∨ Q := by
  left

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

  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