【Lean4】left,right

left,right

目標が「または」のとき、どちらを証明するか選ぶ

Plaintext

example (P Q : Prop) (hP : P) : P ∨ Q := by
  left
  exact hP
  
example (P Q : Prop) (hQ : Q) : P ∨ Q := by
  right
  exact hQ

example (P Q : Prop) (hP : P) : P ∨ Q := by
  left
  exact hP
  
example (P Q : Prop) (hQ : Q) : P ∨ Q := by
  right
  exact hQ