conv

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