apply .. at
apply
は通常ゴールに対して適用しますが、at
を付けてローカルコンテキストの命題などに対して使用するという使い方ができます。
実際にはこの構文は apply
と似ているだけで、別のタクティクです。この at
がついている構文は通常の apply
とは異なり、後方推論ではなく前方推論になります。
import Mathlib.Tactic.ApplyAt
variable (P Q : Prop)
example (h : P → Q) (hP : P) : Q := by
-- `hP` に `h` を適用してしまう
apply h at hP
-- `hP` が書き換わる
guard_hyp hP : Q
assumption
便利な記法以上のものではなく、他のタクティクを利用しても同じことができます。
example (h : P → Q) (hP : P) : Q := by
-- `apply at` は `replace` と同じように動作する
replace hP := h hP
-- `hP` が書き換わる
guard_hyp hP : Q
assumption