【Lean4】rw

rw

等式を使って書き換える

Plaintext

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

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

逆向きに書き換えるには、rw [← h]を使う