等式の種類：
- definitional equality ： Leanカーネルが判定する項の同一性。システムレベルで「同じ」とみなす。
- propositional equality ： 等値性を意味する命題（真か偽の文）。証明がないと保証されない。システムレベルで事前に成立している同一性ではない。
- syntactic equality ： 証明済み命題的等式だが、左辺から右辺の構文書き換え規則とみなされた等式。等式的書き換え〈rewrite〉で使う。左右〈from-to〉の別がある。
一部のタクティク（use, splitなど）はmathlibで定義されてるので、import Mathlib.Tactic.Use が必要。とりあえず出来たところだけ。
ship/assumption/exact
Γ, (p! : P) |! ship p! Γ, (p! : P) |-! P
Γ, (p! : P) |-? P assumption（または exact p!） Γ, (p! : P) |!
apply モダスポネンス
Γ, (p2q! : P → Q) |-? Q apply p2q! at <target> Γ, (p2q! : P → Q) |-? P Γ, (p2q! : P → Q) |-! P adopt as p! Γ, p2q! : P → Q, p!: P |! ship (apply p2q! at p!) Γ, (p2q! : P → Q), (p!: P) |-! Q
rw 等値 両方向
Γ, (e! : a => b) |-* a + 1 = 37 rw with e! at <target> Γ, (e! : a => b) |-* b + 1 = 37
rw 同値 両方向
Γ, (e! : P <->> Q), (h! : P → (R ∨ <-> S)) |-* X rw with e! at h! Γ, (e! : P <->> Q), (h! : Q → (R ∨ <-> S)) |-* X
rw 同値 ライブラリ利用
Γ∋ ( not_iff_imp_false : ￢ P <->> (P → false) ) Γ |-* ￢P → Q rw with not_iff_imp_false at <target> Γ |-* (P → false) → Q
by_contra 背理法
Γ |-? P by_contra Γ, (h : ￢P) |-? false Γ, (h : ￢P) |-! false by_contra Γ |-! P
cases AND
Γ, (ab! : A∧B) |-? X cases ab! a! b! Γ, (a! : A(), (b! : B) |-? X Γ, (a! : A), (b! : B) |-! X context_and_intro a! b! ab! Γ, (ab! : A∧B) |-! X
cases 同値
Γ, (aEb! : A <-> B) |-? X cases aEb! a2b! b2a! Γ, (a2b! : A → B), (b2a! : B → A) |-? X Γ, (a2b! : A → B), (b2a! : B → A) |-! X context_and_intro a2b! b2a! a2bAb2a! Γ, (a2bAb2a! : (A → B)∧(B → A)) |-! X rw with 同値の定義 at a2bAb2a! to aEb! Γ, (aEb! : A <-> B) |-! X
cases OR
Γ, (aOb! : A ∨ B) |-? X cases aOb! a! b! Γ, (a! : A) |-? X ＆＆ Γ, (b! : B) |-? X Γ, (a! : A) |-! X ＆＆ Γ, (b! : B) |-! X context_or_intro !a !b aOb! Γ, (aOb! : A∨B) |-! X
cases 自然数
Γ, (n : Nat) |-? P n cases n m Γ, (n : Nat) |-? P 0 ＆＆ Γ, (m : Nat) |-? P (suc m)
cases 存在
Γ, (h : ∃ x, x^3 + x = 37) |-? X cases h with a ha Γ, (a : Nat), (ha : a^3 + a = 37) |-? X Γ, (a : Nat), (ha : a^3 + a = 37) |-! X context_ex_intro ha a h x Γ, (h : ∃ x, x^3 + x = 37) |-! X
