have(Lean)
have: 補題を用意する - Lean4 タクティク逆引きリスト