From e874a976cd5dfdf9c86eb6b5607b8dcbcda6c79c Mon Sep 17 00:00:00 2001
From: Kitamado <47292598+Seasawher@users.noreply.github.com>
Date: Sat, 23 May 2026 00:16:43 +0900
Subject: [PATCH] =?UTF-8?q?rcases=20=E3=81=AE=20rfl=20=E3=83=91=E3=82=BF?=
 =?UTF-8?q?=E3=83=BC=E3=83=B3=E3=82=92=E7=B4=B9=E4=BB=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Tactic/Rcases.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/LeanByExample/Tactic/Rcases.lean b/LeanByExample/Tactic/Rcases.lean
index d7438d78..1d236e1b 100644
--- a/LeanByExample/Tactic/Rcases.lean
+++ b/LeanByExample/Tactic/Rcases.lean
@@ -44,3 +44,17 @@ example (s : Sample) : True := by
     guard_hyp z : String
 
     trivial
+
+/- ## 等式を rfl で分解する
+
+`rcases` のパターンには `rfl` も使えます。等式の仮定 `h : a = b` に対して `rcases h with rfl` と書くと、`a` と `b` が同じ値である場合に分解されます。-/
+
+example {a b c : Nat} (h : a = b) : a + c = b + c := by
+  rcases h with rfl
+  rfl
+
+/- `rfl` は、ほかの `rcases` パターンの中にも書くことができます。たとえば、論理積を分解しながら、片方の等式を同時に消去できます。-/
+
+example {a b : Nat} (h : a = b ∧ b = 3) : a = 3 := by
+  rcases h with ⟨rfl, hb⟩
+  exact hb