KさんがLeanで証明を書く練習をしているので、それに関してのメモ。このメモ自体は檜山による。
関数(引数) = 関数'(引数') という命題を示す根拠として、
- A = B がassumeされていて、f(A) = f(B) を示したいなら、congr_arg 規則を使う。
- f = g がassumeされていて、f(A) = g(A) を示したいなら、congr_fun 規則を使う。
- f = g, A = B がassumeされていて f(A) = g(B) を示したいなら、congr 規則を使う。congr へのパラメータは 関数の等式 引数の等式（fun_eq arg_eq）の順になる。こういう順番も覚える必要がある。
- 根拠＝使うべき規則を示さないと自動的には推論してくれない。
参考： https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html
