【Lean4】apply

apply

目標を証明するために使えそうな定理を適用し、残りの条件を新しい目標にする

Plaintext

example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by
  apply hPQ
  exact hP

example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by
  apply hPQ
  exact hP