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*	⊢
	: , : , :
1	reference	110	⊢
2	instantiation	110, 5, 6	⊢
	: , : , :
3	instantiation	7, 199	⊢
	:
4	instantiation	133, 8, 9	⊢
	: , : , :
5	instantiation	10, 99	⊢
	:
6	axiom		⊢
	proveit.physics.quantum.QPE._Psi_def
7	theorem		⊢
	proveit.physics.quantum.QPE._psi_t_formula
8	instantiation	142, 11	⊢
	: , : , :
9	instantiation	133, 12, 13	⊢
	: , : , :
10	axiom		⊢
	proveit.physics.quantum.QPE._alpha_m_def
11	instantiation	14, 15, 16, 17	⊢
	: , : , : , :
12	instantiation	133, 18, 19	⊢
	: , : , :
13	instantiation	22, 41, 70, 20, 39, 21*	⊢
	: , : , :
14	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
15	instantiation	29, 70, 202, 124, 125, 23	⊢
	: , : , : , : , : , :
16	instantiation	26, 202, 70, 23	⊢
	: , : , : , : , :
17	instantiation	22, 191, 70, 38, 23	⊢
	: , : , :
18	instantiation	133, 24, 25	⊢
	: , : , :
19	instantiation	26, 202, 197, 70, 38, 39	⊢
	: , : , : , : , :
20	instantiation	129	⊢
	: , : , :
21	instantiation	27, 70, 28	⊢
	: , :
22	theorem		⊢
	proveit.physics.quantum.algebra.scalar_mult_factorization
23	instantiation	46, 82, 59, 48	⊢
	: , : , : , :
24	instantiation	29, 70, 202, 124, 125, 30	⊢
	: , : , : , : , : , :
25	instantiation	37, 197, 191, 124, 57, 38, 125, 31	⊢
	: , : , : , : , : , :
26	theorem		⊢
	proveit.physics.quantum.algebra.qmult_pulling_scalar_out_front
27	axiom		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
28	instantiation	93, 32, 44	⊢
	: , : , :
29	theorem		⊢
	proveit.physics.quantum.algebra.scalar_mult_absorption
30	instantiation	93, 39, 33	⊢
	: , : , :
31	instantiation	93, 34, 35	⊢
	: , : , :
32	instantiation	36, 82, 83, 47, 48	⊢
	: , : , : , :
33	instantiation	37, 202, 191, 124, 38, 125, 39	⊢
	: , : , : , : , : , :
34	instantiation	46, 82, 83, 40, 48	⊢
	: , : , : , :
35	instantiation	56, 41, 42	⊢
	: , : , :
36	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_ket_is_ket
37	theorem		⊢
	proveit.physics.quantum.algebra.qmult_disassociation
38	instantiation	139	⊢
	: , :
39	instantiation	93, 43, 44	⊢
	: , : , :
40	instantiation	81, 82, 83, 45	⊢
	: , : , :
41	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
42	instantiation	129	⊢
	: , : , :
43	instantiation	46, 82, 83, 47, 48	⊢
	: , : , : , :
44	instantiation	56, 191, 49	⊢
	: , : , :
45	instantiation	93, 50, 51	⊢
	: , : , :
46	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_ket_in_QmultCodomain
47	instantiation	81, 82, 83, 52	⊢
	: , : , :
48	modus ponens	53, 54	⊢
49	instantiation	139	⊢
	: , :
50	instantiation	58, 82, 83, 55, 59	⊢
	: , : , : , : , :
51	instantiation	56, 191, 57	⊢
	: , : , :
52	instantiation	58, 82, 83, 71, 59	⊢
	: , : , : , : , :
53	instantiation	60, 189, 66	⊢
	: , : , : , : , : , :
54	generalization	61	⊢
55	instantiation	81, 82, 83, 62	⊢
	: , : , :
56	axiom		⊢
	proveit.physics.quantum.algebra.multi_qmult_def
57	instantiation	139	⊢
	: , :
58	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_op_is_op
59	instantiation	63, 97, 64	⊢
	: , : , :
60	theorem		⊢
	proveit.linear_algebra.addition.summation_closure
61	instantiation	65, 66, 67, 68	⊢
	: , : , : , :
62	instantiation	69, 70, 82, 83, 71	⊢
	: , : , : , :
63	theorem		⊢
	proveit.physics.quantum.algebra.qmult_matrix_is_linmap
64	instantiation	161, 72, 73	⊢
	: , : , :
65	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
66	instantiation	74, 97	⊢
	:
67	instantiation	91, 75, 76	⊢
	: , :
68	instantiation	77, 199, 165	⊢
	: , :
69	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_complex_closure
70	instantiation	105, 78, 79, 80	⊢
	: , :
71	instantiation	81, 82, 83, 84	⊢
	: , : , :
72	instantiation	85, 97	⊢
	:
73	instantiation	86, 199	⊢
	:
74	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
75	instantiation	200, 168, 87	⊢
	: , : , :
76	instantiation	110, 88, 89	⊢
	: , : , :
77	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_in_register_space
78	instantiation	200, 168, 90	⊢
	: , : , :
79	instantiation	91, 160, 92	⊢
	: , :
80	instantiation	93, 94, 95	⊢
	: , : , :
81	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_is_linmap
82	instantiation	96, 97	⊢
	:
83	theorem		⊢
	proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
84	instantiation	98, 199, 99	⊢
	: , :
85	theorem		⊢
	proveit.linear_algebra.matrices.unitaries_are_matrices
86	theorem		⊢
	proveit.physics.quantum.QFT.invFT_is_unitary
87	instantiation	200, 149, 100	⊢
	: , : , :
88	instantiation	136, 113, 101	⊢
	: , :
89	instantiation	133, 102, 103	⊢
	: , : , :
90	instantiation	200, 179, 104	⊢
	: , : , :
91	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
92	instantiation	105, 145, 160, 120	⊢
	: , :
93	theorem		⊢
	proveit.logic.equality.sub_left_side_into
94	instantiation	106, 167, 107	⊢
	: , :
95	instantiation	142, 108	⊢
	: , : , :
96	theorem		⊢
	proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
97	instantiation	109, 197, 194	⊢
	: , :
98	theorem		⊢
	proveit.physics.quantum.algebra.num_bra_is_lin_map
99	assumption		⊢
100	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
101	instantiation	110, 111, 112	⊢
	: , : , :
102	instantiation	123, 202, 114, 124, 116, 125, 113, 137, 138, 127	⊢
	: , : , : , : , : , :
103	instantiation	123, 124, 197, 114, 125, 115, 116, 160, 128, 137, 138, 127	⊢
	: , : , : , : , : , :
104	instantiation	200, 188, 196	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.division.div_complex_closure
106	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
107	instantiation	200, 117, 118	⊢
	: , : , :
108	instantiation	119, 145, 160, 120, 121*	⊢
	: , :
109	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
110	theorem		⊢
	proveit.logic.equality.sub_right_side_into
111	instantiation	136, 122, 127	⊢
	: , :
112	instantiation	123, 124, 197, 202, 125, 126, 137, 138, 127	⊢
	: , : , : , : , : , :
113	instantiation	136, 160, 128	⊢
	: , :
114	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
115	instantiation	139	⊢
	: , :
116	instantiation	129	⊢
	: , : , :
117	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
118	instantiation	130, 173, 131	⊢
	: , :
119	theorem		⊢
	proveit.numbers.division.div_as_mult
120	instantiation	132, 191	⊢
	:
121	instantiation	133, 134, 135	⊢
	: , : , :
122	instantiation	136, 137, 138	⊢
	: , :
123	theorem		⊢
	proveit.numbers.multiplication.disassociation
124	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
125	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
126	instantiation	139	⊢
	: , :
127	instantiation	200, 168, 140	⊢
	: , : , :
128	instantiation	200, 168, 141	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
130	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
131	instantiation	200, 190, 199	⊢
	: , : , :
132	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
133	axiom		⊢
	proveit.logic.equality.equals_transitivity
134	instantiation	142, 143	⊢
	: , : , :
135	instantiation	144, 145, 146	⊢
	: , :
136	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
137	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
138	instantiation	200, 168, 147	⊢
	: , : , :
139	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
140	instantiation	200, 179, 148	⊢
	: , : , :
141	instantiation	200, 149, 150	⊢
	: , : , :
142	axiom		⊢
	proveit.logic.equality.substitution
143	instantiation	151, 152, 189, 153*	⊢
	: , :
144	theorem		⊢
	proveit.numbers.multiplication.commutation
145	instantiation	200, 168, 154	⊢
	: , : , :
146	instantiation	200, 168, 155	⊢
	: , : , :
147	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
148	instantiation	200, 188, 156	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
150	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
151	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
152	instantiation	200, 157, 158	⊢
	: , : , :
153	instantiation	159, 160	⊢
	:
154	instantiation	161, 162, 199	⊢
	: , : , :
155	instantiation	200, 179, 163	⊢
	: , : , :
156	instantiation	200, 164, 165	⊢
	: , : , :
157	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
158	instantiation	200, 166, 167	⊢
	: , : , :
159	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
160	instantiation	200, 168, 169	⊢
	: , : , :
161	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
162	instantiation	170, 171	⊢
	: , :
163	instantiation	200, 172, 173	⊢
	: , : , :
164	instantiation	174, 175, 176	⊢
	: , :
165	assumption		⊢
166	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
167	instantiation	200, 177, 178	⊢
	: , : , :
168	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
169	instantiation	200, 179, 180	⊢
	: , : , :
170	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
171	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
172	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
173	instantiation	181, 182, 183	⊢
	: , :
174	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
175	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
176	instantiation	184, 185, 186	⊢
	: , :
177	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
178	instantiation	200, 187, 191	⊢
	: , : , :
179	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
180	instantiation	200, 188, 193	⊢
	: , : , :
181	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
182	instantiation	200, 190, 189	⊢
	: , : , :
183	instantiation	200, 190, 191	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
185	instantiation	192, 193, 194	⊢
	: , :
186	instantiation	195, 196	⊢
	:
187	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
188	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
189	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
190	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
191	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
192	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
193	instantiation	200, 201, 197	⊢
	: , : , :
194	instantiation	200, 198, 199	⊢
	: , : , :
195	theorem		⊢
	proveit.numbers.negation.int_closure
196	instantiation	200, 201, 202	⊢
	: , : , :
197	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
198	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
199	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
200	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
201	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
202	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements