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