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	generalization	1	, , , ,  ⊢
1	instantiation	2, 3, 4	, , , , ,  ⊢
	: , : , :
2	theorem		⊢
	proveit.logic.equality.sub_left_side_into
3	instantiation	5, 6, 17, 7	, , , , ,  ⊢
	: , : , : , :
4	instantiation	8, 9, 10, 11	, , , , ,  ⊢
	: , : , : , :
5	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
6	instantiation	12, 23, 24, 33	⊢
	: , : , :
7	instantiation	13, 14, 15	, , , ,  ⊢
	: , : , :
8	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
9	instantiation	16, 17, 60, 31, 32, 33, 18, 35, 36, 37, 38	, , , , ,  ⊢
	: , : , : , : , : , : , : , : , : , :
10	instantiation	19	⊢
	:
11	instantiation	20, 21	, , , ,  ⊢
	: , :
12	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
13	theorem		⊢
	proveit.logic.equality.sub_right_side_into
14	instantiation	22, 23, 24, 33, 25, 35, 36, 37, 38	, , , ,  ⊢
	: , : , : , :
15	instantiation	26, 31, 60, 32, 33, 34, 35, 36, 37, 38	, , , ,  ⊢
	: , : , : , : , : , : , : , : , : , :
16	theorem		⊢
	proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod
17	assumption		⊢
18	instantiation	41	⊢
	: , :
19	axiom		⊢
	proveit.logic.equality.equals_reflexivity
20	theorem		⊢
	proveit.logic.equality.equals_reversal
21	instantiation	27, 28	, , , ,  ⊢
	: , : , :
22	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
23	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
24	instantiation	29	⊢
	: , : , : , :
25	instantiation	29	⊢
	: , : , : , :
26	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_association
27	axiom		⊢
	proveit.logic.equality.substitution
28	instantiation	30, 31, 60, 32, 33, 34, 35, 36, 37, 38	, , , ,  ⊢
	: , : , : , : , : , : , : , : , : , :
29	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
30	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_disassociation
31	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
32	instantiation	41	⊢
	: , :
33	instantiation	39, 40	⊢
	:
34	instantiation	41	⊢
	: , :
35	assumption		⊢
36	assumption		⊢
37	instantiation	42, 43	,  ⊢
	:
38	assumption		⊢
39	theorem		⊢
	proveit.linear_algebra.real_vec_set_is_vec_space
40	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
41	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
42	assumption		⊢
43	instantiation	44, 45, 46	⊢
	:
44	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
45	instantiation	61, 47, 59	⊢
	: , : , :
46	instantiation	48, 49	⊢
	: , :
47	instantiation	50, 57, 58	⊢
	: , :
48	theorem		⊢
	proveit.numbers.ordering.relax_less
49	instantiation	51, 52, 53	⊢
	: , : , :
50	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
51	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
52	instantiation	54, 55	⊢
	:
53	instantiation	56, 57, 58, 59	⊢
	: , : , :
54	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
55	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
56	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
57	instantiation	61, 62, 60	⊢
	: , : , :
58	instantiation	61, 62, 63	⊢
	: , : , :
59	assumption		⊢
60	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
61	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
62	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
63	theorem		⊢
	proveit.numbers.numerals.decimals.nat4