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

Examples/Congr.lean

@@ -1,25 +1,36 @@
 import Mathlib.Algebra.Group.Defs -- `add_zero` を使用するため
 
-variable (X : Type)
+variable (X : Type) (f : Int → Int)
 
--- ANCHOR: first
-example (f : Int → X) (h : x = 0) : f (2 + x) = f 2 := by
+/-! ## congr -/
+
+example (h : x = 0) : f (2 + x) = f 2 := by
   congr
   show 2 + x = 2
 
   simp only [h, add_zero]
--- ANCHOR_END: first
 
+/-! ## congr の再帰の深さを調節する -/
+
+example (g : Int → X) (h : x = 0) (hf : ∀ x, f x = f (- x)) :
+    g (f (2 + x)) = g (f (- 2)) := by
+
+  -- congr の再帰がアグレッシブすぎて上手くいかないことがある
+  try (
+    congr
 
--- ANCHOR: option
-example (f : Int → Int) (g : Int → X) (h : x = 0)
-  (hf : ∀ x, f x = f (- x)) : g (f (2 + x)) = g (f (- 2)) := by
-  -- 仮に `congr` とすると
-  -- ゴールが `⊢ 2 + x = -2` になってしまう
+    -- 分解しすぎた
+    show 2 + x = -2
 
+    -- これでは示すことができない
+    fail
+  )
+
+  -- 再帰の深さを数値として指定できる
   congr 1
+
+  -- ちょうどよい分解になった
   show f (2 + x) = f (-2)
 
   simp only [h, add_zero]
   exact hf _
--- ANCHOR_END: option

src/congr.md

@@ -2,14 +2,10 @@
 
 named after: 合同(congruence)
 
-`congr` は，`⊢ f as = f bs` という形のゴールがあったときに，ゴールを `⊢ as = bs` に変えます．再帰的に適用されるので，`⊢ g (f as) = g (f bs)` という形のゴールでも同じ結果になります．
-
-```lean
-{{#include ../Examples/Congr.lean:first}}
-```
+`congr` は，`⊢ f as = f bs` という形のゴールがあったときに，ゴールを `⊢ as = bs` に変えます．再帰的に適用されるので，`⊢ g (f as) = g (f bs)` という形のゴールでも `⊢ as = bs` というゴールになります．
 
 `congr` が適用される再帰の深さを引数として渡すことができます．これは，主に単に `congr` とするだけだと「行き過ぎ」になるときに調整する目的で使用されます．
 
 ```lean
-{{#include ../Examples/Congr.lean:option}}
+{{#include ../Examples/Congr.lean}}
 ```