replace

replace は have と同じく補題を入手するためのタクティクですが、have とは異なりローカルコンテキストにすでにある命題を置き換えることができます。

have を使った場合、ローカルコンテキストにすでに h : P がある状態で、再び h という名前で別の命題を示すと、古い方の h はアクセス不能になって † が付いた状態になってしまいます。

replace であれば、古い方が新しい方に置き換えられ、† の付いた命題は出現しません。

import Mathlib.Tactic -- 大雑把に import する

/-- `5 * n` が偶数なら、`n` も偶数 -/
example : ∀ (n : ℤ), Even (5 * n) → Even n := by
  intro n hn

  -- `Even (5 * n)` という仮定を分解
  obtain ⟨k, hk⟩ := hn

  -- 以下がローカルコンテキストに追加される
  guard_hyp hk : 5 * n = k + k

  -- `k + k` という形が使いづらいので、`2 * k` に置き換える
  replace hk : 5 * n = 2 * k := by
    rw [hk]
    ring

  -- `hk` の内容が変化している
  guard_hyp hk : 5 * n = 2 * k

  -- 計算をする
  have := calc
    n = 5 * n - 4 * n := by ring
    _ = 2 * k - 4 * n := by rw [hk]
    _ = 2 * (k - 2 * n) := by ring

  exists k - 2 * n
  nth_rw 1 [this]
  ring

Lean by Example

replace