rel のコード例をそのまま実行できる形式に修正

Examples/Rel.lean

@@ -2,13 +2,34 @@ import Mathlib.Tactic.GCongr
 
 variable (a b c d: Nat)
 
--- ANCHOR: first
+/-! ## rel -/
+
+-- 不等式を示す例
 example (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by
   rel [h1, h2]
--- ANCHOR_END: first
 
+-- 下記で示すように，ゴールが関係式でないときにはエラーになる
+
+/-- error: rel failed, goal not a relation -/
+#guard_msgs in
+  example (x : Nat) : Nat := by rel [x]
+
+/-! ## gcongr -/
+
+example (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by
+  -- `gcongr` でも示すことができる
+  gcongr
+
+/-!
+  ## rel の推論
+
+  `rel` は，たとえば整数 `x: Int` に対して `0 ≤ x ^ 2` であることを
+  自動的に適用するなど, 多少の推論を行います．
+-/
 
--- ANCHOR: guess
 example (x: Int) (h1 : a ≤ b) : x ^ 2 * a ≤ x ^ 2 * b := by
   rel [h1]
--- ANCHOR_END: guess
+
+example (x: Int) (h1 : a ≤ b) : x ^ 2 * a ≤ x ^ 2 * b := by
+  -- これも `gcongr` で示すことができる
+  gcongr

src/rel.md

@@ -1,17 +1,11 @@
 # rel
 
-needs: `import Mathlib.Tactic.GCongr`
-
 named after: 関係(relation)
 
-`rel` は，不等式を代入して適用し，不等式を示します．
-
-```lean
-{{#include ../Examples/Rel.lean:first}}
-```
+`rel` は，一般化された合同性を用いてゴールを分解し，命題を代入することで示すタクティクです．ゴールが関係(relation)について述べているときに使用できます．
 
-`rel` は，たとえば整数 `x: Int` に対して `0 ≤ x ^ 2` であることを自動的に適用するなど, 多少の推論を行います．
+典型的には不等式を代入して適用し，不等式を示します．
 
 ```lean
-{{#include ../Examples/Rel.lean:guess}}
+{{#include ../Examples/Rel.lean}}
 ```