rw: 等式による書き換え

rw [h] は，等式 h : a = b を使って，ゴール中の a を b に書き換えます． 命題の中では，同値 P ↔ Q も書き換えに使えます． rw は指定された補題を左から右へ使い，rw [← h] と書くと逆向きに使います．

example (a b c : Nat) (h : a = b) : a + c = b + c := by
  rw [h]

書き換えの向きを逆にしたいときは ← を使います．

example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]

example (a b : Nat) : b + a = a + b := by
  rw [← Nat.add_comm a b]

仮定の中を書き換えるときは rw [h] at h2 のように at を使います．

example (a b c : Nat) (h : a = b) (h2 : a + c = 10) : b + c = 10 := by
  rw [h] at h2
  exact h2

congr は，両辺に同じ関数が適用されている等式を，引数の等式に帰着します． たとえば f a = f b を示す問題を a = b に変えることができます． 次の例では，残った a = b のゴールをローカルコンテキストの h : a = b が閉じています．

example (f : Nat → Nat) (a b : Nat) (h : a = b) : f a = f b := by
  congr

演習

rw を使って等式を書き換えてください．

example (a b c : Nat) (h : a = b) : a + c = b + c := by
  sorry