split の説明を詳細にする

src/SUMMARY.md

@@ -44,7 +44,7 @@
 - [show: 示すべきことを宣言](./show.md)
 - [simp: 簡約](./simp.md)
 - [sorry: 証明したことにする](./sorry.md)
-- [split: if 式を示す](./split.md)
+- [split: if 式を含む命題を示す](./split.md)
 - [suffices: 十分条件に帰着](./suffices.md)
 - [trivial: 自明](./trivial.md)
 - [wlog: 一般性を失わずに特殊化](./wlog.md)

src/split.md

@@ -4,6 +4,13 @@
 
 if 式を扱う必要が生じるのは，典型的には Lean で定義したアルゴリズムや関数に関して，何か性質を証明しようとしたときです．
 
+ゴールが `⊢ Q (if P then a else b)` であったときに，`split` を使用すると2つのサブゴールが生成されます．具体的には
+
+* 1つはローカルコンテキストに `† : P` が追加され，ゴールが `⊢ Q (a)`
+* 1つはローカルコンテキストに `† : ¬ P` が追加され，ゴールが `⊢ Q (b)`
+
+というサブゴールです．`split` によって追加される仮定は名前がついているとは限りません．名前がついていなかった場合，`case` などで名前を付けることができます．
+
 ```lean
 {{#include ../Examples/Split.lean:first}}
 ```