証明図から証明項に引き写すのは手作業。支援系とかいいながら、ソフトウェアは何も支援してくれない。
/-! example_1.lean -/ namespace Imp def elim_right {A B: Prop} (f:A → B) (a:A) : B := f a def elim_left {A B: Prop} (a:A) (f:A → B) : B := f a end Imp variable (A B C D: Prop) def example_1 (p1: A) (p2: A→B) (p3: B→C) : C∧(A∨D) := /-(1)-/ have a: A := p1 /-(2)-/ have a_imp_b := p2 /-(3)-/ have b: B := Imp.elim_left a a_imp_b /-(4)-/ have c_imp_b := p3 /-(5)-/ have c: C := Imp.elim_right c_imp_b b /-(6) = (1) -/ -- 重複記述はできない /-(7)-/ have a_or_d: A∨D := Or.intro_left D a /-(8)-/ show C∧(A∨D) from And.intro c a_or_d #check example_1 def example_1' (p1: A) (p2: A→B) (p3: B→C) : C∧(A∨D) := /-(1)-/ have b: B := p2 p1 /-(2)-/ have c: C := p3 b /-(3)-/ have a_or_d: A∨D := Or.intro_left D p1 /-(4)-/ show C∧(A∨D) from And.intro c a_or_d #check example_1'