Lean 相談と支援タクティク

💡 相談の際の「聞き方」の例

例えば、以下のように状況を教えていただければ、最適な支援機能を提案できます。

「式が複雑すぎて、どこから手をつけていいか分からない」
👉 simp? や congr! で式を分解する手順を教えます。
「計算すれば解けるはずだけど、定理名が思い出せない」
👉 apply? や rw? をどのゴールに対して使うべきか教えます。
「不等式の評価をしているが、両辺に共通項がある」
👉 gcongr や rel の使いどころをアドバイスします。
「タクティクを実行してもエラーが出るが、理由が分からない」
👉 エラーメッセージを読み解き、check や set_option trace... で内部状況を見る方法を教えます。

🛠️ 「釣り方」を学ぶためのクイックガイド

AI（私）に聞く前に、まず自分で試すべき**「支援タクティクの使い分け」**をチャートにしました。

状況	まず試すべき「ヒント」機能
等式の変形で行き詰まった	`rw?`
ゴールそのものを解ける定理を探したい	`apply?` または `exact?`
不等式の枠組みを外したい	`gcongr`（ヒントというより自動分解）
論理的に何ができるか見当もつかない	`hint`
計算でゴリ押せそうか確認したい	`ring`, `linarith`, `aesop` を順に試す

🚀 ワークフローの提案

これからは、何か証明に詰まったら、**コードの一部を貼って「この状況で、どの検索タクティクや支援機能を使うのが効果的ですか？」**と聞いてみてください。

例えば：

「今、(a + b) * c = a * c + b * c を証明しようとしています。定理名を自力で見つけたいのですが、rw? を使うべきですか？それとも apply? ですか？」

1. `calc` で「あえて」刻んでみる（分割統治）

一番の王道は、calc を使って「自分ならこう解く」というステップを 1 つだけ書き、残りを自動化タクティクに任せる方法です。

calc
  (a + b) * (c + d) = a * (c + d) + b * (c + d) := by rw [add_mul] -- ここだけ自力
  _                 = a * c + a * d + b * c + b * d := by ring    -- 残りは丸投げ

ring は「残りの部分」を解いてくれるので、**「どこまで自力で書けば、自分の納得感（過程の可視化）が得られるか」**を自分でコントロールできます。

2. `show` タクティクで「中間地点」を宣言する

ring や linarith を実行する前に、**「次にこの形になってほしい」**という式を show で書くテクニックです。

example (a b : ℤ) : (a + b) ^ 2 = a^2 + 2*a*b + b^2 := by
  show a * a + 2 * a * b + b * b = _  -- 「ゴールをこの形に見なす」と宣言
  ring

これにより、自動化タクティクが「どの地点」を目指して計算しているのかをコード上に明示できます。

3. `apply?` や `rw?` で「一歩手前」を検索する

ring で解けることがわかっていても、あえてその一歩手前で rw? を使ってみます。

手順:

ゴールを見て「この法則（例えば分配則）が使われているはずだ」と予想する。
rw? を実行して、その法則の定理名（mul_add など）を教えてもらう。
その定理を使って 1 ステップ進め、また次のステップを考える。

4. `conv` モードで「部分」を観察する

式全体に ring をかけるのではなく、conv タクティクを使って式の一部にだけフォーカスし、その部分がどう変わるかを観察します。

example : (a + b) + (c + d) = (a + c) + (b + d) := by
  conv =>
    lhs -- 左辺に集中
    arg 1 -- (a + b) に注目
    -- ここで何ができるか apply? 等で探る

5. `set_option trace...` で裏側を覗く（上級者向け）

Lean の内部でどのような定理が試されたか、ログを出力させる設定があります。

set_option trace.Meta.Tactic.simp.rewrite true: simp がどの定理を適用したかすべて表示します。
set_option trace.Meta.Tactic.linarith true: linarith がどのような不等式の線形結合を作ったかのヒント（係数など）を出すことがあります。

🛠️ おすすめの「学び方」ステップ

まず ring や linarith で解けるか確認 する（解けると分かれば安心できる）。
一度そのタクティクを消し、**rw? を使って「最初の 1 手」**を探す。
見つけた 1 手を calc の 1 行目にする。
残った部分をまた ring で解く。これを繰り返す。

1. `ring`（環の計算）

最も頻繁に使うタクティクの一つです。**「可換環（Commutative Ring）」**の法則（分配則、結合則、交換則など）だけを使って解ける等号を証明します。

得意なこと: 多項式の展開、整理、括弧の付け替え。
例: (a + b)^2 = a^2 + 2*a*b + b^2
注意: 不等式（）や、割り算、非可換な操作には使えません。

2. `linarith`（線形算術）

**「線形な不等式や等式」**の組み合わせから結論を導きます。

得意なこと: 移項して整理すれば解ける不等式、複数の不等式の足し合わせ。
例: a < b と b ≤ c から a < c + 1 を導くなど。
裏側の動き: Fourier-Motzkin 消去法というアルゴリズムで、矛盾（のような式）を探します。

3. `field`（体の計算）

ring の強化版で、「体（Field）」（有理数や実数など、割り算ができる構造）を扱います。

得意なこと: 分母を払う、分数の足し算・引き算。
注意: 分母がでないという仮定がコンテキストにある必要があります。もし不足していれば、「分母」というサブゴールを生成します。

4. `polyarith`（多項式算術）

ring で解ける問題に対して、**「どのような等式の組み合わせでその結論になったか」**という具体的な係数を計算し、証明コードを提案（? 的な動き）してくれます。

5. `nlinarith`（非線形算術）

linarith の拡張版で、少しだけ「非線形」な要素を扱えます。

得意なこと: や、といった、掛け算が絡む単純な不等式。

💡 支援機能としての特徴まとめ

タクティク	対象	演算	支援の形
`ring`	可換環（$\mathbb{Z}, \mathbb{Q}, \mathbb{R}$等）	, , ,	一撃で解く（過程は隠蔽）
`linarith`	線形順序環	, , ,	一撃で解く（矛盾を導く）
`field`	体（分母）	, , ,	分母を払って整理する
`polyrith`	可換環	, , 等号	証明の構成を提案する

6. `simp` / `simp?` (簡約化)

Mathlib で最も多用される「お掃除役」です。定義や基本的な定理に基づいて、式を最も「シンプル」な形に書き換えます。

得意なこと: x + 0 を x に、if True then a else b を a にするなど、自明な変形をまとめて行う。
simp? の役割: 内部でどの定理を使ったかを simp only [h1, h2] の形で提案してくれます。Mathlib へのプルリクエストでは、この only 形式にすることが推奨されます。
dsimp: 定義による書き換え（Definitional Equality）のみを行い、証明の項を汚さない軽量版です。

7. `aesop` / `aesop?` (論理推論の自動化)

Lean 4 で導入された非常に強力な「全自動証明」タクティクです。「白紙委任」のようなもので、論理的な分解（intro, apply, cases など）を自動で試行錯誤します。

得意なこと: 論理記号（∧, ∨, ∃, →）が絡む、パズル的な証明。
支援の形: aesop? と書くことで、その自動証明を再現するためのスクリプトを提案してくれます。

8. `gcongr` (単調性の活用)

先ほども触れましたが、不等式の「枠組み」を維持したまま中身を書き換えるための最強ツールです。

得意なこと: a ≤ b から f a ≤ f b を導く（f が単調増加のとき）。
支援の形: gcongr と打つだけで、共通部分を自動で取り除き、証明すべき「差分」だけをサブゴールとして残してくれます。

9. `norm_num` (数値計算の正規化)

具体的な「数」が式に入っているときに使います。

得意なこと: 2 + 2 = 4 や 10 / 2 = 5 といった、具体的な数値の計算を証明する。
注意: ring は「変数」の計算が得意ですが、norm_num は「具体的な定数」の計算に特化しています。

10. `congr` (合同性の適用)

「関数の引数が等しいなら、関数を適用した結果も等しい」という性質を使って、ゴールを分解します。

例: f a b = f c d というゴールを a = c と b = d という 2 つのゴールに分解します。
congr!: Mathlib の拡張版で、より賢く、より強力に分解を試みます。

💡 支援タクティクの「黄金のフロー」

Mathlib スタイルで証明を書く際、これらのタクティクを以下の順番で検討するのが効率的です。

形を整える: simp や congr! でゴールを扱いやすくする。
方針を探る: apply? や rw? で使える定理を探す。
構造を分解する: gcongr で不等式の外枠を外す。
計算でとどめを刺す: ring, linarith, field, norm_num のいずれかを使って、残った計算を一撃で解く。

🛠️ まとめ表

タクティク	支援の性質	主な用途
`simp`	簡約化	式を標準的な形に掃除する
`aesop`	全自動	複雑な論理構造を自動で解きほぐす
`gcongr`	構造分解	不等式の両辺の共通項を無視して中身を比べる
`norm_num`	定数計算	`2 + 3 = 5` などの具体的な計算を証明する
`congr!`	関数分解	`f x = f y` を `x = y` に落とし込む

import Mathlib.Tactic

section
open Classical

variable (A : Type)
variable (f : A → A)
variable (P : A → Prop)
variable (T : A -> A  → Prop)
variable (h : ∀ x, P x → P (f x))

example : ∀ y, P y → P (f (f y)) := by
  rintro x h1
  let h2: P (f x) := by exact h x h1
  exact h (f x) h2

example : ∀ y, P y → P (f (f y))
| x => h (f x) ∘ h x
end

1. 難しさの正体：「関数の入れ子」と「変数管理」

タクティクモード（intro, apply）では、Leanが裏側で変数の名前や型を管理してくれますが、項モードではそれらすべてを自分で記述する必要があります。

全称記号 (): 項モードでは単なる 「関数（-abstraction）」 です。
intro x は、項モードでは fun x ↦ ... に相当します。
存在記号 (): 項モードでは 「構造体（依存ペア）」 です。
use x は、項モードでは ⟨x, proof_of_Px⟩ という括弧（anonymous constructor）で包む必要があります。
含意 (): これも項モードでは 「関数」 です。
「証拠を受け取って、別の証拠を返す」という処理を頭の中でシミュレートしなければなりません。

2. 項モードを攻略する「翻訳」のコツ

難易度を下げるために、タクティクでの操作を以下のように「脳内変換」すると見通しが良くなります。

タクティク	項モードの「正体」	イメージ
`intro x`	`fun x ↦`	新しい変数を引数に取る関数を作る
`apply h`	`h (...)`	関数 `h` に引数を渡して実行する
`have h2 := ...`	`let h2 := ...`	計算の途中の結果に名前をつける
`use x`	`⟨x, ...⟩`	値と証明をセットにしたペアを作る
`cases h`	`match h with	⟨x, px⟩ =>`

3. 項モードが「パズル」から「設計」へ変わる瞬間

述語論理の項モードが難しく感じるのは、「型（Type）」と「命題（Prop）」の境界がなくなるからです。

例えば (h : ∀ x, P x) という前提があるとき、h x と書くことは、「関数 h に値 x を放り込んで、P x という結果を取り出す」というプログラミングそのものです。この**「証明を組み立てる＝プログラムを書く」**という感覚（カリー＝ハワード同型対応）に慣れるまでは、パズルのピースが多すぎて混乱しがちです。

💡 対策：複雑なときは `let` で刻む

一度に巨大な項を書こうとするとエラーの場所すらわからなくなります。述語論理では let を多用して、一段階ずつ証拠を作っていくのが Lean Mathlib スタイルのコツです。

-- 一気に書こうとすると難しい
fun h_ex ↦ match h_ex with | ⟨x, px⟩ => h_univ x px

-- let で刻むと、タクティクに近い感覚で書ける
fun h_ex ↦
  let ⟨x, px⟩ := h_ex
  let h_res := h_univ x px
  h_res

import Mathlib.Tactic

-- 命題を反証する：ある特定の A, P, Q のもとで、この含意は成り立たない
example : ¬ (∀ {A : Type} {P Q : A → Prop}, (∀ y, ∃ x, P x → Q y) → ((∃ x, P x) → ∀ y, Q y)) := by
  -- 1. 「もしこの命題が常に真（h_all）なら矛盾する」ことを示す
  intro h_all

  -- 2. 具体的な反例のモデルを定義する
  let A := Bool
  let p (b : Bool) : Prop := (b = true)  -- trueはP、falseはPでない
  let q (_ : Bool) : Prop := False       -- 誰もQではない

  -- 3. この反例モデルを h_all に適用して、具体的な含意を取り出す
  -- h_spec : (∀ y, ∃ x, p x → q y) → ((∃ x, p x) → ∀ y, q y)
  let h_spec := h_all (A := A) (P := p) (Q := q)

  -- 4. 前提 (∀ y, ∃ x, p x → q y) がこのモデルで「真」であることを示す
  have h_premise : ∀ y : Bool, ∃ x : Bool, p x → q y := by
    intro y
    -- x として false を選べば、p false は「偽」なので、ならばは常に「真」
    use false
    intro (hp_false : false = true)
    -- false = true という矛盾した仮定からは何でも導ける
    nomatch hp_false

  -- 5. 結論の「ならば」の左側 (∃ x, p x) が「真」であることを示す
  have h_exists_p : ∃ x : Bool, p x := by
    use true
    rfl -- true = true は定義より自明

  -- 6. h_spec にこれらを流し込むと、「∀ y, q y」が導かれてしまう
  let h_forall_q : ∀ y : Bool, q y := h_spec h_premise h_exists_p

  -- 7. しかし q false は False と定義したので、ここで矛盾が発生！
  -- h_forall_q false : False
  exact h_forall_q false

この証明のポイント（学びのポイント）

let A := Bool: 抽象的な型 A に、具体的な「2つの要素を持つ型」を代入しています。反例を作る際、Bool（true と false）は非常に便利です。
p x := (x = true): 「一部の人はだが、一部の人はではない」という状況を x = true という定義で作りました。
use false (Step 4): ここが最大の急所です。前提の ∃ x, P x → Q y において、「ではない人（）」を一人連れてくるだけで、前提全体を真にできてしまう（が何であろうと関係なくなる）ことを突いています。
**nomatch / rfl**:

自動化タクティクを駆使する場合の「現代的な Mathlib スタイル」を解説します。

「足場を探す」という観点では、simp で定義をバラし、aesop や tauto で論理的な隙間を埋めるのが王道です。これらを使うと、先ほどの「一歩ずつ」の証明が驚くほど短くなります。

回答の概要

simp [A]: A の定義（if-then-else）と集合の定義を一度に展開し、自明な項を整理します。
aesop (Automated Extensible Search Over Proofs):

intro, apply, cases などの論理操作を全自動で探索します。
「誰かが存在するはずだ」「ならばそれを持ってこよう」という推論を代行してくれます。

fin_cases: Fin 2 のような小さな型の有限個の場合分けを一瞬で終わらせます。

自動化を極めた最短の証明例

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Fin.Basic
import Mathlib.Tactic

open Set

def A (i j : Fin 2) : Set ℕ :=
  if i = j then {0} else ∅

/-- 1. 右辺： aesop に A の定義を教えて一発解決 -/
lemma mem_iInter_iUnion_example_aesop : 0 ∈ ⋂ j : Fin 2, ⋃ i : Fin 2, A i j := by
  -- 「A の定義を展開して、論理的に探索して」と頼む
  aesop? (add simp A)

/-- 2. 左辺： 同じく aesop で解決 -/
lemma not_mem_iUnion_iInter_example_aesop : 0 ∉ ⋃ i : Fin 2, ⋂ j : Fin 2, A i j := by
  -- 否定の証明も、aesop は内部で intro を試みるので成功します
  aesop? (add simp A)

/-- 3. 結論： 全体を aesop で繋ぐ -/
theorem distribution_counterexample_aesop :
    ¬ (⋂ j : Fin 2, ⋃ i : Fin 2, A i j ⊆ ⋃ i : Fin 2, ⋂ j : Fin 2, A i j) := by
  -- 上記の補題を「信頼できるルール(safe)」として追加
  aesop? (add safe mem_iInter_iUnion_example_aesop,
             safe not_mem_iUnion_iInter_example_aesop,
             simp subset_def)

「足場」を見つけるためのテクニック

自動化を使うとき、何が起きているか分からなくなった場合の対処法（足場の探し方）がいくつかあります。

simp?: simp が内部でどの補題を使ったかを表示してくれます。これをコピーして貼り付けることで、ブラックボックスを「明示的な証明」に置き換えられます。
aesop?: aesop が見つけた証明のステップをタクティクとして出力してくれます。
**apply? / exact?**: 「今ある仮定から、この結論を導けるライブラリの定理はないか？」を検索してくれます。

Mathlib スタイルのポイント

hi.elim: 0 ∈ ∅ という仮定 hi があるとき、False.elim を呼び出す代わりに .elim と書くだけで「空集合に属するなんてありえない」と一蹴できます。
fin_cases: 手動で match i with と書くよりも、Mathlib ではこのタクティクが標準的です。

自動化を使うと、「どう解くか」よりも「どの補題を組み合わせるか」というパズル感覚が強くなります。

1. 証明の最初の一手：「論理の解体」

何が起きているか分からなくなるのを防ぐために、まずは手動で「外枠」をバラします。

使う手: intro, obtain, constructor, cases
理由: aesop に任せると変数を勝手に名付けられてしまいますが、自分で intro x hx と書けば、その後の証明で hx という名前を使い続けられます。
コツ: 集合の包含関係（$\subseteq$）なら、まずは rw [subset_def] でバラしてから、要素を取り出すところまで自分でやります。

2. トリッキーな変形が必要な時：「中間地点の設置」

aesop が見つけられない「遠回り」や「ひらめき」が必要な場合です。

使う手: have, show, calc
理由: 「今はまだゴールに届かないけれど、とりあえずこの中間定理 $P$ だけは先に証明しておくぞ」と宣言します。
コツ: have h_mid : P := by ... と書いて「足場」を固めれば、その後の aesop はその h_mid を使ってゴールに辿り着けるようになります。

3. 巨大な計算が必要な時：「特化型タクティク」

aesop は汎用的な探索をするため、純粋な計算（算術や代数）では非効率です。

使う手:
算術（不等式など）: linarith
代数（多項式の展開など）: ring / polyrith
集合の基本変形: simp only [...]
理由: これらは特定の数学的構造に特化したアルゴリズムを使っているため、aesop よりも圧倒的に速く、タイムアウトしません。

まとめ：タクティクの使い分けマップ

場面	推奨する手	役割
最初の一歩	`intro`, `rw`	迷子にならないための「地図」作り。
ひらめきが必要	`have`, `use`	「この値を使うぞ！」という意思決定。
計算が重い	`ring`, `linarith`	専用の「計算機」に丸投げ。
最後の下処理	`aesop`	散らかった仮定をまとめて片付ける。

次のステップ：実践への落とし込み

今回の「分配法則の反例」で言うと、以下のような構成がベストです。

最初の一手: rw [subset_def] （手動でバラす）
トリッキーな一手: use 0 （「反例は 0 だ！」と人間が決める）
仕上げ: aesop （残った 0 に関する細かい条件を自動で解く）

1. `rw` (Rewrite)

「手動のメス」：指定した場所を 1 箇所（または全部）書き換えます。

動作: 最初に見つかった一致する項を書き換えます。
弱点: 「ラムダ式（$\lambda$）の中」や「限定記号（$\forall, \exists$）の中」には潜り込めません。
使い時:
一番外側に見えている項を、一歩ずつ丁寧に書き換えたい時。
rw [h] at hl のように、特定の仮定を書き換えたい時。

2. `simp_rw` (Simplifying Rewrite)

「潜入捜査官」：rw の精密さと simp の突破力を兼ね備えています。

動作: ラムダ式や $\forall, \exists$ の中まで深く潜り込んで、指定したルールを「繰り返し」適用します。
使い時:
$\forall x, f x = g x$ という式の中にある $f x$ を $g x$ に書き換えたい時（rw では届きません）。
simp だと余計なことまでされるが、rw だと「中身」に届かないという絶妙なシーン。
Mathlib流: simp only [h1, h2] と似ていますが、simp_rw は「順番通りに、かつ深く」適用されるため、より制御しやすいです。

3. `simp` (Simplifier)

「全自動お掃除ロボット」：利用可能なすべての知識を使って、式を最短化します。

動作: Mathlib に登録された数千のルール（@[simp]属性）と、自分が渡したルールを駆使して、勝手に「最も簡単な形」を模索します。
弱点: 賢すぎて、自分が止めてほしいところで止まってくれない（「そこはまだ展開しないで！」という時がある）。
使い時:
集合の定義（mem_union など）を一気に論理式までバラバラにする時。
証明の最後の方で、細かい計算を丸投げしたい時。

4. `nth_rewrite`

「ピンポイント狙撃手」：番号で場所を指定します。

動作: 同じ形が複数あるうち、指定した $n$ 番目の箇所だけを書き換えます。
使い時:
x + y = y + x を証明する際、左側の x だけを x + 0 に変えたい時。
全部書き換えると「無限ループ」してしまう等式を扱う時。

比較表：どれを使うべきか？

タクティク	潜り込み（$\forall$内など）	自動繰り返し	順番の厳守	主な用途
`rw`	❌	❌	✅	目に見える場所の 1 ステップ変形
`simp_rw`	✅	✅	✅	構造の中にある項の全置換
`simp`	✅	✅	❌	複雑な式の一気通貫な整理
`nth_rewrite`	❌	❌	✅	ループ回避や、特定の項のみの操作

実戦での使い分けチャート

迷ったときは、この優先順位で試してみてください。

優先度	タクティク	使うべきシーン
1	`simp`	集合の定義を一気にバラす、計算を終わらせるなど、「結果オーライ」な時。
2	`rw`	目に見える場所を 1 箇所だけ変えたい時。等号の左右を入れ替える（`←`）時。
3	`simp_rw`	`∀` や `∃` の中、あるいは関数の中を書き換えたいが、`simp` だと余計なことまでされる時。
4	`nth_rewrite`	同じ項が複数ある中で、特定の場所だけを狙い撃つ時。

`simp_rw` が「主役」になる時

逆に、以下のようなケースでは simp_rw が最強の武器になります。

-- ∀ の中にある A ∪ B をバラしたい場合
example (f : α → Set β) : (∀ x, f x ∈ A ∪ B) ↔ (∀ x, f x ∈ A ∨ f x ∈ B) := by
  -- rw [mem_union] だと「中身に届かない」とエラーが出る
  -- simp only [mem_union] でも行けるが、
  -- 他の simp ルールを適用したくない場合は simp_rw がベスト
  simp_rw [mem_union]

まとめ：あなたの現在の学習フェーズなら

これまでの集合の証明の流れを踏まえると、おすすめの使い分けはこうです：

まず ext で要素を出す。
simp only [mem_...] で集合を論理式に翻訳する。
論理式の変形で、rw だとエラーが出る（中身に届かない）時に simp_rw を発動する。

1. 矛盾（False）からの証明

前提に矛盾がある場合、tauto はそれを即座に見抜いて証明を終了させます。

例: $(P \land \neg P) \to Q$
集合での例: $x \in A \cap A^c \to x \in B$

example (h : x ∈ A ∩ Aᶜ) : x ∈ B := by
  simp [mem_inter_iff, mem_compl] at h
  tauto -- x ∈ A と ¬(x ∈ A) の矛盾を自動検出

2. 排中律（$P \lor \neg P$）が絡むケース

「$P$ か $P$ でないか」でケース分けが必要な問題も、tauto は自動で処理します。

例: $(P \to Q) \to (\neg Q \to \neg P)$ （対偶）
集合での例: $(A \cup B)^c = A^c \cap B^c$ （ド・モルガン）

example : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
  ext x
  simp [mem_compl, mem_union, mem_inter_iff]
  tauto -- ド・モルガンの論理的な正しさを判定

3. 冗長な条件の整理

同じ条件が複数回出てきたり、複雑に絡み合っているが、整理すると当たり前になる場合です。

例: $P \to (Q \to P)$
集合での例: $A \cap (A \cup B) = A$ （吸収律）

example : A ∩ (A ∪ B) = A := by
  ext x
  simp [mem_inter_iff, mem_union]
  tauto -- 「x ∈ A かつ (x ∈ A または x ∈ B)」が「x ∈ A」と等価であることを判定

4. 複雑な「ならば（$\to$）」の連鎖

「$A$ ならば $B$、$B$ ならば $C$、ゆえに $A$ ならば $C$」といった三段論法が複雑に組み合わさった場合です。

例: $(P \to Q) \land (Q \to R) \to (P \to R)$
集合での例: $A \subseteq B \land B \subseteq C \to A \subseteq C$

example (h1 : A ⊆ B) (h2 : B ⊆ C) : A ⊆ C := by
  rw [subset_def] at *
  -- ⊢ ∀ x, x ∈ A → x ∈ C
  intro x
  tauto -- h1 と h2 の連鎖を自動で解く

`tauto` を使う時の「心得」

量化子（$\forall, \exists$）には弱い: tauto は「命題論理」のプロですが、「述語論理（$x$ によって中身が変わる式）」の深い推論は苦手です。そのため、ext x や intro x で要素を固定してから使うのが鉄則です。
simp とのコンビネーション: 今回のあなたの証明のように、simp [mem_...] で「集合の言葉」を「論理の言葉（$\land, \lor, \to, \neg$）」に翻訳した直後に tauto を投げるのが、最も成功率の高いパターンです。

まとめ：回答の概要

矛盾の検出（$P$ と $\neg P$ がある）
対偶やド・モルガン（否定の絡む論理変形）
包含関係の連鎖（三段論法）
吸収律（余計な条件の削除）これらはすべて tauto で解決可能です。

タクティク,得意なこと,例 norm_num,具体的な数値の計算,“100+200=300, 25<40” ring,変数を含む多項式の整理,(x+y)2=x2+2xy+y2 simp,定義や規則に基づいた書き換え,“x+0=x, A∧A=A” arith (linarith),線形な不等式の鎖を解く,a<b∧b<c⟹a<c

aesop, tauto, itauto

Lean 相談と支援タクティク

💡 相談の際の「聞き方」の例

🛠️ 「釣り方」を学ぶためのクイックガイド

🚀 ワークフローの提案

1. calc で「あえて」刻んでみる（分割統治）

2. show タクティクで「中間地点」を宣言する

3. apply? や rw? で「一歩手前」を検索する

4. conv モードで「部分」を観察する

5. set_option trace... で裏側を覗く（上級者向け）