Expression of type ExprTuple

from the theory of proveit.linear_algebra.tensors

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import Conditional, ExprTuple, K, Lambda, V, b, i, k
from proveit.core_expr_types import U_1_to_i, W_1_to_k, a_1_to_i, c_1_to_k, d_1_to_i, e_1_to_k
from proveit.linear_algebra import TensorProd, VecSpaces
from proveit.logic import And, Equals, Forall, Implies, InSet
from proveit.numbers import Natural

# build up the expression from sub-expressions
expr = ExprTuple(Lambda([i, k], Conditional(Forall(instance_param_or_params = [U_1_to_i, V, W_1_to_k], instance_expr = Forall(instance_param_or_params = [a_1_to_i, c_1_to_k, d_1_to_i, e_1_to_k], instance_expr = Forall(instance_param_or_params = [b], instance_expr = Implies(Equals(TensorProd(a_1_to_i, c_1_to_k), TensorProd(d_1_to_i, e_1_to_k)).with_wrapping_at(2), Equals(TensorProd(a_1_to_i, b, c_1_to_k), TensorProd(d_1_to_i, b, e_1_to_k)).with_wrapping_at(2)).with_wrapping_at(2), domain = V), domains = [U_1_to_i, W_1_to_k, U_1_to_i, W_1_to_k]).with_wrapping(), domain = VecSpaces(K)).with_wrapping(), And(InSet(i, Natural), InSet(k, Natural)))))

expr:

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(\left(i, k\right) \mapsto \left\{\begin{array}{l}\forall_{U_{1}, U_{2}, \ldots, U_{i}, V, W_{1}, W_{2}, \ldots, W_{k} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)}~\\
\left[\begin{array}{l}\forall_{\left(a_{1} \in U_{1}\right), \left(a_{2} \in U_{2}\right), \ldots, \left(a_{i} \in U_{i}\right),\left(c_{1} \in W_{1}\right), \left(c_{2} \in W_{2}\right), \ldots, \left(c_{k} \in W_{k}\right),\left(d_{1} \in U_{1}\right), \left(d_{2} \in U_{2}\right), \ldots, \left(d_{i} \in U_{i}\right),\left(e_{1} \in W_{1}\right), \left(e_{2} \in W_{2}\right), \ldots, \left(e_{k} \in W_{k}\right)}~\\
\left[\forall_{b \in V}~\left(\begin{array}{c} \begin{array}{l} \left(\begin{array}{c} \begin{array}{l} \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i}{\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) =  \\ \left(d_{1} {\otimes}  d_{2} {\otimes}  \ldots {\otimes}  d_{i}{\otimes} e_{1} {\otimes}  e_{2} {\otimes}  \ldots {\otimes}  e_{k}\right) \end{array} \end{array}\right) \Rightarrow  \\ \left(\begin{array}{c} \begin{array}{l} \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i} {\otimes} b{\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) =  \\ \left(d_{1} {\otimes}  d_{2} {\otimes}  \ldots {\otimes}  d_{i} {\otimes} b{\otimes} e_{1} {\otimes}  e_{2} {\otimes}  \ldots {\otimes}  e_{k}\right) \end{array} \end{array}\right) \end{array} \end{array}\right)\right]\end{array}\right]\end{array} \textrm{ if } i \in \mathbb{N} ,  k \in \mathbb{N}\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	ExprTuple	1
1	Lambda	parameters: 2 body: 3
2	ExprTuple	100, 103
3	Conditional	value: 4 condition: 5
4	Operation	operator: 37 operand: 8
5	Operation	operator: 39 operands: 7
6	ExprTuple	8
7	ExprTuple	9, 10
8	Lambda	parameters: 11 body: 12
9	Operation	operator: 71 operands: 13
10	Operation	operator: 71 operands: 14
11	ExprTuple	15, 75, 16
12	Conditional	value: 17 condition: 18
13	ExprTuple	100, 19
14	ExprTuple	103, 19
15	ExprRange	lambda_map: 20 start_index: 102 end_index: 100
16	ExprRange	lambda_map: 21 start_index: 102 end_index: 103
17	Operation	operator: 37 operand: 24
18	Operation	operator: 39 operands: 23
19	Literal
20	Lambda	parameter: 113 body: 76
21	Lambda	parameter: 113 body: 77
22	ExprTuple	24
23	ExprTuple	25, 26, 27
24	Lambda	parameters: 28 body: 29
25	ExprRange	lambda_map: 30 start_index: 102 end_index: 100
26	Operation	operator: 42 operands: 31
27	ExprRange	lambda_map: 32 start_index: 102 end_index: 103
28	ExprTuple	92, 93, 94, 96
29	Conditional	value: 33 condition: 34
30	Lambda	parameter: 113 body: 35
31	ExprTuple	75, 49
32	Lambda	parameter: 113 body: 36
33	Operation	operator: 37 operand: 44
34	Operation	operator: 39 operands: 40
35	Operation	operator: 42 operands: 41
36	Operation	operator: 42 operands: 43
37	Literal
38	ExprTuple	44
39	Literal
40	ExprTuple	45, 46, 47, 48
41	ExprTuple	76, 49
42	Literal
43	ExprTuple	77, 49
44	Lambda	parameter: 95 body: 51
45	ExprRange	lambda_map: 52 start_index: 102 end_index: 100
46	ExprRange	lambda_map: 53 start_index: 102 end_index: 103
47	ExprRange	lambda_map: 54 start_index: 102 end_index: 100
48	ExprRange	lambda_map: 55 start_index: 102 end_index: 103
49	Operation	operator: 56 operand: 64
50	ExprTuple	95
51	Conditional	value: 58 condition: 59
52	Lambda	parameter: 113 body: 60
53	Lambda	parameter: 113 body: 61
54	Lambda	parameter: 113 body: 62
55	Lambda	parameter: 113 body: 63
56	Literal
57	ExprTuple	64
58	Operation	operator: 65 operands: 66
59	Operation	operator: 71 operands: 67
60	Operation	operator: 71 operands: 68
61	Operation	operator: 71 operands: 69
62	Operation	operator: 71 operands: 70
63	Operation	operator: 71 operands: 72
64	Variable
65	Literal
66	ExprTuple	73, 74
67	ExprTuple	95, 75
68	ExprTuple	104, 76
69	ExprTuple	105, 77
70	ExprTuple	106, 76
71	Literal
72	ExprTuple	107, 77
73	Operation	operator: 79 operands: 78
74	Operation	operator: 79 operands: 80
75	Variable
76	IndexedVar	variable: 81 index: 113
77	IndexedVar	variable: 82 index: 113
78	ExprTuple	83, 84
79	Literal
80	ExprTuple	85, 86
81	Variable
82	Variable
83	Operation	operator: 90 operands: 87
84	Operation	operator: 90 operands: 88
85	Operation	operator: 90 operands: 89
86	Operation	operator: 90 operands: 91
87	ExprTuple	92, 93
88	ExprTuple	94, 96
89	ExprTuple	92, 95, 93
90	Literal
91	ExprTuple	94, 95, 96
92	ExprRange	lambda_map: 97 start_index: 102 end_index: 100
93	ExprRange	lambda_map: 98 start_index: 102 end_index: 103
94	ExprRange	lambda_map: 99 start_index: 102 end_index: 100
95	Variable
96	ExprRange	lambda_map: 101 start_index: 102 end_index: 103
97	Lambda	parameter: 113 body: 104
98	Lambda	parameter: 113 body: 105
99	Lambda	parameter: 113 body: 106
100	Variable
101	Lambda	parameter: 113 body: 107
102	Literal
103	Variable
104	IndexedVar	variable: 108 index: 113
105	IndexedVar	variable: 109 index: 113
106	IndexedVar	variable: 110 index: 113
107	IndexedVar	variable: 111 index: 113
108	Variable
109	Variable
110	Variable
111	Variable
112	ExprTuple	113
113	Variable