apply(Lean)

apply(Lean)

現在のゴールに適用可能なmathlibの定理(もしくは定義)を探すタクティク

code:lean

example Group G Group H (f : G →* H) (a b : G) :

f (a * b) = f a * f b := by

-- ヒント: apply?を使う

-- apply?を使うと「Try this: exact MonoidHom.map_mul f a b」というメッセージが出る(!!)

exact MonoidHom.map_mul f a b