/- # conv

`conv` は変換モードに入るためのタクティクです。詳細については[Theorem Proving in Lean4](https://aconite-ac.github.io/theorem_proving_in_lean4_ja/conv.html)をご参照ください。-/