prololo https://blog.hatena.ne.jp/prololo/ prololo’s diary https://prololo.hatenablog.com/ ちょっと空いた時間にLEANで圏論をやってる． 自然変換の等価性を証明するときに困ったけど，友達に聞いて解決したので備忘録． 結論から言うと， 構造体を要素に分解するときはcases_onを使う． cc tacticは便利． 構造体hogeで説明（？） 次のようにして構造体hogeを定義し， 命題eq_hoge_of_eq_fugaを証明したい． structure hoge := (fuga : ℕ) (piyo : fuga = fuga) lemma eq_hoge_of_eq_fuga : ∀ (hg₁ hg₂ : hoge), hg₁.fuga = hg₂.fuga → hg₁ = … 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fprololo.hatenablog.com%2Fentry%2F2018%2F12%2F20%2F215702" title="LEANで構造体の等価性を証明する - prololo’s diary" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2018-12-20 21:57:02 rich https://prololo.hatenablog.com/entry/2018/12/20/215702 1.0 100%