| step type | requirements | statement |
0 | instantiation | 1, 2, 3 | ⊢  |
| : , : , :  |
1 | theorem | | ⊢  |
| proveit.logic.equality.sub_left_side_into |
2 | instantiation | 4, 69, 66, 14, 35, 5 | ⊢  |
| : , : , : , : , :  |
3 | instantiation | 20, 6, 7 | ⊢  |
| : , : , :  |
4 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.proper_subset_of_superset |
5 | instantiation | 8, 69, 14, 9, 10, 11 | ⊢  |
| : , : , :  |
6 | instantiation | 20, 12, 13 | ⊢  |
| : , : , :  |
7 | instantiation | 33, 69, 66, 29, 14, 35, 31 | ⊢  |
| : , : , : , : , : , : , :  |
8 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.nonmembership_fold |
9 | instantiation | 16, 15 | ⊢  |
| : , :  |
10 | instantiation | 16, 17 | ⊢  |
| : , :  |
11 | instantiation | 26, 27, 18, 19 | ⊢  |
| : , :  |
12 | instantiation | 20, 21, 22 | ⊢  |
| : , : , :  |
13 | instantiation | 33, 66, 69, 29, 23, 24, 31 | ⊢  |
| : , : , : , : , : , : , :  |
14 | instantiation | 37 | ⊢  |
| : , : , :  |
15 | instantiation | 26, 66, 27, 25 | ⊢  |
| : , :  |
16 | theorem | | ⊢  |
| proveit.logic.equality.not_equals_symmetry |
17 | instantiation | 26, 30, 27, 28 | ⊢  |
| : , :  |
18 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat6 |
19 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.less_5_6 |
20 | axiom | | ⊢  |
| proveit.logic.equality.equals_transitivity |
21 | instantiation | 33, 29, 34, 30, 31, 32 | ⊢  |
| : , : , : , : , : , : , :  |
22 | instantiation | 33, 34, 66, 35, 36 | ⊢  |
| : , : , : , : , : , : , :  |
23 | instantiation | 44 | ⊢  |
| : , :  |
24 | instantiation | 37 | ⊢  |
| : , : , :  |
25 | instantiation | 38, 57, 39, 59, 40, 41*, 42* | ⊢  |
| : , : , :  |
26 | theorem | | ⊢  |
| proveit.numbers.ordering.less_is_not_eq_nat |
27 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat5 |
28 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.less_4_5 |
29 | axiom | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.zero_in_nats |
30 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat4 |
31 | theorem | | ⊢  |
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
32 | instantiation | 43 | ⊢  |
| : , : , : , :  |
33 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.leftward_permutation |
34 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat1 |
35 | instantiation | 44 | ⊢  |
| : , :  |
36 | instantiation | 44 | ⊢  |
| : , :  |
37 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq |
38 | theorem | | ⊢  |
| proveit.numbers.addition.strong_bound_via_left_term_bound |
39 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.zero_is_real |
40 | instantiation | 45, 46 | ⊢  |
| :  |
41 | instantiation | 49, 47, 48 | ⊢  |
| : , : , :  |
42 | instantiation | 49, 50, 51 | ⊢  |
| : , : , :  |
43 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_4_typical_eq |
44 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
45 | theorem | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos |
46 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat3 |
47 | instantiation | 52, 55 | ⊢  |
| :  |
48 | instantiation | 54, 55, 53 | ⊢  |
| : , :  |
49 | theorem | | ⊢  |
| proveit.logic.equality.sub_right_side_into |
50 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.add_2_3 |
51 | instantiation | 54, 55, 56 | ⊢  |
| : , :  |
52 | theorem | | ⊢  |
| proveit.numbers.addition.elim_zero_right |
53 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.zero_is_complex |
54 | theorem | | ⊢  |
| proveit.numbers.addition.commutation |
55 | instantiation | 67, 58, 57 | ⊢  |
| : , : , :  |
56 | instantiation | 67, 58, 59 | ⊢  |
| : , : , :  |
57 | instantiation | 67, 61, 60 | ⊢  |
| : , : , :  |
58 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_within_complex |
59 | instantiation | 67, 61, 62 | ⊢  |
| : , : , :  |
60 | instantiation | 67, 64, 63 | ⊢  |
| : , : , :  |
61 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_within_real |
62 | instantiation | 67, 64, 65 | ⊢  |
| : , : , :  |
63 | instantiation | 67, 68, 66 | ⊢  |
| : , : , :  |
64 | theorem | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.int_within_rational |
65 | instantiation | 67, 68, 69 | ⊢  |
| : , : , :  |
66 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat2 |
67 | theorem | | ⊢  |
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
68 | theorem | | ⊢  |
| proveit.numbers.number_sets.integers.nat_within_int |
69 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat3 |
*equality replacement requirements |