Skip to content

Commit

Permalink
deploy: 3e44cd7
Browse files Browse the repository at this point in the history
  • Loading branch information
@Seasawher
Seasawher committed Oct 25, 2023
1 parent dfb4796 commit 3c532ee
Show file tree
Hide file tree
Showing 49 changed files with 373 additions and 52 deletions.
2 changes: 1 addition & 1 deletion 404.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@

<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply_assumption.html">apply_assumption: 仮定から後方推論</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索で後方推論</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定からゴールを閉じる</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="choose.html">choose: 選択関数を得る</a></li><li class="chapter-item expanded "><a href="congr.html">congr: ゴールの差異に注目する</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 爆発律</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="convert.html">convert: 惜しい補題を使う</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exact_question.html">exact?: ゴールをライブラリ検索</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="guard_hyp.html">guard_hyp: 仮定や補題を確認</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="linarith.html">linarith: 線形(不)等式を示す</a></li><li class="chapter-item expanded "><a href="nlinarith.html">nlinarith: 非線形な(不)等式を示す</a></li><li class="chapter-item expanded "><a href="push_neg.html">push_neg: ドモルガン</a></li><li class="chapter-item expanded "><a href="refine.html">refine: プレースホルダを使う</a></li><li class="chapter-item expanded "><a href="rel.html">rel: 不等式を使う</a></li><li class="chapter-item expanded "><a href="replace.html">replace: 補題の入れ替え</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 関係の反射性を示す</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="says.html">says: タクティク提案の痕跡を残す</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li><li class="chapter-item expanded "><a href="wlog.html">wlog: 一般性を失わずに特殊化</a></li></ol>
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply_assumption.html">apply_assumption: 仮定から後方推論</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索で後方推論</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定からゴールを閉じる</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="choose.html">choose: 選択関数を得る</a></li><li class="chapter-item expanded "><a href="congr.html">congr: ゴールの差異に注目する</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 爆発律</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="convert.html">convert: 惜しい補題を使う</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exact_question.html">exact?: ゴールをライブラリ検索</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="guard_hyp.html">guard_hyp: 仮定や補題を確認</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="linarith.html">linarith: 線形(不)等式を示す</a></li><li class="chapter-item expanded "><a href="nlinarith.html">nlinarith: 非線形な(不)等式を示す</a></li><li class="chapter-item expanded "><a href="push_neg.html">push_neg: ドモルガン</a></li><li class="chapter-item expanded "><a href="refine.html">refine: プレースホルダを使う</a></li><li class="chapter-item expanded "><a href="rel.html">rel: 不等式を使う</a></li><li class="chapter-item expanded "><a href="replace.html">replace: 補題の入れ替え</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 関係の反射性を示す</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="says.html">says: タクティク提案の痕跡を残す</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="split.html">split: if 式を示す</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li><li class="chapter-item expanded "><a href="wlog.html">wlog: 一般性を失わずに特殊化</a></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle"></div>
</nav>
Expand Down
2 changes: 1 addition & 1 deletion aesop.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@

<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html" class="active">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply_assumption.html">apply_assumption: 仮定から後方推論</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索で後方推論</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定からゴールを閉じる</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="choose.html">choose: 選択関数を得る</a></li><li class="chapter-item expanded "><a href="congr.html">congr: ゴールの差異に注目する</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 爆発律</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="convert.html">convert: 惜しい補題を使う</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exact_question.html">exact?: ゴールをライブラリ検索</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="guard_hyp.html">guard_hyp: 仮定や補題を確認</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="linarith.html">linarith: 線形(不)等式を示す</a></li><li class="chapter-item expanded "><a href="nlinarith.html">nlinarith: 非線形な(不)等式を示す</a></li><li class="chapter-item expanded "><a href="push_neg.html">push_neg: ドモルガン</a></li><li class="chapter-item expanded "><a href="refine.html">refine: プレースホルダを使う</a></li><li class="chapter-item expanded "><a href="rel.html">rel: 不等式を使う</a></li><li class="chapter-item expanded "><a href="replace.html">replace: 補題の入れ替え</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 関係の反射性を示す</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="says.html">says: タクティク提案の痕跡を残す</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li><li class="chapter-item expanded "><a href="wlog.html">wlog: 一般性を失わずに特殊化</a></li></ol>
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html" class="active">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply_assumption.html">apply_assumption: 仮定から後方推論</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索で後方推論</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定からゴールを閉じる</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="choose.html">choose: 選択関数を得る</a></li><li class="chapter-item expanded "><a href="congr.html">congr: ゴールの差異に注目する</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 爆発律</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="convert.html">convert: 惜しい補題を使う</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exact_question.html">exact?: ゴールをライブラリ検索</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="guard_hyp.html">guard_hyp: 仮定や補題を確認</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="linarith.html">linarith: 線形(不)等式を示す</a></li><li class="chapter-item expanded "><a href="nlinarith.html">nlinarith: 非線形な(不)等式を示す</a></li><li class="chapter-item expanded "><a href="push_neg.html">push_neg: ドモルガン</a></li><li class="chapter-item expanded "><a href="refine.html">refine: プレースホルダを使う</a></li><li class="chapter-item expanded "><a href="rel.html">rel: 不等式を使う</a></li><li class="chapter-item expanded "><a href="replace.html">replace: 補題の入れ替え</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 関係の反射性を示す</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="says.html">says: タクティク提案の痕跡を残す</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="split.html">split: if 式を示す</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li><li class="chapter-item expanded "><a href="wlog.html">wlog: 一般性を失わずに特殊化</a></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle"></div>
</nav>
Expand Down
Loading

0 comments on commit 3c532ee

Please sign in to comment.