「数学系のためのLean勉強会」の教材を解いた

[haruhisa-enomoto]

https://github.com/yuma-mizuno/lean-math-workshop
この教材のTutorial全てに一応解答を書いてみました。
解析は不等式評価等が慣れずちょっと難しかったです。
https://github.com/haruhisa-enomoto/lean-workshop-tutorial-fork/tree/my-cheat-sol/Tutorial/Advanced

[haruhisa-enomoto]

勉強会のREADMEについてですが、リポジトリ作者さんに聞いてみたところ、管理が長期に渡ると大変になることに比べてメリットもあまりないことから、各自がこういうコミュニティで共有すればいいのではということになりました。
とりあえずこの勉強会のものについては、ここを解答共有の場としてここに（本人や同意が取れた人の解答リンク集を）集めてみるといいかもしれません。

[Seasawher]

@aconite-ac よろしければ解答の共有お願いします

[aconite-ac]

https://github.com/aconite-ac/lean-math-workshop-fork/tree/aconite-sol/Tutorial

「数学系のためのLean勉強会」の教材の全問題に対する自身の解答例です。
simpやaesopをあまり使わない方針の解答です。
showタクティクを用いている箇所は、dsimpタクティクを用いた方が自然かもしれません。
また、Category/Lecture2.lean内のexample (F : Functor Coproduct.Shape (CommAlgCat R)) : Colimit (tensorCocone F)の解答については、
誘導に乗れていないためあまり参考にならないかもしれません。