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*	,  ⊢
	: , : , : , :
1	theorem		⊢
	proveit.linear_algebra.addition.norm_of_sum_of_orthogonal_pair
2	reference	8	⊢
3	reference	16	⊢
4	instantiation	7, 8, 32, 17	,  ⊢
	: , : , : , :
5	instantiation	63, 9, 10	,  ⊢
	: , : , :
6	instantiation	11, 15, 32, 17, 12*	,  ⊢
	: , : , : , :
7	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
8	instantiation	13, 23	⊢
	:
9	instantiation	14, 15, 32, 16, 17	,  ⊢
	: , : , : , : , :
10	instantiation	60, 18, 19	,  ⊢
	: , : , :
11	theorem		⊢
	proveit.linear_algebra.inner_products.scaled_norm
12	instantiation	60, 20, 21	,  ⊢
	: , : , :
13	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
14	theorem		⊢
	proveit.linear_algebra.inner_products.inner_prod_scalar_mult_right
15	instantiation	22, 23	⊢
	:
16	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_in_qubit_space
17	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_in_qubit_space
18	instantiation	52, 24	⊢
	: , : , :
19	instantiation	25, 32, 26, 27*	,  ⊢
	: , :
20	instantiation	52, 28	,  ⊢
	: , : , :
21	instantiation	29, 30	⊢
	:
22	theorem		⊢
	proveit.linear_algebra.inner_products.complex_vec_set_is_inner_prod_space
23	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
24	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_and_one_have_zero_inner_prod
25	axiom		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
26	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
27	instantiation	31, 32	,  ⊢
	:
28	instantiation	33, 34, 35*	,  ⊢
	:
29	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
30	instantiation	36, 37, 38	⊢
	: , : , :
31	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
32	instantiation	98, 39, 40	,  ⊢
	: , :
33	theorem		⊢
	proveit.numbers.absolute_value.complex_unit_length
34	instantiation	63, 41, 42	,  ⊢
	: , : , :
35	instantiation	43, 44	,  ⊢
	: , :
36	theorem		⊢
	proveit.logic.equality.sub_left_side_into
37	instantiation	128, 108, 45	⊢
	: , : , :
38	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_norm
39	instantiation	128, 108, 46	⊢
	: , : , :
40	instantiation	63, 47, 48	,  ⊢
	: , : , :
41	instantiation	94, 84, 49	,  ⊢
	: , :
42	instantiation	60, 50, 51	,  ⊢
	: , : , :
43	theorem		⊢
	proveit.logic.equality.equals_reversal
44	instantiation	52, 53	,  ⊢
	: , : , :
45	instantiation	128, 111, 54	⊢
	: , : , :
46	instantiation	128, 101, 55	⊢
	: , : , :
47	instantiation	89, 66, 56	,  ⊢
	: , :
48	instantiation	60, 57, 58	,  ⊢
	: , : , :
49	instantiation	94, 59, 93	,  ⊢
	: , :
50	instantiation	79, 127, 113, 80, 73, 81, 66, 91, 83	,  ⊢
	: , : , : , : , : , :
51	instantiation	79, 80, 113, 81, 72, 73, 99, 77, 91, 83	,  ⊢
	: , : , : , : , : , :
52	axiom		⊢
	proveit.logic.equality.substitution
53	instantiation	60, 61, 62	,  ⊢
	: , : , :
54	instantiation	128, 114, 123	⊢
	: , : , :
55	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
56	instantiation	63, 64, 65	,  ⊢
	: , : , :
57	instantiation	79, 127, 67, 80, 68, 81, 66, 90, 91, 83	,  ⊢
	: , : , : , : , : , :
58	instantiation	79, 80, 113, 67, 81, 72, 68, 99, 77, 90, 91, 83	,  ⊢
	: , : , : , : , : , :
59	instantiation	69, 104, 70	,  ⊢
	: , :
60	axiom		⊢
	proveit.logic.equality.equals_transitivity
61	instantiation	71, 80, 113, 81, 72, 73, 99, 77, 90, 91, 83	,  ⊢
	: , : , : , : , : , : , :
62	instantiation	74, 127, 75, 80, 76, 81, 90, 99, 77, 91, 83	,  ⊢
	: , : , : , : , : , :
63	theorem		⊢
	proveit.logic.equality.sub_right_side_into
64	instantiation	89, 78, 83	,  ⊢
	: , :
65	instantiation	79, 80, 113, 127, 81, 82, 90, 91, 83	,  ⊢
	: , : , : , : , : , :
66	instantiation	128, 108, 84	⊢
	: , : , :
67	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
68	instantiation	85	⊢
	: , : , :
69	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
70	instantiation	86, 87	,  ⊢
	:
71	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
72	instantiation	92	⊢
	: , :
73	instantiation	92	⊢
	: , :
74	theorem		⊢
	proveit.numbers.multiplication.association
75	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
76	instantiation	88	⊢
	: , : , : , :
77	instantiation	128, 108, 95	⊢
	: , : , :
78	instantiation	89, 90, 91	,  ⊢
	: , :
79	theorem		⊢
	proveit.numbers.multiplication.disassociation
80	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
81	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
82	instantiation	92	⊢
	: , :
83	instantiation	128, 108, 93	⊢
	: , : , :
84	instantiation	94, 104, 95	⊢
	: , :
85	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
86	theorem		⊢
	proveit.numbers.negation.nat_closure
87	instantiation	96, 115, 97	,  ⊢
	:
88	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
89	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
90	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
91	instantiation	98, 99, 100	,  ⊢
	: , :
92	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
93	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
94	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
95	instantiation	128, 101, 102	⊢
	: , : , :
96	theorem		⊢
	proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
97	instantiation	103, 119, 120, 117	,  ⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
99	instantiation	128, 108, 104	⊢
	: , : , :
100	instantiation	105, 106	,  ⊢
	:
101	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
102	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
103	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
104	instantiation	128, 111, 107	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.negation.complex_closure
106	instantiation	128, 108, 109	,  ⊢
	: , : , :
107	instantiation	128, 114, 110	⊢
	: , : , :
108	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
109	instantiation	128, 111, 112	,  ⊢
	: , : , :
110	instantiation	128, 126, 113	⊢
	: , : , :
111	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
112	instantiation	128, 114, 115	,  ⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
114	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
115	instantiation	128, 116, 117	,  ⊢
	: , : , :
116	instantiation	118, 119, 120	⊢
	: , :
117	assumption		⊢
118	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
119	instantiation	121, 122, 123	⊢
	: , :
120	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
121	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
122	instantiation	124, 125	⊢
	:
123	instantiation	128, 126, 127	⊢
	: , : , :
124	theorem		⊢
	proveit.numbers.negation.int_closure
125	instantiation	128, 129, 130	⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
127	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
128	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
129	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
130	assumption		⊢
*equality replacement requirements