前回書いた自明な等式の証明だけど，もっと強力なringというタクティクがあるらしい．ドキュメントはLean3のものしか見つからないのだが，import Mathlib.Tactic.RingすればLean4/Mathlib4でも使える．

import Mathlib.Tactic.Ring
lemma a (n m : Nat) : n + m + 1 = 1 + m + n := by ring
lemma b (n m : Nat) : 1 + n + 2 * m = m + n + 1 + m := by ring

すげーとか喜んでしまったが，別に示されるのは自明な式なんだよなぁ……．