| | step type | requirements | statement |
|---|
| 0 | instantiation | 1, 2, 3 |  ,  ,  ,  ,  ,  ,  ⊢  |
| |  :  ,  :  ,  :  |
| 1 | axiom | | ⊢  |
| | proveit.logic.equality.equals_transitivity |
| 2 | instantiation | 4, 5 | , , , , , ⊢  |
| |  :  , :  , :  |
| 3 | instantiation | 6, 7, 8, 18, 19, 9* | , , , , , , ⊢  |
| |  :  ,  :  , :  ,  :  ,  : |
| 4 | axiom | | ⊢  |
| | proveit.logic.equality.substitution |
| 5 | instantiation | 10, 19, 24, 26, 28, 29, 11, 31, 12, 13* | , , , , , ⊢  |
| | : , : ,  :  ,  :  ,  :  , :  ,  :  , :  ,  :  ,  : |
| 6 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled |
| 7 | instantiation | 20, 14, 15, 29 | ⊢  |
| | : , :  , :  |
| 8 | instantiation | 21, 14, 15, 29, 16, 31, 32, 33, 34, 35 | , , , , ⊢  |
| | : , : , : , :  |
| 9 | instantiation | 17, 18, 19 | , ⊢  |
| | : , : |
| 10 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod |
| 11 | instantiation | 20, 22, 27, 29 | ⊢  |
| | : , :  , :  |
| 12 | instantiation | 21, 22, 27, 29, 30, 32, 33, 34, 35 | , , , ⊢  |
| | : , : , : , :  |
| 13 | instantiation | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35 | , , , , ⊢  |
| | : , : ,  : , : , : , : , : , : , : , : |
| 14 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat5 |
| 15 | instantiation | 36 | ⊢  |
| | :  , : , : ,  : ,  : |
| 16 | instantiation | 36 | ⊢  |
| | :  , :  , :  , : , : |
| 17 | axiom | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult |
| 18 | instantiation | 37, 52, 38 | ⊢  |
| |  :  ,  : , : |
| 19 | assumption | | ⊢ |
| 20 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space |
| 21 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space |
| 22 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat4 |
| 23 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_disassociation |
| 24 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat1 |
| 25 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat4 |
| 26 | axiom | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.zero_in_nats |
| 27 | instantiation | 40 | ⊢  |
| | : , : , : , : |
| 28 | theorem | | ⊢  |
| | proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
| 29 | instantiation | 39, 49 | ⊢  |
| |  :  |
| 30 | instantiation | 40 | ⊢  |
| | : , : , : , : |
| 31 | instantiation | 45, 46, 41 | ⊢  |
| | :  , : , : |
| 32 | instantiation | 45, 46, 42 | ⊢  |
| | : , : , : |
| 33 | instantiation | 45, 46, 43 | ⊢  |
| | : , : , : |
| 34 | instantiation | 45, 46, 44 | ⊢  |
| | : , : , : |
| 35 | instantiation | 45, 46, 47 | ⊢  |
| | : , : , : |
| 36 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_5_typical_eq |
| 37 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
| 38 | assumption | | ⊢ |
| 39 | theorem | | ⊢  |
| | proveit.linear_algebra.complex_vec_set_is_vec_space |
| 40 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_4_typical_eq |
| 41 | assumption | | ⊢ |
| 42 | assumption | | ⊢ |
| 43 | assumption | | ⊢ |
| 44 | assumption | | ⊢ |
| 45 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.unfold_subset_eq |
| 46 | instantiation | 48, 49, 50 | ⊢  |
| |  : , : , : |
| 47 | assumption | | ⊢ |
| 48 | theorem | | ⊢  |
| | proveit.logic.sets.cartesian_products.cart_exp_subset_eq |
| 49 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat3 |
| 50 | instantiation | 51, 52 | ⊢  |
| | : , : |
| 51 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.relax_proper_subset |
| 52 | theorem | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.real_within_complex |
| *equality replacement requirements |
