変更内容取り込み (#67)

Author: s-taiga

MIL/C01_Introduction/S01_Getting_Started.lean

@@ -101,9 +101,9 @@ OMIT. -/
 
 1. ``ctrl+shift+P`` (Macの場合は ``command+shift+P`` )を押します．
 
-2. 上記手順で現れたバーで ``Lean 4: Open Documentation View`` と打ち込み，エンターキーを押します．（もしくはメニュー内で上記の文字列が選択されてハイライトされている場合はそのままエンターキーを押しても良いです．）
+2. 上記手順で現れたバーで ``Lean 4: Docs: Show Documentation Resources`` と打ち込み，エンターキーを押します．（もしくはメニュー内で上記の文字列が選択されてハイライトされている場合はそのままエンターキーを押しても良いです．）
 
-3. これで開いたウィンドウで ``Open documentation of current project`` をクリックします．
+3. これで開いたウィンドウで ``Mathematics in Lean`` をクリックします．
 
 TEXT. -/
 /- OMIT:

MIL/C01_Introduction/S02_Overview.lean

@@ -202,7 +202,7 @@ That said, in this book, our emphasis will be on the use of tactics.
 
 OMIT. -/
 /- TEXT:
-証明を組み立てるうえで，細かいステップごとに段階的にフィードバックを受けられることは，非常に役に立ちます．このため，タクティクを使うと証明項を書き下すよりも早く，簡単に証明を書くことができます．とはいえタクティクスタイルと項スタイルの間に明確な線引きは存在しません:上記の例の ``by rw [hk, mul_left_comm]`` のように，項スタイルの証明の途中にタクティクスタイルの証明を入れることが可能です．そして反対に，この後見ていくようにタクティクスタイルの証明中で短い項による証明を用いるのが便利なこともよくあります．とはいえ，本書ではタクティクの使用に重点を置くこととしています．
+証明を組み立てるうえで，細かいステップごとに段階的にフィードバックを受けられることは，非常に役に立ちます．このため，タクティクを使うと証明項を書き下すよりも早く，簡単に証明を書くことができます．とはいえタクティクスタイルと項スタイルの間に明確な線引きは存在しません:上記の例の ``by rw [hk, mul_add]`` のように，項スタイルの証明の途中にタクティクスタイルの証明を入れることが可能です．そして反対に，この後見ていくようにタクティクスタイルの証明中で短い項による証明を用いるのが便利なこともよくあります．とはいえ，本書ではタクティクの使用に重点を置くこととしています．
 
 TEXT. -/
 /- OMIT:

MIL/C02_Basics/S01_Calculating.lean

@@ -145,7 +145,7 @@ OMIT. -/
 
 .. index:: proof state, local context, goal
 
-カーソルがタクティクスタイルの証明の途中にあるとき，Lean は現在の証明の状態を **Lean infoview** ウィンドウに表示します．カーソルを動かすと，状態が変化するのがわかります．Leanの典型的な証明の状態は以下のようになります：
+カーソルがタクティクスタイルの証明の途中にあるとき，Lean は現在の証明の状態を **Lean Infoview** ウィンドウに表示します．カーソルを動かすと，状態が変化するのがわかります．Leanの典型的な証明の状態は以下のようになります：
 
 .. code-block::
 
@@ -570,7 +570,7 @@ occurrence of ``a + b`` with ``c``.
 OMIT. -/
 
 /- TEXT:
-``ring`` タクティクは ``Mathlib.Data.Real.Basic`` をインポートしたときに間接的にインポートされています．しかし，次章では実数以外の構造体の計算にも ``ring`` タクティクが使用できることを解説していきます． ``ring`` は ``import Mathlib.Tactic`` コマンドを使用して明示的にインポートすることができます．他の代数的対象にも同様のタクティクがあることを今後見ていきます． ``nth_rewrite`` と呼ばれる ``rw`` の亜種が存在し，それを使用するとゴール(証明したい命題)の中にある表現のうち特定のものだけを置換することができます．ありうる置換対象は1から順番に列挙されます．次の例では ``nth_rewrite 2 h`` は2番目に出現する ``a + b`` を ``c`` に置換しています．
+``ring`` タクティクは ``Mathlib.Data.Real.Basic`` をインポートしたときに間接的にインポートされています．しかし，次章では実数以外の構造体の計算にも ``ring`` タクティクが使用できることを解説していきます． ``ring`` は ``import Mathlib.Tactic`` コマンドを使用して明示的にインポートすることができます．他の代数的対象にも同様のタクティクがあることを今後見ていきます． ``nth_rw`` と呼ばれる ``rw`` の亜種が存在し，それを使用するとゴール(証明したい命題)の中にある表現のうち特定のものだけを置換することができます．ありうる置換対象は1から順番に列挙されます．次の例では ``nth_rw 2 h`` は2番目に出現する ``a + b`` を ``c`` に置換しています．
 
 EXAMPLES: -/
 -- QUOTE:

MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean

@@ -249,7 +249,7 @@ but for now we will stick to examples that don't require the case split.
 
 OMIT. -/
 /- TEXT:
-乗法が加法に対して分配法則を満たすように ``min`` 関数が ``max`` に対して分配法則を満たし，その逆も成り立つというのは興味深い事実です．言い換えれば，実数上において ``min a (max b c) ≤ max (min a b) (min a c)`` が成り立ち，この式の ``max`` と ``min`` を入れ替えた同様の式も成り立つということです．しかし次の節では， ``≤`` の推移性と反射性，そして上記で示した ``min`` と ``max`` を特徴付ける性質からこれが **成り立たない** ことを見ていきます．この性質を示すには実数上の関係 ``≤`` が **全順序** （total order）であること，つまり ``∀ x y, x ≤ y ∨ y ≤ x`` という性質が成り立つという事実を利用する必要があります．ここで記号 ``∨`` は選言記号で「または」を表します．最初のケースでは ``min x y = x`` となり，2番めのケースでは ``min x y = y`` となります．場合分けを使って証明する方法は :numref:`disjunction` で学びますが，現時点では場合分けをする必要のない例で説明します．
+乗法が加法に対して分配法則を満たすように ``min`` 関数が ``max`` に対して分配法則を満たし，その逆も成り立つというのは興味深い事実です．言い換えれば，実数上において ``min a (max b c) = max (min a b) (min a c)`` が成り立ち，この式の ``max`` と ``min`` を入れ替えた同様の式も成り立つということです．しかし次の節では， ``≤`` の推移性と反射性，そして上記で示した ``min`` と ``max`` を特徴付ける性質からこれが **成り立たない** ことを見ていきます．この性質を示すには実数上の関係 ``≤`` が **全順序** （total order）であること，つまり ``∀ x y, x ≤ y ∨ y ≤ x`` という性質が成り立つという事実を利用する必要があります．ここで記号 ``∨`` は選言記号で「または」を表します．最初のケースでは ``min x y = x`` となり，2番めのケースでは ``min x y = y`` となります．場合分けを使って証明する方法は :numref:`disjunction` で学びますが，現時点では場合分けをする必要のない例で説明します．
 
 TEXT. -/
 /- OMIT:
@@ -394,7 +394,7 @@ See if you can guess the names of the theorems
 you need to prove the following:
 OMIT. -/
 /- TEXT:
-最後の例では，指数が自然数であり ``dvd_mul_left`` を ``apply`` することでLeanに ``x^2`` の定義を ``x * x^1`` に展開させています．次の例を証明するのに必要な定理名を推測してみましょう:
+最後の例では，指数が自然数であり ``dvd_mul_left`` を ``apply`` することでLeanに ``x^2`` の定義を ``x^1 * x`` に展開させています．次の例を証明するのに必要な定理名を推測してみましょう:
 TEXT. -/
 -- QUOTE:
 -- BOTH:

MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean

@@ -29,7 +29,7 @@ like ``≤`` on the real numbers.
 Lean knows about partial orders:
 OMIT. -/
 /- TEXT:
-:numref:`proving_identities_in_algebraic_structures` では，実数上で成り立つ多くの一般的な恒等式が，可換環のようなより一般的な代数的構造のクラスでも成り立つことを確認しました．等式だけでなく，代数的構造を記述するために必要な公理はなんでも表現することができます．例えば **半順序** （partial order）は実数上の ``≤`` のような，集合上の反射的で推移的な二項関係のことです．Leanはこの半順序を表現できます:
+:numref:`proving_identities_in_algebraic_structures` では，実数上で成り立つ多くの一般的な恒等式が，可換環のようなより一般的な代数的構造のクラスでも成り立つことを確認しました．等式だけでなく，代数的構造を記述するために必要な公理はなんでも表現することができます．例えば **半順序** （partial order）は実数上の ``≤`` のような，集合上の反射的で推移的かつ反対称的な二項関係のことです．Leanはこの半順序を表現できます:
 TEXT. -/
 section
 -- QUOTE:

MIL/C04_Sets_and_Functions/S01_Sets.lean

@@ -439,7 +439,7 @@ and confirm that the proof still works.
 
 OMIT. -/
 /- TEXT:
-この証明を順を追って見て，何が起こっているのか理解してください．そして ``rw [evens, odds]`` の行を削除しても証明がまだ機能することを確認してください．
+この証明を順を追って見て，何が起こっているのか理解してください．ここでゴールにある ``¬ Even n`` を保持するために，単純化器に ``Nat.not_even_iff`` を **使わない** よう指示していることに注意してください．そして ``rw [evens, odds]`` の行を削除しても証明がまだ機能することを確認してください．
 
 TEXT. -/
 /- OMIT:

MIL/C04_Sets_and_Functions/S02_Functions.lean

@@ -660,7 +660,7 @@ meets the first part of this specification.
 
 OMIT. -/
 /- TEXT:
-``noncomputable section`` と ``open Classical`` の行は古典論理を本質的な意味で使っているため必要です．入力 ``y`` に対して，関数 ``inverse f`` は ``f x = y`` を満たす ``x`` の値があればそれを返し，なければ ``α`` のデフォルトの要素を返します．これは **依存的なif** （dependent if）による構成の例になっています．というのも条件が真の場合，返される値 ``Classical.choose h`` は仮定 ``h`` に依存するからです．条件式 ``if h : e then a else b`` は，等式 ``dif_pos h`` によって ``h : e`` が与えられると ``a`` に書き換えられ，同様に ``dif_neg h`` によって ``h : ¬ e`` が与えられると ``b`` に書き換えられます．定理 ``inverse_spec`` は ``inverse f`` が if 式の条件を満たすことを述べています．
+``noncomputable section`` と ``open Classical`` の行は古典論理を本質的な意味で使っているため必要です．入力 ``y`` に対して，関数 ``inverse f`` は ``f x = y`` を満たす ``x`` の値があればそれを返し，なければ ``α`` のデフォルトの要素を返します．これは **依存的なif** （dependent if）による構成の例になっています．というのも条件が真の場合，返される値 ``Classical.choose h`` は仮定 ``h`` に依存するからです．条件式 ``if h : e then a else b`` は，等式 ``dif_pos h`` によって ``h : e`` が与えられると ``a`` に書き換えられ，同様に ``dif_neg h`` によって ``h : ¬ e`` が与えられると ``b`` に書き換えられます．また似たものとして ``if_pos`` と ``if_neg`` というものもあり，これは非依存なifの構成で機能し，これは次節で用いられます．定理 ``inverse_spec`` は ``inverse f`` が if 式の条件を満たすことを述べています．
 
 TEXT. -/
 /- OMIT:

MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean

@@ -268,7 +268,7 @@ Notice that rewriting with ``sbAux`` here replaces ``sbAux f g 0``
 with the right-hand side of the corresponding defining equation.
 OMIT. -/
 /- TEXT:
-以下の証明を見て，大筋をつかめたら残りの部分を埋めてみてください．最後に ``inv_fun_eq`` を使う必要があります．ここで ``sb_aux`` を使って書き直すと ``sb_aux f g 0`` が対応する定義している等式の右辺に置き換わることに注意しましょう．
+以下の証明を見て，大筋をつかめたら残りの部分を埋めてみてください．最後に ``invFun_eq`` を使う必要があります．ここで ``sbAux`` を使って書き直すと ``sbAux f g 0`` が対応する定義している等式の右辺に置き換わることに注意しましょう．
 BOTH: -/
 -- QUOTE:
 theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by
@@ -390,7 +390,7 @@ and more readable, but they sometimes require us to do more work.
 
 OMIT. -/
 /- TEXT:
-この証明ではいくつか新しいタクティクを導入しています．まず ``set`` タクティクに注目します．これは ``sb_set f g`` と ``sb_fun f g`` に対してそれぞれ ``A`` と ``h`` という略語を導入するものです．またこの対応を定義する等式に ``A_def`` と ``h_def`` と名付けています．この省略は定義的なものであり，Leanは必要に応じて自動的に省略形を展開することがあります．しかし常に行われるわけではありません．例えば， ``rw`` を使用する場合，一般的には ``A_def`` と ``h_def`` を明示的に使用する必要があります．つまり，定義はトレードオフの関係にあるのです．式をより短く読みやすくすることができますが，時にはより多くの作業が必要に成ります．
+この証明ではいくつか新しいタクティクを導入しています．まず ``set`` タクティクに注目します．これは ``sbSet f g`` と ``sb_fun f g`` に対してそれぞれ ``A`` と ``h`` という略語を導入するものです．またこの対応を定義する等式に ``A_def`` と ``h_def`` と名付けています．この省略は定義的なものであり，Leanは必要に応じて自動的に省略形を展開することがあります．しかし常に行われるわけではありません．例えば， ``rw`` を使用する場合，一般的には ``A_def`` と ``h_def`` を明示的に使用する必要があります．つまり，定義はトレードオフの関係にあるのです．式をより短く読みやすくすることができますが，時にはより多くの作業が必要に成ります．
 
 TEXT. -/
 /- OMIT: