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	, , , , , ,  ⊢
	: , : , :
1	reference	4	⊢
2	instantiation	4, 5, 6	, , , , , ,  ⊢
	: , : , :
3	instantiation	13, 14, 61, 46, 15, 7	, , , , , ,  ⊢
	: , : , : , : , :
4	axiom		⊢
	proveit.logic.equality.equals_transitivity
5	instantiation	13, 8, 9, 59, 10, 11, 12	, , , , , ,  ⊢
	: , : , : , : , :
6	instantiation	13, 14, 57, 56, 15, 16	, , , , , ,  ⊢
	: , : , : , : , :
7	instantiation	42, 17, 18	, , , , ,  ⊢
	: , : , :
8	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
9	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
10	instantiation	19	⊢
	: , : , : , :
11	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
12	instantiation	42, 20, 21	, , , , ,  ⊢
	: , : , :
13	theorem		⊢
	proveit.physics.quantum.algebra.qmult_pulling_scalar_out_front
14	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
15	instantiation	67	⊢
	: , :
16	instantiation	42, 22, 23	, , , , ,  ⊢
	: , : , :
17	instantiation	28, 51, 52, 24, 30	, , , , ,  ⊢
	: , : , : , :
18	instantiation	54, 31, 25	⊢
	: , : , :
19	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
20	instantiation	28, 51, 52, 26, 30	, , , , ,  ⊢
	: , : , : , :
21	instantiation	54, 31, 27	⊢
	: , : , :
22	instantiation	28, 51, 52, 29, 30	, , , , ,  ⊢
	: , : , : , :
23	instantiation	54, 31, 32	⊢
	: , : , :
24	instantiation	35, 51, 52, 33	, , , ,  ⊢
	: , : , :
25	instantiation	37	⊢
	: , : , :
26	instantiation	35, 51, 52, 34	, , , ,  ⊢
	: , : , :
27	instantiation	37	⊢
	: , : , :
28	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_ket_in_QmultCodomain
29	instantiation	35, 51, 52, 36	, , , ,  ⊢
	: , : , :
30	assumption		⊢
31	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
32	instantiation	37	⊢
	: , : , :
33	instantiation	42, 38, 39	, , , ,  ⊢
	: , : , :
34	instantiation	42, 40, 41	, , , ,  ⊢
	: , : , :
35	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_is_linmap
36	instantiation	42, 43, 44	, , , ,  ⊢
	: , : , :
37	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
38	instantiation	49, 45, 51, 52, 53	, , , ,  ⊢
	: , : , : , :
39	instantiation	54, 55, 46	⊢
	: , : , :
40	instantiation	49, 47, 51, 52, 53	, , , ,  ⊢
	: , : , : , :
41	instantiation	54, 55, 48	⊢
	: , : , :
42	theorem		⊢
	proveit.logic.equality.sub_left_side_into
43	instantiation	49, 50, 51, 52, 53	, , , ,  ⊢
	: , : , : , :
44	instantiation	54, 55, 56	⊢
	: , : , :
45	instantiation	58, 57, 60, 59	,  ⊢
	: , : , :
46	instantiation	67	⊢
	: , :
47	instantiation	58, 61, 60, 57	,  ⊢
	: , : , :
48	instantiation	67	⊢
	: , :
49	theorem		⊢
	proveit.physics.quantum.algebra.qmult_complex_op_closure
50	instantiation	58, 59, 60, 61	,  ⊢
	: , : , :
51	instantiation	62, 65	⊢
	:
52	instantiation	62, 64	⊢
	:
53	instantiation	63, 64, 65, 66	, ,  ⊢
	: , : , :
54	axiom		⊢
	proveit.physics.quantum.algebra.multi_qmult_def
55	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
56	instantiation	67	⊢
	: , :
57	assumption		⊢
58	theorem		⊢
	proveit.physics.quantum.algebra.qmult_complex_ket_closure
59	assumption		⊢
60	theorem		⊢
	proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
61	assumption		⊢
62	theorem		⊢
	proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
63	theorem		⊢
	proveit.physics.quantum.algebra.qmult_matrix_is_linmap
64	assumption		⊢
65	assumption		⊢
66	assumption		⊢
67	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq