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