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