Lean，結合律と可換性をきちんと意識して計算しないとならないのがうざくて，例えば$n + m + 1 = 1 + m + n$というどう考えても自明の式も（例えば）きちんと結合律一回可換法則二回を適用しないとならない．

lemma a (n m : Nat) : n + m + 1 = 1 + m + n := by
  rw[add_assoc 1 m n]
  rw[add_comm]
  rw[add_comm n m]

と思っていたのだが，ac_rflというタクティクがあることを知った．可換な結合的演算があった時にそれだけを使って示せる等式の証明をいっぱつでやってくれるらしい．少なくとも上の式はac_rfl一発で終わる．ただし他の法則は使えないので，例えば$1 + n + 2 * m = m + n + 1 + m$は駄目．rw[two_mul]で一度$2*m = m + m$と書き換えてからやればよい．