rfl の説明を修正

「定義から等しいものを示す」ではなく，「反射性を示す」という説明にする

Examples.lean

@@ -21,7 +21,8 @@ import Examples.LeftRight
 import Examples.Linarith
 import Examples.Refine
 import Examples.Rel
-import Examples.Rfl
+import Examples.Rfl.Refl
+import Examples.Rfl.Rfl
 import Examples.Ring
 import Examples.Rw
 import Examples.Show

Examples/Rfl.lean → Examples/Rfl/Refl.lean

@@ -4,4 +4,4 @@ example : 1 + 1 = 2 := by rfl
 -- 変数を含む等式
 example (x : Nat) : x = x := by rfl
 
-example (P : Prop) : P = P := by rfl
+example (P : Prop) : P = P := by rfl

Examples/Rfl/Rfl.lean

@@ -0,0 +1,18 @@
+import Mathlib.Tactic.Relation.Rfl
+
+-- `n ≤ n` を示すために必要
+import Mathlib.Data.Nat.Basic
+
+-- ANCHOR: first
+inductive MyEq {α : Type u} : α → α → Prop
+  | refl (a : α) : MyEq a a
+
+attribute [refl] MyEq.refl
+
+example (n : ℕ) : MyEq n n := by rfl
+-- ANCHOR_END: first
+
+-- ANCHOR: nat
+-- `import Mathlib.Data.Nat.Basic` が必要
+example (n : Nat) : n ≤ n := by rfl
+-- ANCHOR_END: nat

src/SUMMARY.md

@@ -31,7 +31,7 @@
 - [push_neg: ドモルガン](./push_neg.md)
 - [refine: プレースホルダを使う](./refine.md)
 - [rel: 不等式を使う](./rel.md)
-- [rfl: 定義そのまま](./rfl.md)
+- [rfl: 関係の反射性を示す](./rfl.md)
 - [ring: 環の等式を示す](./ring.md)
 - [rw: 同値変形](./rw.md)
 - [show: 示すべきことを宣言](./show.md)

src/rfl.md

@@ -1,9 +1,32 @@
 # rfl
 
+needs: `import Mathlib.Tactic.Relation.Rfl`
+
 named after: 反射律(reflexivity)
 
-`rfl` は，定義から等しいものが等しいことを示すタクティクです．
+`rfl` は，`refl attribute` の付けられた定理を用いて関係の反射性を示すタクティクです．
+
+```lean
+{{#include ../Examples/Rfl/Rfl.lean:first}}
+```
+
+`@[refl]` で登録された定理を用いるので，追加でライブラリを import することにより示すことができる命題が増えます．
+
+```lean
+{{#include ../Examples/Rfl/Rfl.lean:nat}}
+```
+
+## 補足
+
+実は `Mathlib.Tactic.Relation.Rfl` を import するかどうかにより，内部で呼び出されるタクティクが変わります．
+
+* `Mathlib.Tactic.Relation.Rfl` ありなら [Lean.MVarId.rfl](https://leanprover-community.github.io/mathlib4_docs//Mathlib/Tactic/Relation/Rfl.html#Lean.MVarId.rfl) が，
+* なしなら [Lean.MVarId.refl](https://leanprover-community.github.io/mathlib4_docs//Lean/Meta/Tactic/Refl.html#Lean.MVarId.refl) が
+
+それぞれ参照されます．後者は `@[refl]` が付けられた一般の関係の反射性にアクセスできず，等号 `=` の反射性しか使うことができません．
+
+後者の場合 `rfl` は，単に定義から等しいものが等しいことを示すタクティクになります．
 
 ```lean
-{{#include ../Examples/Rfl.lean}}
-```
+{{#include ../Examples/Rfl/Refl.lean}}
+```