【Lean4】cases

cases

仮定を場合分けしたり、構造を分解したりする

Plaintext

example (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by
  cases h with
  | inl hP =>
      right
      exact hP
  | inr hQ =>
      left
      exact hQ

example (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by
  cases h with
  | inl hP =>
      right
      exact hP
  | inr hQ =>
      left
      exact hQ