conv

conv は変換モードに入るためのタクティクです。詳細についてはTheorem Proving in Lean4をご参照ください。