rfl パターンによる自動書き換え

1. rfl パターンによる自動書き換え

存在記号 ∃ x, y = f x ∧ P x のような形を分解する際、rfl をパターンに入れると、その瞬間に「$y$ を $f(x)$ に置き換える」処理が走ります。

-- y ∈ f '' s の定義は ∃ x, x ∈ s ∧ f x = y
-- これを rintro ⟨x, xs, rfl⟩ で分解すると：
-- 1. 存在記号から x を取り出す
-- 2. xs : x ∈ s を取り出す
-- 3. f x = y という等式を使って、ゴールや他の仮定内の y をすべて f x に置換する
rintro ⟨x, xs, rfl⟩

これにより、後続のステップで rw [h_eq] at ... と書く手間が省けます。

2. 構造分解と再構築 (⟨ ⟩ と |)

等式と論理和（∨）が組み合わさった複雑な仮定も、一行で仕分けられます。

-- 仮定 h : y ∈ f '' (s ∪ t)
-- 分解: ∃ x, (x ∈ s ∨ x ∈ t) ∧ f x = y
rintro ⟨x, xs | xt, rfl⟩
· -- ケース1: x ∈ s かつ y = f x
· -- ケース2: x ∈ t かつ y = f x

このとき、各ケースの内部ではすでに y が f x に書き換わった状態からスタートできます。

3. 匿名コンストラクタによる「逆」の書き換え

ゴールが ∃（存在）や ∧（かつ）の場合、use を使わずに ⟨ ⟩ で直接「証拠」を並べて解決できます。

-- ゴール ⊢ ∃ x, P x ∧ f x = y
-- x という値と、P x の証明 hP、そして f x = y の証明 (rfl) を一気に渡す
exact ⟨x, hP, rfl⟩

ここで rfl を渡しているのは、ゴールにある f x = y という等式が、定義的に（あるいは代入によって）f x = f x となっている場合に「それは自明（等しい）」と宣言するためです。

---

書き換えパターンの比較表

タクティック	通常の書き方	パターンを使った書き方	メリット
分解	rcases h with ⟨x, hx, hy⟩, rw [hy] at *	rcases h with ⟨x, hx, rfl⟩	変数の数が減り、ゴールが整理される
分岐	cases h, case inl h1 => ...	`rcases h with h1	h2`
構築	use x, constructor, exact h1, rfl	exact ⟨x, h1, rfl⟩	1行で証明が完結する

操作	逆像 ($f^{-1}$) との相性	順像 ($f ”$) との相性
和集合 ($\cup$)	最高 (常に保存)	最高 (常に保存)
共通部分 ($\cap$)	最高 (常に保存)	条件付 (単射なら保存)
差集合 ($\setminus$)	最高 (常に保存)	条件付 (単射なら保存)
補集合 ($^c$)	最高 (常に保存)	困難 (一筋縄ではいかない)