目次のネストを1段階に固定する

Examples/Command/Attribute/CasesEliminator.lean → Examples/Attribute/CasesEliminator.lean

@@ -1,8 +1,8 @@
 /- # cases_eliminator
 
-`[cases_eliminator]` 属性は、[`cases`](../../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。
+`[cases_eliminator]` 属性は、[`cases`](../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。
 
-より詳しくいうと、[`cases`](../../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`cases`](../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace CasesEliminator --#
 
@@ -63,7 +63,7 @@ example (x : Many α) : True := by
   case none => trivial
   case more x => trivial
 
-/- なお [`rcases`](../../Tactic/Rcases.md) には影響しません。 -/
+/- なお [`rcases`](../Tactic/Rcases.md) には影響しません。 -/
 
 example (xs : Many α) : True := by
   rcases xs with _ | _

Examples/Command/Attribute/InductionEliminator.lean → Examples/Attribute/InductionEliminator.lean

@@ -2,7 +2,7 @@
 
 `[induction_eliminator]` 属性は、帰納法の枝を変更することを可能にします。
 
-より詳しくいうと、[`induction`](../../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`induction`](../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace InductionEliminator --#
 

Examples/Command/Attribute/Simps.lean → Examples/Attribute/Simps.lean

@@ -1,6 +1,6 @@
 /- # simps
 
-補題を [`simp`](../../Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
+補題を [`simp`](../Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
 
 例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
 -/

Examples/Command/Declarative/AddAesopRules.lean → Examples/Declarative/AddAesopRules.lean

@@ -1,5 +1,5 @@
 /- # add_aesop_rules
-`add_aesop_rules` は [`aesop`](../../Tactic/Aesop.md) タクティクに追加のルールを登録するためのコマンドです。-/
+`add_aesop_rules` は [`aesop`](../Tactic/Aesop.md) タクティクに追加のルールを登録するためのコマンドです。-/
 import Aesop
 
 /-- 自然数 n が正の数であることを表す命題 -/

Examples/Command/Declarative/Axiom.lean → Examples/Declarative/Axiom.lean

@@ -253,7 +253,7 @@ variable {p : α → Prop}
 #check (Classical.choose_spec : (h : ∃ x, p x) → p (Classical.choose h))
 
 /- #### なぜ証明無関係と矛盾しないのか
-[証明無関係](../../Term/Type/Prop.md#ProofIrrel)の節で詳しく述べているように、存在命題は「何かがある」としか主張しておらず、具体的な項を復元するのに必要な情報を持っていません。したがって存在が主張されている項を取り出して関数の返り値にすることはできないはずですが、選択原理を使うと存在命題から具体的な項が得られてしまいます。これが矛盾を生まないのはなぜでしょうか？
+[証明無関係](../Type/Prop.md#ProofIrrel)の節で詳しく述べているように、存在命題は「何かがある」としか主張しておらず、具体的な項を復元するのに必要な情報を持っていません。したがって存在が主張されている項を取り出して関数の返り値にすることはできないはずですが、選択原理を使うと存在命題から具体的な項が得られてしまいます。これが矛盾を生まないのはなぜでしょうか？
 
 答えは、選択原理は証明方法が異なる証明項であっても、同じ命題であれば一様に同じ項を返すからです。以下の例では、「証拠」が異なるような存在命題の証明項を２つ与えていますが、そこから選択される項は同じです。つまり、選択原理は同値な存在命題すべてに対して一斉に同じ項を取り出す方法があると主張しているのであって、「存在が主張されている項を取り出して関数の返り値にする」ことができるとまでは主張していないのです。-/
 

Examples/Command/Declarative/Noncomputable.lean → Examples/Declarative/Noncomputable.lean

@@ -3,7 +3,7 @@
 
 Lean は、[`def`](./Def.md) で定義された関数はすべて計算可能であると想定しています。したがって、計算可能でない関数を定義すると、エラーが発生します。
 
-計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](./Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](../../Term/Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。
+計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](./Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](../Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。
 -/
 
 variable {X Y : Type}

Examples/Command/Declarative/Private.lean → Examples/Declarative/Private.lean

@@ -3,7 +3,7 @@
 
 不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。
 -/
-import Examples.Command.Declarative.Protected -- protected のページをインポート
+import Examples.Declarative.Protected -- protected のページをインポート
 import Lean
 namespace Private --#
 

Examples/Command/Diagnostic/Eval.lean → Examples/Diagnostic/Eval.lean

@@ -49,7 +49,7 @@ failed to be synthesized, this instance instructs Lean on how to display the res
 -/
 #guard_msgs in #eval (fun x => x + 1)
 
-/- 一般に、[`Repr`](../../Term/TypeClass/Repr.md) や [`ToString`](../../Term/TypeClass/ToString.md) のインスタンスでないような型の項は `#eval` に渡すことができません。-/
+/- 一般に、[`Repr`](../TypeClass/Repr.md) や [`ToString`](../TypeClass/ToString.md) のインスタンスでないような型の項は `#eval` に渡すことができません。-/
 
 /-! ## 例外処理の慣例
 Lean および Mathlib では、「関数ではなく定理に制約を付ける」ことが慣例です。

Examples/Command/Diagnostic/Guard.lean → Examples/Diagnostic/Guard.lean

@@ -34,7 +34,7 @@ error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains error
 #guard_msgs (whitespace := lax) in
 #guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)
 
-/-! しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../../Term/TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
+/-! しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
 
 -- 型は Prop
 /-- info: 1 + 1 = 2 : Prop -/

Examples/Solution/HeytingAndBooleanAlgebra.lean

@@ -136,7 +136,7 @@ end HeytingAlgebra
 
 しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。
 
-こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Command/Declarative/AddAesopRules.md) の記事が参考になると思います。
+こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Declarative/AddAesopRules.md) の記事が参考になると思います。
 
 ### 問1.1 半順序集合であること
 -/

Examples/Tactic/Aesop.lean

@@ -61,7 +61,7 @@ attribute [aesop safe constructors] Pos
 -- `aesop` で証明できるようになった！
 example : Pos 1 := by aesop
 
-/- 上記の例のように `[aesop]` 属性によってルールを追加することもできますし、[`add_aesop_rules`](../Command/Declarative/AddAesopRules.md) というコマンドでルールを追加することもできます。-/
+/- 上記の例のように `[aesop]` 属性によってルールを追加することもできますし、[`add_aesop_rules`](../Declarative/AddAesopRules.md) というコマンドでルールを追加することもできます。-/
 
 example (n : Nat) (h : Pos n) : 0 < n := by
   -- ルールが足りないので、`aesop` で示すことはできない

Examples/Tactic/Choose.lean

@@ -13,7 +13,7 @@ theorem choice (h : ∀ x, ∃ y, P x y) : ∃ f : X → Y, ∀ x, P x (f x) :=
   exact ⟨f, hf⟩
 
 /- ## 舞台裏
-`choose` は裏で選択原理 [`Classical.choice`](../Command/Declarative/Axiom.md#ClassicalChoice) を使用しています。
+`choose` は裏で選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を使用しています。
 -/
 
 /-- info: 'choice' depends on axioms: [Classical.choice] -/

Examples/Tactic/Decide.lean

@@ -1,7 +1,7 @@
 /- # decide
 `decide` は、決定可能な命題を示すタクティクです。
 
-命題 `P : Prop` が決定可能であるとは、型クラス [`Decidable`](../Term/TypeClass/Decidable.md) のインスタンスであることを意味します。`P` が `Decidable` のインスタンスであるとき、`decide` 関数を適用することにより `decide P : Bool` が得られるので、これを呼び出すことによって証明したり反証したりすることができます。つまり一言でいえば、決定可能であるとは決定するためのアルゴリズムが存在するということです。
+命題 `P : Prop` が決定可能であるとは、型クラス [`Decidable`](../TypeClass/Decidable.md) のインスタンスであることを意味します。`P` が `Decidable` のインスタンスであるとき、`decide` 関数を適用することにより `decide P : Bool` が得られるので、これを呼び出すことによって証明したり反証したりすることができます。つまり一言でいえば、決定可能であるとは決定するためのアルゴリズムが存在するということです。
 -/
 -- 決定可能な命題を決定する関数 decide が存在する
 #check (decide : (P : Prop) → [Decidable P] → Bool)

Examples/Tactic/Exact.lean

@@ -16,7 +16,7 @@ example (hP : P) (hQ : Q) : P ∧ Q := by
 
 example (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ
 
-/-! なお `And` は構造体なので[無名コンストラクタ](../Command/Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/
+/-! なお `And` は構造体なので[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/
 
 example (hP : P) (hQ : Q) : P ∧ Q := ⟨hP, hQ⟩
 

Examples/Tactic/Exists.lean

@@ -27,7 +27,7 @@ Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
 -- このとき `w : α` と `h : p w` が与えられたとき `∃ x : α, p x` が成り立つ。
 #check (Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α) (h : p w), Exists p)
 
-/- したがって `Exists` は単一のコンストラクタを持つ帰納型、つまり構造体なので、上記の `exists` は `exact` と[無名コンストラクタ](../Command/Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
+/- したがって `Exists` は単一のコンストラクタを持つ帰納型、つまり構造体なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exact ⟨2, show 3 * 2 + 1 = 7 from by rfl⟩

Examples/Tactic/Have.lean

@@ -25,7 +25,7 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
 
 `P` の証明 `hp : P` と `Q` の証明 `hq : Q` があるとき、`P ∧ Q` の証明は `And.intro hp hq` で構成できます。ここで `And.intro` は構造体 `And` 型のコンストラクタです。
 
-これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](../Command/Declarative/Structure.md#AnonymousConstructor)と呼ばれるもので、`And` に限らず任意の構造体に使用することができます。-/
+これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)と呼ばれるもので、`And` に限らず任意の構造体に使用することができます。-/
 variable (hp : P) (hq : Q)
 
 def hpq : P ∧ Q := ⟨hp, hq⟩

Examples/Tactic/Intro.lean

@@ -28,7 +28,7 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
 /- ## 特定の形の命題に対しての使用法
 
 ### A ∧ B → C
-前提が論理積の形をしていた場合、[無名コンストラクタ](../Command/Declarative/Structure.md#AnonymousConstructor)で仮定を分解することができます。
+前提が論理積の形をしていた場合、[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で仮定を分解することができます。
 -/
 
 example {S : Prop} (hPR : P → R) (hQR : Q → S) : P ∧ Q → R ∧ S := by

Examples/Tactic/Itauto.lean

@@ -2,7 +2,7 @@
 # itauto
 `itauto` は、直観主義論理(intuitionistic logic)の範囲内でトートロジー(tautology)を証明します。
 
-命題論理を扱うタクティクには他にも [`tauto`](./Tauto.md) がありますが、あちらは選択原理 [`Classical.choice`](../Command/Declarative/Axiom.md#ClassicalChoice) を勝手に使用することがあります。なお選択原理は Lean が標準で用意している公理のひとつで、排中律 `P ∨ ¬ P` や二重否定の除去 `¬ ¬ P → P` を示すのに必要です。
+命題論理を扱うタクティクには他にも [`tauto`](./Tauto.md) がありますが、あちらは選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を勝手に使用することがあります。なお選択原理は Lean が標準で用意している公理のひとつで、排中律 `P ∨ ¬ P` や二重否定の除去 `¬ ¬ P → P` を示すのに必要です。
 -/
 import Mathlib.Tactic.ITauto
 import Mathlib.Tactic.Tauto

Examples/Term/Type/Prop.lean → Examples/Type/Prop.lean

@@ -99,15 +99,15 @@ namespace Proposition --#
 -- 各命題の証明項はただ一つしかない
 theorem proof_irrel (P : Prop) (h1 h2 : P) : h1 = h2 := rfl
 
-/- 証明無関係は [`axiom`](../../Command/Declarative/Axiom.md) で導入された公理から従う定理ではなく、Lean の型システムに組み込まれたものであることに注意してください。-/
+/- 証明無関係は [`axiom`](../Declarative/Axiom.md) で導入された公理から従う定理ではなく、Lean の型システムに組み込まれたものであることに注意してください。-/
 
 /-- info: 'Proposition.proof_irrel' does not depend on any axioms -/
 #guard_msgs in #print axioms proof_irrel
 
 /- ### No Large Elimination
 証明無関係の重要な帰結のひとつに、「証明から値を取り出すことができるのは、証明の中だけ」というものがあります。この現象は、「`Prop` は large elimination を許可しない」という言葉で表現されることがあります。
 
-たとえば次のように、証明の中であれば証明項を [`cases`](../../Tactic/Cases.md) や [`rcases`](../../Tactic/Rcases.md) で分解して値を取り出すことができます。-/
+たとえば次のように、証明の中であれば証明項を [`cases`](../Tactic/Cases.md) や [`rcases`](../Tactic/Rcases.md) で分解して値を取り出すことができます。-/
 
 -- 同じ存在命題の２通りの証明
 -- 2乗すると1になる整数を２通り与えた