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	20	⊢
2	instantiation	20, 4, 5	, , ,  ⊢
	: , : , :
3	instantiation	34, 6	,  ⊢
	: , : , :
4	instantiation	20, 7, 8	,  ⊢
	: , : , :
5	instantiation	10, 9	, , ,  ⊢
	: , :
6	instantiation	10, 11	,  ⊢
	: , :
7	instantiation	20, 12, 13	,  ⊢
	: , : , :
8	instantiation	34, 14, 24*, 15*	,  ⊢
	: , : , :
9	modus ponens	16, 17	, , ,  ⊢
10	theorem		⊢
	proveit.logic.equality.equals_reversal
11	modus ponens	18, 19	,  ⊢
12	instantiation	20, 21, 22	,  ⊢
	: , : , :
13	instantiation	34, 23, 37*, 24*	,  ⊢
	: , : , :
14	modus ponens	25, 26	,  ⊢
15	instantiation	49, 99	⊢
	: , :
16	instantiation	27, 59, 53, 63	,  ⊢
	: , : , : , : , : , : , : , :
17	modus ponens	28, 29	,  ⊢
18	instantiation	30, 100, 59, 74, 53, 75	⊢
	: , : , : , : , : , : , : , : , : , : , :
19	generalization	31	,  ⊢
20	axiom		⊢
	proveit.logic.equality.equals_transitivity
21	instantiation	34, 32, 33*, 36*	,  ⊢
	: , : , :
22	instantiation	34, 35, 36*, 37*	,  ⊢
	: , : , :
23	modus ponens	38, 39	,  ⊢
24	instantiation	49, 99	⊢
	: , :
25	instantiation	58, 59	⊢
	: , : , : , : , : , : , :
26	generalization	40	,  ⊢
27	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum_with_scalar_mult
28	instantiation	41, 59, 53	⊢
	: , : , : , : , : , :
29	generalization	43	,  ⊢
30	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_distribution_over_summation_with_scalar_mult
31	instantiation	42, 43, 44	, ,  ⊢
	: , : , :
32	modus ponens	45, 46	,  ⊢
33	instantiation	49, 99	⊢
	: , :
34	axiom		⊢
	proveit.logic.equality.substitution
35	modus ponens	47, 48	,  ⊢
36	instantiation	49, 99	⊢
	: , :
37	instantiation	49, 99	⊢
	: , :
38	instantiation	58, 59	⊢
	: , : , : , : , : , : , :
39	generalization	50	,  ⊢
40	instantiation	61, 100, 104, 74, 76, 75, 51, 79, 80	, ,  ⊢
	: , : , : , : , : , :
41	theorem		⊢
	proveit.linear_algebra.addition.summation_closure
42	theorem		⊢
	proveit.logic.equality.sub_left_side_into
43	instantiation	52, 53, 56, 54	, ,  ⊢
	: , : , : , :
44	instantiation	55, 56, 100, 74, 75, 68, 70, 71	, ,  ⊢
	: , : , : , : , : , : , : , : , : , :
45	instantiation	58, 59	⊢
	: , : , : , : , : , : , :
46	generalization	57	,  ⊢
47	instantiation	58, 59	⊢
	: , : , : , : , : , : , :
48	generalization	60	,  ⊢
49	theorem		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
50	instantiation	61, 74, 104, 75, 62, 76, 78, 77, 79, 80	, ,  ⊢
	: , : , : , : , : , :
51	instantiation	105, 87, 63	,  ⊢
	: , : , :
52	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
53	instantiation	64, 66, 67, 68	⊢
	: , : , :
54	instantiation	65, 66, 67, 68, 69, 70, 71	,  ⊢
	: , : , : , :
55	theorem		⊢
	proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod
56	instantiation	81, 90, 88	⊢
	: , :
57	instantiation	73, 74, 104, 100, 75, 72, 78, 79, 77, 80	, ,  ⊢
	: , : , : , : , : , : , :
58	theorem		⊢
	proveit.core_expr_types.lambda_maps.general_lambda_substitution
59	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
60	instantiation	73, 74, 100, 104, 75, 76, 77, 78, 79, 80	, ,  ⊢
	: , : , : , : , : , : , :
61	theorem		⊢
	proveit.numbers.multiplication.association
62	instantiation	84	⊢
	: , :
63	instantiation	81, 86, 85	,  ⊢
	: , :
64	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
65	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
66	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
67	instantiation	84	⊢
	: , :
68	instantiation	82, 83	⊢
	:
69	instantiation	84	⊢
	: , :
70	assumption		⊢
71	assumption		⊢
72	instantiation	84	⊢
	: , :
73	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
74	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
75	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
76	instantiation	84	⊢
	: , :
77	instantiation	105, 87, 85	⊢
	: , : , :
78	instantiation	105, 87, 86	⊢
	: , : , :
79	instantiation	105, 87, 90	⊢
	: , : , :
80	instantiation	105, 87, 88	⊢
	: , : , :
81	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
82	theorem		⊢
	proveit.linear_algebra.real_vec_set_is_vec_space
83	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
84	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
85	assumption		⊢
86	assumption		⊢
87	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
88	instantiation	89, 90, 91	⊢
	: , :
89	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
90	instantiation	105, 93, 92	⊢
	: , : , :
91	instantiation	105, 93, 94	⊢
	: , : , :
92	instantiation	105, 96, 95	⊢
	: , : , :
93	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
94	instantiation	105, 96, 97	⊢
	: , : , :
95	instantiation	105, 98, 99	⊢
	: , : , :
96	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
97	instantiation	105, 106, 100	⊢
	: , : , :
98	instantiation	101, 102, 103	⊢
	: , :
99	assumption		⊢
100	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
101	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
102	instantiation	105, 106, 104	⊢
	: , : , :
103	instantiation	105, 106, 107	⊢
	: , : , :
104	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
105	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
106	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
107	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
*equality replacement requirements