順不同・断片的な記述となる。ネタ元は：
https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#basic-tactics で出てくるタクティクを列挙。
- apply Iff.itro ： 論理同値を分解する。Iff.introの逆行。
- intro h ： ターゲット含意の前件を、証拠名 h でコンテキストに移す。含意導入の逆行。
- apply Or.elim (And.right h) ： 式 Or.elim (And.right h) - - の適用の逆行。
- apply Or.elim h ： 式 Or.elim h - - の逆行。順行のOr.elimをよーく理解してないと逆行は難しい。
theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :=
match h with
| Or.inl h => left h
| Or.inr h => right h説明：
- 第一明示引数 (h : Or a b) ： Or命題に至る証明、inl, inrという証明値コフィールド〈選択肢〉を持つコタプル構造〈コレコード〉h : a または h: b のどちらかとなる。
- 第二明示引数 (left : a → c) ： aからcへの証明
- 第三明示引数 (right : b → c) ： bからcへの証明
- ターゲット〈戻り型〉 c ： 共通の結論型
/-
case mp
p q r : Prop
h : p ∧ (q ∨ r)
⊢ p ∧ q ∨ p ∧ r
-/
apply Or.elim (And.right h) -- p → p∨r
/-
case mp.left
p q r : Prop
h : p ∧ (q ∨ r)
⊢ q → p ∧ q ∨ p ∧ r
case mp.right
p q r : Prop
h : p ∧ (q ∨ r)
⊢ r → p ∧ q ∨ p ∧ r
-/
