convert
ローカルコンテキストに現在のゴールに近いけれども等しくはない h
があるとき、exact h
としても失敗します。しかし convert h
は成功する可能性があり、成功した場合は h
とゴールの差分を新たなゴールとします。
import Mathlib.Tactic.Convert
variable (a b c: Nat)
example (f : Nat → Nat) (h : f (a + b) = 0) (hc: a + b = c) : f (c) = 0 := by
-- `h` はゴールと等しくないので失敗する
fail_if_success exact [h]
-- `h` とゴールの差分を新たなゴールにする
convert h
-- ゴールが `⊢ c = a + b` に変わっている
show c = a + b
rw [hc]