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*	, ,  ⊢
	: , :
1	axiom		⊢
	proveit.logic.equality.not_equals_def
2	instantiation	3, 4	, ,  ⊢
	:
3	axiom		⊢
	proveit.logic.booleans.eq_true_intro
4	instantiation	5, 6	, ,  ⊢
	: , :
5	theorem		⊢
	proveit.logic.equality.unfold_not_equals
6	modus ponens	7, 8	, ,  ⊢
7	instantiation	9, 60, 127, 10, 11, 12, 13, 14, 15, 16	⊢
	: , : , : , :
8	instantiation	17, 60, 18, 19, 20	, ,  ⊢
	: , : , :
9	theorem		⊢
	proveit.physics.quantum.circuits.qcircuit_neq
10	instantiation	108, 21, 23, 24	⊢
	: , : , : , :
11	instantiation	108, 22, 23, 24	⊢
	: , : , : , :
12	instantiation	108, 25, 68, 28	⊢
	: , : , : , :
13	instantiation	108, 26, 68, 28	⊢
	: , : , : , :
14	instantiation	108, 27, 68, 28	⊢
	: , : , : , :
15	instantiation	108, 66, 68, 28	⊢
	: , : , : , :
16	instantiation	108, 67, 68, 28	⊢
	: , : , : , :
17	theorem		⊢
	proveit.core_expr_types.expr_arrays.varray_neq_via_any_elem_neq
18	instantiation	170	⊢
	: , : , : , :
19	instantiation	170	⊢
	: , : , : , :
20	instantiation	29, 118, 191, 30, 192, 31, 32, 33, 34, 35	, ,  ⊢
	: , : , : , : , :
21	instantiation	80, 37, 36, 39, 40, 83, 84, 48, 41*	⊢
	: , : , : , :
22	instantiation	80, 37, 38, 39, 40, 83, 84, 48, 41*	⊢
	: , : , : , :
23	instantiation	124, 42	⊢
	: , :
24	instantiation	124, 43	⊢
	: , :
25	instantiation	80, 81, 44, 150, 139, 83, 84, 99*, 142*	⊢
	: , : , : , :
26	instantiation	80, 81, 45, 46, 47, 83, 48, 99*, 75*	⊢
	: , : , : , :
27	instantiation	80, 81, 49, 150, 139, 83, 84, 99*, 142*	⊢
	: , : , : , :
28	instantiation	124, 50	⊢
	: , :
29	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_any
30	instantiation	144	⊢
	: , : , :
31	instantiation	198	⊢
	: , :
32	instantiation	198	⊢
	: , :
33	instantiation	198	⊢
	: , :
34	instantiation	198	⊢
	: , :
35	instantiation	51, 52, 53, 54, 55, 56	, ,  ⊢
	: , : , :
36	instantiation	88	⊢
	: , : , : , : , : , : , : , :
37	theorem		⊢
	proveit.numbers.numerals.decimals.posnat8
38	instantiation	88	⊢
	: , : , : , : , : , : , : , :
39	instantiation	88	⊢
	: , : , : , : , : , : , : , :
40	instantiation	88	⊢
	: , : , : , : , : , : , : , :
41	instantiation	211, 57, 58	⊢
	: , : , :
42	instantiation	147, 248, 246, 191, 139, 192, 123, 184, 172	⊢
	: , : , : , : , : , :
43	instantiation	59, 60, 61, 102	⊢
	: , : , :
44	instantiation	207	⊢
	: , :
45	instantiation	207	⊢
	: , :
46	instantiation	207	⊢
	: , :
47	instantiation	207	⊢
	: , :
48	instantiation	100, 154, 75	⊢
	: , : , :
49	instantiation	207	⊢
	: , :
50	instantiation	101, 102	⊢
	: , :
51	theorem		⊢
	proveit.core_expr_types.tuples.tuple_neq_via_any_elem_neq
52	instantiation	215, 62, 63	⊢
	: , :
53	instantiation	211, 64, 65	⊢
	: , : , :
54	instantiation	108, 66, 68, 69	⊢
	: , : , : , :
55	instantiation	108, 67, 68, 69	⊢
	: , : , : , :
56	instantiation	86, 158, 154, 191, 133, 130, 192, 70	, ,  ⊢
	: , : , : , : , : , :
57	instantiation	71, 72, 73, 74, 99, 142, 75	⊢
	: , : , : , :
58	instantiation	108, 76, 77, 78	⊢
	: , : , : , :
59	theorem		⊢
	proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1
60	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
61	instantiation	157, 206	⊢
	: , :
62	instantiation	100, 251, 99	⊢
	: , : , :
63	instantiation	100, 214, 142	⊢
	: , : , :
64	instantiation	230, 99	⊢
	: , : , :
65	instantiation	230, 142	⊢
	: , : , :
66	instantiation	80, 81, 79, 150, 139, 83, 84, 99*, 142*	⊢
	: , : , : , :
67	instantiation	80, 81, 82, 150, 139, 83, 84, 99*, 142*	⊢
	: , : , : , :
68	instantiation	186	⊢
	:
69	instantiation	124, 85	⊢
	: , :
70	instantiation	86, 191, 158, 248, 192, 133, 87	, ,  ⊢
	: , : , : , : , : , :
71	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
72	theorem		⊢
	proveit.numbers.numerals.decimals.nat8
73	instantiation	88	⊢
	: , : , : , : , : , : , : , :
74	instantiation	88	⊢
	: , : , : , : , : , : , : , :
75	instantiation	211, 89, 90	⊢
	: , : , :
76	instantiation	108, 91, 92, 93	⊢
	: , : , : , :
77	instantiation	190, 191, 206, 192, 94, 96, 184, 172, 95*	⊢
	: , : , : , : , : , :
78	instantiation	190, 248, 206, 191, 96, 192, 97, 172, 98*	⊢
	: , : , : , : , : , :
79	instantiation	207	⊢
	: , :
80	theorem		⊢
	proveit.core_expr_types.tuples.general_len
81	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
82	instantiation	207	⊢
	: , :
83	instantiation	100, 158, 99	⊢
	: , : , :
84	instantiation	100, 154, 142	⊢
	: , : , :
85	instantiation	101, 102	⊢
	: , :
86	theorem		⊢
	proveit.logic.booleans.disjunction.disassociate
87	instantiation	103, 104, 105, 106	, ,  ⊢
	: , :
88	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_8_typical_eq
89	instantiation	230, 107	⊢
	: , : , :
90	instantiation	108, 109, 110, 111	⊢
	: , : , : , :
91	instantiation	117, 248, 112, 113, 184, 172	⊢
	: , : , : , : , : , : , :
92	instantiation	117, 246, 118, 114, 115, 116, 184, 172	⊢
	: , : , : , : , : , : , :
93	instantiation	117, 118, 248, 119, 120, 184, 172	⊢
	: , : , : , : , : , : , :
94	instantiation	170	⊢
	: , : , : , :
95	instantiation	124, 121, 126*	⊢
	: , :
96	instantiation	170	⊢
	: , : , : , :
97	instantiation	122, 123, 184	⊢
	: , :
98	instantiation	124, 125, 126*	⊢
	: , :
99	instantiation	167, 195, 184, 168	⊢
	: , : , :
100	theorem		⊢
	proveit.logic.equality.sub_left_side_into
101	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
102	instantiation	249, 179, 127	⊢
	: , : , :
103	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_left
104	instantiation	129, 251, 133, 128	⊢
	: , :
105	instantiation	129, 214, 130, 131	⊢
	: , :
106	instantiation	132, 251, 133, 134	, ,  ⊢
	: , :
107	instantiation	135, 184, 195	⊢
	: , :
108	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
109	instantiation	138, 191, 246, 192, 139, 136, 184, 172, 137, 195	⊢
	: , : , : , : , : , :
110	instantiation	138, 246, 248, 139, 140, 184, 172, 162, 165, 195	⊢
	: , : , : , : , : , :
111	instantiation	211, 141, 142	⊢
	: , : , :
112	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
113	instantiation	143	⊢
	: , : , : , : , :
114	instantiation	207	⊢
	: , :
115	instantiation	207	⊢
	: , :
116	instantiation	144	⊢
	: , : , :
117	theorem		⊢
	proveit.numbers.addition.leftward_commutation
118	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
119	instantiation	144	⊢
	: , : , :
120	instantiation	144	⊢
	: , : , :
121	instantiation	147, 191, 206, 248, 192, 148, 195, 184, 145*	⊢
	: , : , : , : , : , :
122	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
123	instantiation	249, 209, 146	⊢
	: , : , :
124	theorem		⊢
	proveit.logic.equality.equals_reversal
125	instantiation	147, 191, 206, 248, 192, 148, 195, 172, 149*	⊢
	: , : , : , : , : , :
126	instantiation	190, 191, 246, 192, 150, 195, 151*	⊢
	: , : , : , : , : , :
127	instantiation	215, 251, 214	⊢
	: , :
128	modus ponens	152, 153	⊢
129	theorem		⊢
	proveit.logic.booleans.disjunction.closure
130	instantiation	157, 154	⊢
	: , :
131	modus ponens	155, 156	⊢
132	theorem		⊢
	proveit.logic.booleans.disjunction.any_if_all
133	instantiation	157, 158	⊢
	: , :
134	modus ponens	159, 160	, ,  ⊢
135	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
136	instantiation	207	⊢
	: , :
137	instantiation	161, 162, 165	⊢
	: , :
138	theorem		⊢
	proveit.numbers.addition.disassociation
139	instantiation	207	⊢
	: , :
140	instantiation	207	⊢
	: , :
141	instantiation	163, 191, 248, 246, 192, 164, 184, 172, 165, 195, 166	⊢
	: , : , : , : , : , : , : , :
142	instantiation	167, 195, 172, 168	⊢
	: , : , :
143	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
144	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
145	instantiation	171, 184	⊢
	:
146	instantiation	249, 228, 169	⊢
	: , : , :
147	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
148	instantiation	170	⊢
	: , : , : , :
149	instantiation	171, 172	⊢
	:
150	instantiation	207	⊢
	: , :
151	instantiation	211, 173, 174	⊢
	: , : , :
152	instantiation	180, 243, 244, 181	⊢
	: , : , : , :
153	generalization	175	⊢
154	instantiation	249, 179, 214	⊢
	: , : , :
155	instantiation	180, 243, 176, 177	⊢
	: , : , : , :
156	generalization	178	⊢
157	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
158	instantiation	249, 179, 251	⊢
	: , : , :
159	instantiation	180, 243, 244, 181	⊢
	: , : , : , :
160	generalization	182	, ,  ⊢
161	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
162	instantiation	183, 184	⊢
	:
163	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
164	instantiation	207	⊢
	: , :
165	instantiation	249, 209, 185	⊢
	: , : , :
166	instantiation	186	⊢
	:
167	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
168	instantiation	186	⊢
	:
169	instantiation	249, 240, 187	⊢
	: , : , :
170	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
171	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
172	instantiation	249, 209, 188	⊢
	: , : , :
173	instantiation	230, 189	⊢
	: , : , :
174	instantiation	190, 191, 246, 248, 192, 193, 194, 195, 196*	⊢
	: , : , : , : , : , :
175	instantiation	198	⊢
	: , :
176	instantiation	249, 250, 214	⊢
	: , : , :
177	instantiation	199, 197	⊢
	:
178	instantiation	198	⊢
	: , :
179	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
180	theorem		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
181	instantiation	199, 200	⊢
	:
182	instantiation	201, 202, 203	, , ,  ⊢
	: , : , : , :
183	theorem		⊢
	proveit.numbers.negation.complex_closure
184	instantiation	249, 209, 204	⊢
	: , : , :
185	instantiation	249, 228, 205	⊢
	: , : , :
186	axiom		⊢
	proveit.logic.equality.equals_reflexivity
187	instantiation	249, 247, 206	⊢
	: , : , :
188	instantiation	224, 225, 214	⊢
	: , : , :
189	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
190	theorem		⊢
	proveit.numbers.addition.association
191	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
192	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
193	instantiation	207	⊢
	: , :
194	instantiation	249, 209, 208	⊢
	: , : , :
195	instantiation	249, 209, 210	⊢
	: , : , :
196	instantiation	211, 212, 213	⊢
	: , : , :
197	instantiation	215, 214, 216	⊢
	: , :
198	theorem		⊢
	proveit.logic.equality.not_equals_is_bool
199	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
200	instantiation	215, 251, 216	⊢
	: , :
201	theorem		⊢
	proveit.physics.quantum.circuits.qcircuit_output_part_neq
202	instantiation	217, 218, 219	⊢
	:
203	instantiation	220, 251, 221, 222, 223	, ,  ⊢
	: , : , :
204	instantiation	224, 225, 251	⊢
	: , : , :
205	instantiation	249, 240, 226	⊢
	: , : , :
206	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
207	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
208	instantiation	249, 228, 227	⊢
	: , : , :
209	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
210	instantiation	249, 228, 229	⊢
	: , : , :
211	axiom		⊢
	proveit.logic.equality.equals_transitivity
212	instantiation	230, 231	⊢
	: , : , :
213	theorem		⊢
	proveit.numbers.numerals.decimals.add_3_1
214	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
215	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
216	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
217	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
218	instantiation	249, 232, 245	⊢
	: , : , :
219	instantiation	233, 234, 235	⊢
	: , : , :
220	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_neq
221	assumption		⊢
222	assumption		⊢
223	assumption		⊢
224	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
225	instantiation	236, 237	⊢
	: , :
226	instantiation	238, 243	⊢
	:
227	instantiation	249, 240, 239	⊢
	: , : , :
228	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
229	instantiation	249, 240, 243	⊢
	: , : , :
230	axiom		⊢
	proveit.logic.equality.substitution
231	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_1
232	instantiation	241, 243, 244	⊢
	: , :
233	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
234	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
235	instantiation	242, 243, 244, 245	⊢
	: , : , :
236	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
237	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
238	theorem		⊢
	proveit.numbers.negation.int_closure
239	instantiation	249, 247, 246	⊢
	: , : , :
240	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
241	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
242	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
243	instantiation	249, 247, 248	⊢
	: , : , :
244	instantiation	249, 250, 251	⊢
	: , : , :
245	assumption		⊢
246	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
247	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
248	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
249	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
250	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
251	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
*equality replacement requirements