Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

	step type	requirements	statement
0	instantiation	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11*	⊢
	: , : , : , : , : , :
1	reference	63	⊢
2	reference	126	⊢
3	reference	109	⊢
4	theorem		⊢
	proveit.numbers.numerals.decimals.nat6
5	reference	128	⊢
6	instantiation	119	⊢
	: , :
7	instantiation	12	⊢
	: , : , : , : , : , :
8	instantiation	145, 139, 13	⊢
	: , : , :
9	reference	137	⊢
10	reference	41	⊢
11	instantiation	94, 14, 15	⊢
	: , : , :
12	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_6_typical_eq
13	instantiation	145, 141, 16	⊢
	: , : , :
14	instantiation	106, 17	⊢
	: , : , :
15	instantiation	63, 126, 109, 59, 128, 18, 19, 20, 137, 41, 21*	⊢
	: , : , : , : , : , :
16	instantiation	145, 143, 22	⊢
	: , : , :
17	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_1
18	instantiation	119	⊢
	: , :
19	instantiation	23	⊢
	: , : , : , : , :
20	instantiation	145, 139, 24	⊢
	: , : , :
21	instantiation	94, 25, 26	⊢
	: , : , :
22	instantiation	145, 146, 109	⊢
	: , : , :
23	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
24	instantiation	145, 141, 27	⊢
	: , : , :
25	instantiation	106, 28	⊢
	: , : , :
26	instantiation	63, 126, 109, 60, 128, 29, 30, 41, 137, 31*	⊢
	: , : , : , : , : , :
27	instantiation	145, 143, 32	⊢
	: , : , :
28	theorem		⊢
	proveit.numbers.numerals.decimals.add_3_1
29	instantiation	119	⊢
	: , :
30	instantiation	33	⊢
	: , : , : , :
31	instantiation	94, 34, 35	⊢
	: , : , :
32	instantiation	145, 146, 37	⊢
	: , : , :
33	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
34	instantiation	106, 36	⊢
	: , : , :
35	instantiation	63, 126, 109, 37, 128, 38, 39, 40, 41, 137, 42*	⊢
	: , : , : , : , : , :
36	theorem		⊢
	proveit.numbers.numerals.decimals.add_4_1
37	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
38	instantiation	119	⊢
	: , :
39	instantiation	43	⊢
	: , : , :
40	instantiation	145, 139, 44	⊢
	: , : , :
41	instantiation	145, 139, 45	⊢
	: , : , :
42	instantiation	94, 46, 47	⊢
	: , : , :
43	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
44	instantiation	145, 141, 48	⊢
	: , : , :
45	instantiation	145, 141, 49	⊢
	: , : , :
46	instantiation	106, 50	⊢
	: , : , :
47	instantiation	63, 126, 109, 128, 51, 110, 52, 137, 53*	⊢
	: , : , : , : , : , :
48	instantiation	145, 143, 54	⊢
	: , : , :
49	instantiation	145, 143, 55	⊢
	: , : , :
50	theorem		⊢
	proveit.numbers.numerals.decimals.add_5_4
51	instantiation	119	⊢
	: , :
52	instantiation	145, 139, 56	⊢
	: , : , :
53	instantiation	94, 57, 58	⊢
	: , : , :
54	instantiation	145, 146, 59	⊢
	: , : , :
55	instantiation	145, 146, 60	⊢
	: , : , :
56	instantiation	145, 141, 61	⊢
	: , : , :
57	instantiation	106, 62	⊢
	: , : , :
58	instantiation	63, 126, 109, 147, 128, 64, 65, 137, 66*	⊢
	: , : , : , : , : , :
59	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
60	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
61	instantiation	145, 143, 67	⊢
	: , : , :
62	theorem		⊢
	proveit.numbers.numerals.decimals.add_9_1
63	theorem		⊢
	proveit.numbers.addition.association
64	instantiation	119	⊢
	: , :
65	instantiation	145, 139, 68	⊢
	: , : , :
66	instantiation	94, 69, 70	⊢
	: , : , :
67	instantiation	145, 146, 127	⊢
	: , : , :
68	instantiation	145, 141, 71	⊢
	: , : , :
69	instantiation	106, 72	⊢
	: , : , :
70	instantiation	77, 147, 126, 103, 73, 74*, 75*	⊢
	: , : , : , :
71	instantiation	145, 143, 76	⊢
	: , : , :
72	instantiation	77, 147, 126, 103, 104, 78, 79*, 80*	⊢
	: , : , : , :
73	instantiation	81, 140, 82, 83, 84, 122*, 85*	⊢
	: , : , :
74	instantiation	108, 109, 126, 110, 92, 128, 93	⊢
	: , : , : , : , : , : , :
75	instantiation	94, 86, 87	⊢
	: , : , :
76	instantiation	145, 88, 89	⊢
	: , : , :
77	theorem		⊢
	proveit.numbers.numerals.decimals.md_nine_add_one
78	instantiation	98, 90	⊢
	:
79	instantiation	108, 109, 126, 91, 92, 128, 93	⊢
	: , : , : , : , : , : , :
80	instantiation	94, 95, 96	⊢
	: , : , :
81	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
82	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
83	instantiation	145, 141, 97	⊢
	: , : , :
84	instantiation	98, 99	⊢
	:
85	theorem		⊢
	proveit.numbers.numerals.decimals.add_8_1
86	instantiation	106, 100	⊢
	: , : , :
87	instantiation	108, 109, 126, 101, 111, 128, 112	⊢
	: , : , : , : , : , : , :
88	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
89	instantiation	102, 147, 103, 104, 105	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.numerals.decimals.posnat9
91	instantiation	119	⊢
	: , :
92	instantiation	120, 126	⊢
	: , :
93	instantiation	121, 122	⊢
	: , : , :
94	axiom		⊢
	proveit.logic.equality.equals_transitivity
95	instantiation	106, 107	⊢
	: , : , :
96	instantiation	108, 109, 126, 110, 111, 128, 112	⊢
	: , : , : , : , : , : , :
97	instantiation	145, 143, 113	⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
99	theorem		⊢
	proveit.numbers.numerals.decimals.posnat8
100	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
101	instantiation	119	⊢
	: , :
102	theorem		⊢
	proveit.numbers.numerals.decimals.deci_sequence_is_nat_pos
103	instantiation	115, 114, 117	⊢
	: , : , :
104	instantiation	115, 116, 117	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
106	axiom		⊢
	proveit.logic.equality.substitution
107	instantiation	118, 137	⊢
	:
108	theorem		⊢
	proveit.core_expr_types.tuples.tuple_portion_substitution
109	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
110	instantiation	119	⊢
	: , :
111	instantiation	120, 126	⊢
	: , :
112	instantiation	121, 122	⊢
	: , : , :
113	instantiation	145, 146, 123	⊢
	: , : , :
114	instantiation	125, 147, 123, 124	⊢
	: , : , : , : , :
115	theorem		⊢
	proveit.logic.equality.sub_left_side_into
116	instantiation	125, 126, 127, 128, 129	⊢
	: , : , : , : , :
117	theorem		⊢
	proveit.numbers.numerals.decimals.N_leq_9_enumSet
118	theorem		⊢
	proveit.numbers.addition.elim_zero_left
119	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
120	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
121	axiom		⊢
	proveit.core_expr_types.tuples.empty_range_def
122	instantiation	130, 131, 132	⊢
	: , : , :
123	theorem		⊢
	proveit.numbers.numerals.decimals.nat8
124	instantiation	133	⊢
	: , : , : , : , : , : , : , :
125	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
126	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
127	theorem		⊢
	proveit.numbers.numerals.decimals.nat9
128	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
129	instantiation	134	⊢
	: , : , : , : , : , : , : , : , :
130	theorem		⊢
	proveit.logic.equality.sub_right_side_into
131	instantiation	135, 137	⊢
	:
132	instantiation	136, 137, 138	⊢
	: , :
133	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_8_typical_eq
134	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_9_typical_eq
135	theorem		⊢
	proveit.numbers.addition.elim_zero_right
136	theorem		⊢
	proveit.numbers.addition.commutation
137	instantiation	145, 139, 140	⊢
	: , : , :
138	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
139	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
140	instantiation	145, 141, 142	⊢
	: , : , :
141	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
142	instantiation	145, 143, 144	⊢
	: , : , :
143	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
144	instantiation	145, 146, 147	⊢
	: , : , :
145	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
146	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
147	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements