KさんがLeanで証明を書く練習をしているので、それに関してのメモ。このメモ自体は檜山による。関数(引数) = 関数'(引数') という命題を示す根拠として、 A = B がassumeされていて、f(A) = f(B) を示したいなら、congr_arg 規則を使う。 f = g がassumeされ…