| | step type | requirements | statement |
|---|
| 0 | instantiation | 1, 2, 3* |  ,  ,  ⊢  |
| |  :  ,  :  |
| 1 | reference | 20 | ⊢  |
| 2 | modus ponens | 4, 5 | , , ⊢  |
| 3 | instantiation | 12, 6, 7 | , , ⊢  |
| | : , :  ,  :  |
| 4 | instantiation | 8, 32, 69, 33, 9, 34 | ⊢  |
| |  :  ,  :  ,  :  ,  :  ,  : ,  :  ,  :  ,  :  ,  :  ,  :  |
| 5 | generalization | 10 | , , ⊢  |
| 6 | instantiation | 23, 11 | , ⊢  |
| |  :  , :  , :  |
| 7 | instantiation | 12, 13, 14, 15* | , , ⊢  |
| | : , :  , :  |
| 8 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_distribution_over_summation |
| 9 | instantiation | 16, 55, 56, 70 | ⊢  |
| | : , :  , :  |
| 10 | instantiation | 54, 55, 56, 70, 17, 18, 19 | , , ⊢  |
| | : , : , : , :  |
| 11 | instantiation | 20, 21 | , ⊢  |
| | : , : |
| 12 | axiom | | ⊢  |
| | proveit.logic.equality.equals_transitivity |
| 13 | instantiation | 31, 67, 33, 32, 34, 70, 58, 22 | , , ⊢  |
| | : ,  :  , : , : ,  : , :  ,  :  , : , : , :  |
| 14 | instantiation | 23, 24 | , , ⊢  |
| | :  , :  , :  |
| 15 | instantiation | 25, 26, 27, 61, 28* | , , ⊢  |
| | :  , :  , :  , : , : |
| 16 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space |
| 17 | instantiation | 62 | ⊢  |
| | :  , : |
| 18 | instantiation | 30, 70, 67, 58 | , ⊢  |
| | : , : , : , : |
| 19 | instantiation | 30, 70, 67, 71 | , ⊢  |
| | : , : , : , : |
| 20 | theorem | | ⊢ |
| | proveit.logic.equality.equals_reversal |
| 21 | modus ponens | 29, 59 | , ⊢  |
| 22 | instantiation | 30, 70, 67, 59 | , ⊢  |
| | : , : , : , :  |
| 23 | axiom | | ⊢  |
| | proveit.logic.equality.substitution |
| 24 | instantiation | 31, 67, 32, 33, 34, 70, 58, 59 | , , ⊢  |
| | : , : , : , : , : , : , : , :  , : , : |
| 25 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled |
| 26 | instantiation | 35, 42 | ⊢  |
| |  :  |
| 27 | instantiation | 44, 36, 37 | , ⊢  |
| |  :  ,  : , : |
| 28 | instantiation | 38, 61, 39* | ⊢  |
| | : , : |
| 29 | instantiation | 40, 69, 70, 67 | ⊢  |
| | : , : , : , : , : , : , : |
| 30 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.scalar_mult_closure |
| 31 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod |
| 32 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat1 |
| 33 | axiom | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.zero_in_nats |
| 34 | theorem | | ⊢  |
| | proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
| 35 | theorem | | ⊢  |
| | proveit.linear_algebra.complex_vec_set_is_vec_space |
| 36 | instantiation | 41, 42, 43 | ⊢  |
| |  : , : , : |
| 37 | instantiation | 44, 45, 46 | , ⊢  |
| | : , : , : |
| 38 | axiom | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult |
| 39 | instantiation | 47, 61, 69, 48*, 49* | ⊢  |
| | : , : , : |
| 40 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum |
| 41 | theorem | | ⊢  |
| | proveit.logic.sets.cartesian_products.cart_exp_subset_eq |
| 42 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat9 |
| 43 | instantiation | 50, 66 | ⊢  |
| | : , : |
| 44 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.unfold_subset_eq |
| 45 | instantiation | 51, 55, 52, 73, 53* | ⊢  |
| | : , : , :  |
| 46 | instantiation | 54, 55, 56, 70, 57, 58, 59 | , ⊢  |
| | : , : , : , :  |
| 47 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.product_of_posnat_powers |
| 48 | instantiation | 60, 61 | ⊢  |
| | : |
| 49 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.add_1_1 |
| 50 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.relax_proper_subset |
| 51 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp |
| 52 | instantiation | 62 | ⊢  |
| | :  , : |
| 53 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.mult_3_3 |
| 54 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space |
| 55 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat2 |
| 56 | instantiation | 62 | ⊢  |
| | : , : |
| 57 | instantiation | 62 | ⊢  |
| | : , : |
| 58 | assumption | | ⊢ |
| 59 | modus ponens | 63, 64 | ⊢  |
| 60 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.complex_x_to_first_power_is_x |
| 61 | instantiation | 65, 66, 67 | ⊢  |
| | : , : , : |
| 62 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
| 63 | instantiation | 68, 69, 70 | ⊢  |
| | : , : , : , : , : , : |
| 64 | generalization | 71 | ⊢  |
| 65 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
| 66 | theorem | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.real_within_complex |
| 67 | assumption | | ⊢ |
| 68 | theorem | | ⊢  |
| | proveit.linear_algebra.addition.summation_closure |
| 69 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat1 |
| 70 | instantiation | 72, 73 | ⊢  |
| | : |
| 71 | assumption | | ⊢ |
| 72 | theorem | | ⊢  |
| | proveit.linear_algebra.real_vec_set_is_vec_space |
| 73 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat3 |
| *equality replacement requirements |
