Eq〈イコール〉の定義： inductive Eq : α → α → Prop where /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the equality type. See also `rfl`, which is usually used instead. -/ | refl (a : α) : Eq a aこの定義のリカーサー〈帰…

順不同・断片的な記述となる。ネタ元は： https://leanprover.github.io/theorem_proving_in_lean4/tactics.html https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#basic-tactics で出てくるタクティクを列挙。 apply Iff.itro ： 論理…

過去記事： タクティク解説、等式の種類も タクティクのためのゲンツェン法則 「Leanタクティク」は、実際のLeanのタクティクを話題にする。参考URL： https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_C/Part_C.html ケビン…