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*	, , ,  ⊢
	: , : , :
1	reference	64	⊢
2	modus ponens	6, 7	, , ,  ⊢
3	instantiation	88, 148	⊢
	: , :
4	reference	12	⊢
5	instantiation	81, 8, 9	, , ,  ⊢
	: , : , :
6	instantiation	103, 104	⊢
	: , : , : , : , : , : , :
7	generalization	10	, , ,  ⊢
8	instantiation	64, 11, 12*, 13*	, , ,  ⊢
	: , : , :
9	instantiation	81, 14, 15	, , ,  ⊢
	: , : , :
10	instantiation	56, 57, 16, 126, 127	, , , ,  ⊢
	: , : , : , : , :
11	modus ponens	17, 18	, , ,  ⊢
12	instantiation	88, 148	⊢
	: , :
13	instantiation	88, 148	⊢
	: , :
14	instantiation	81, 19, 20	, , ,  ⊢
	: , : , :
15	instantiation	64, 21	,  ⊢
	: , : , :
16	instantiation	91, 57, 125, 22	, , ,  ⊢
	: , : , : , :
17	instantiation	103, 104	⊢
	: , : , : , : , : , : , :
18	generalization	23	, , ,  ⊢
19	instantiation	81, 24, 25	,  ⊢
	: , : , :
20	instantiation	27, 26	, , ,  ⊢
	: , :
21	instantiation	27, 28	,  ⊢
	: , :
22	instantiation	91, 57, 128, 58	, ,  ⊢
	: , : , : , :
23	instantiation	81, 29, 30	, , , ,  ⊢
	: , : , :
24	instantiation	81, 31, 32	,  ⊢
	: , : , :
25	instantiation	64, 33, 48*, 34*	,  ⊢
	: , : , :
26	modus ponens	35, 36	, , ,  ⊢
27	theorem		⊢
	proveit.logic.equality.equals_reversal
28	modus ponens	37, 38	,  ⊢
29	instantiation	39, 153, 40, 41, 42, 43	, , , ,  ⊢
	: , : , : , :
30	instantiation	56, 57, 58, 60, 99, 44*	, , , ,  ⊢
	: , : , : , : , :
31	instantiation	81, 45, 46	,  ⊢
	: , : , :
32	instantiation	64, 47, 67*, 48*	,  ⊢
	: , : , :
33	modus ponens	49, 50	,  ⊢
34	instantiation	88, 148	⊢
	: , :
35	instantiation	51, 104, 92, 108	,  ⊢
	: , : , : , : , : , : , : , :
36	modus ponens	52, 53	,  ⊢
37	instantiation	54, 149, 104, 122, 92, 123	⊢
	: , : , : , : , : , : , : , : , : , : , :
38	generalization	55	,  ⊢
39	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
40	instantiation	133	⊢
	: , :
41	instantiation	133	⊢
	: , :
42	instantiation	79, 126, 127	,  ⊢
	: , :
43	instantiation	56, 57, 58, 125, 128, 59*	, , ,  ⊢
	: , : , : , : , :
44	instantiation	79, 60, 99, 61*	, ,  ⊢
	: , :
45	instantiation	64, 62, 63*, 66*	,  ⊢
	: , : , :
46	instantiation	64, 65, 66*, 67*	,  ⊢
	: , : , :
47	modus ponens	68, 69	,  ⊢
48	instantiation	88, 148	⊢
	: , :
49	instantiation	103, 104	⊢
	: , : , : , : , : , : , :
50	generalization	70	,  ⊢
51	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum_with_scalar_mult
52	instantiation	71, 104, 92	⊢
	: , : , : , : , : , :
53	generalization	73	,  ⊢
54	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_distribution_over_summation_with_scalar_mult
55	instantiation	72, 73, 74	, ,  ⊢
	: , : , :
56	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled
57	instantiation	109, 111, 75, 76	⊢
	: , : , :
58	instantiation	110, 111, 75, 76, 114, 77, 78	,  ⊢
	: , : , : , :
59	instantiation	79, 125, 128	,  ⊢
	: , :
60	instantiation	154, 136, 80	,  ⊢
	: , : , :
61	instantiation	81, 82, 83	, ,  ⊢
	: , : , :
62	modus ponens	84, 85	,  ⊢
63	instantiation	88, 148	⊢
	: , :
64	axiom		⊢
	proveit.logic.equality.substitution
65	modus ponens	86, 87	,  ⊢
66	instantiation	88, 148	⊢
	: , :
67	instantiation	88, 148	⊢
	: , :
68	instantiation	103, 104	⊢
	: , : , : , : , : , : , :
69	generalization	89	,  ⊢
70	instantiation	106, 149, 153, 122, 124, 123, 90, 127, 128	, ,  ⊢
	: , : , : , : , : , :
71	theorem		⊢
	proveit.linear_algebra.addition.summation_closure
72	theorem		⊢
	proveit.logic.equality.sub_left_side_into
73	instantiation	91, 92, 95, 93	, ,  ⊢
	: , : , : , :
74	instantiation	94, 95, 149, 122, 123, 113, 115, 116	, ,  ⊢
	: , : , : , : , : , : , : , : , : , :
75	instantiation	133	⊢
	: , :
76	instantiation	96, 131	⊢
	:
77	instantiation	97, 98, 115	⊢
	: , : , :
78	instantiation	97, 98, 116	⊢
	: , : , :
79	axiom		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
80	instantiation	129, 135, 139	,  ⊢
	: , :
81	axiom		⊢
	proveit.logic.equality.equals_transitivity
82	instantiation	100, 122, 153, 149, 123, 120, 126, 127, 99	, ,  ⊢
	: , : , : , : , : , :
83	instantiation	100, 153, 122, 120, 101, 123, 126, 127, 125, 128	, ,  ⊢
	: , : , : , : , : , :
84	instantiation	103, 104	⊢
	: , : , : , : , : , : , :
85	generalization	102	,  ⊢
86	instantiation	103, 104	⊢
	: , : , : , : , : , : , :
87	generalization	105	,  ⊢
88	theorem		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
89	instantiation	106, 122, 153, 123, 107, 124, 126, 125, 127, 128	, ,  ⊢
	: , : , : , : , : , :
90	instantiation	154, 136, 108	,  ⊢
	: , : , :
91	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
92	instantiation	109, 111, 112, 113	⊢
	: , : , :
93	instantiation	110, 111, 112, 113, 114, 115, 116	,  ⊢
	: , : , : , :
94	theorem		⊢
	proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod
95	instantiation	129, 139, 137	⊢
	: , :
96	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
97	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
98	instantiation	117, 131, 118	⊢
	: , : , :
99	instantiation	119, 125, 128	,  ⊢
	: , :
100	theorem		⊢
	proveit.numbers.multiplication.disassociation
101	instantiation	133	⊢
	: , :
102	instantiation	121, 122, 153, 149, 123, 120, 126, 127, 125, 128	, ,  ⊢
	: , : , : , : , : , : , :
103	theorem		⊢
	proveit.core_expr_types.lambda_maps.general_lambda_substitution
104	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
105	instantiation	121, 122, 149, 153, 123, 124, 125, 126, 127, 128	, ,  ⊢
	: , : , : , : , : , : , :
106	theorem		⊢
	proveit.numbers.multiplication.association
107	instantiation	133	⊢
	: , :
108	instantiation	129, 135, 134	,  ⊢
	: , :
109	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
110	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
111	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
112	instantiation	133	⊢
	: , :
113	instantiation	130, 131	⊢
	:
114	instantiation	133	⊢
	: , :
115	assumption		⊢
116	assumption		⊢
117	theorem		⊢
	proveit.logic.sets.cartesian_products.cart_exp_subset_eq
118	instantiation	132, 136	⊢
	: , :
119	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
120	instantiation	133	⊢
	: , :
121	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
122	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
123	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
124	instantiation	133	⊢
	: , :
125	instantiation	154, 136, 134	⊢
	: , : , :
126	instantiation	154, 136, 135	⊢
	: , : , :
127	instantiation	154, 136, 139	⊢
	: , : , :
128	instantiation	154, 136, 137	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
130	theorem		⊢
	proveit.linear_algebra.real_vec_set_is_vec_space
131	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
132	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
133	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
134	assumption		⊢
135	assumption		⊢
136	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
137	instantiation	138, 139, 140	⊢
	: , :
138	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
139	instantiation	154, 142, 141	⊢
	: , : , :
140	instantiation	154, 142, 143	⊢
	: , : , :
141	instantiation	154, 145, 144	⊢
	: , : , :
142	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
143	instantiation	154, 145, 146	⊢
	: , : , :
144	instantiation	154, 147, 148	⊢
	: , : , :
145	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
146	instantiation	154, 155, 149	⊢
	: , : , :
147	instantiation	150, 151, 152	⊢
	: , :
148	assumption		⊢
149	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
150	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
151	instantiation	154, 155, 153	⊢
	: , : , :
152	instantiation	154, 155, 156	⊢
	: , : , :
153	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
154	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
155	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
156	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
*equality replacement requirements