OAI/RepresentationTheory/UniversalSquare/Semigroup/SemigroupLocalLeaves.lean

GitHub source file

343 declarations, 0 contain sorry, 0 declared as axioms

Semigroup Local Leaves.

  1. lemma OAI.UniversalTensorSquare.sg0 line 18
  2. lemma OAI.UniversalTensorSquare.sg1 line 21
  3. lemma OAI.UniversalTensorSquare.sg2 line 24
  4. lemma OAI.UniversalTensorSquare.sg3 line 27
  5. lemma OAI.UniversalTensorSquare.sg4 line 30
  6. lemma OAI.UniversalTensorSquare.sg5 line 41
  7. lemma OAI.UniversalTensorSquare.sg6 line 52
  8. lemma OAI.UniversalTensorSquare.sg7 line 55
  9. lemma OAI.UniversalTensorSquare.sg8 line 58
  10. lemma OAI.UniversalTensorSquare.sg9 line 61
  11. lemma OAI.UniversalTensorSquare.sg11 line 65
  12. lemma OAI.UniversalTensorSquare.sg12 line 69
  13. lemma OAI.UniversalTensorSquare.sg13 line 72
  14. lemma OAI.UniversalTensorSquare.sg14 line 76
  15. lemma OAI.UniversalTensorSquare.sg15 line 80
  16. lemma OAI.UniversalTensorSquare.sg16 line 83
  17. lemma OAI.UniversalTensorSquare.sg18 line 87
  18. lemma OAI.UniversalTensorSquare.sg19 line 91
  19. lemma OAI.UniversalTensorSquare.sg20 line 94
  20. lemma OAI.UniversalTensorSquare.sg21 line 97
  21. lemma OAI.UniversalTensorSquare.sg25 line 100
  22. lemma OAI.UniversalTensorSquare.sg26 line 103
  23. lemma OAI.UniversalTensorSquare.sg27 line 107
  24. lemma OAI.UniversalTensorSquare.sg28 line 111
  25. lemma OAI.UniversalTensorSquare.sg29 line 115
  26. lemma OAI.UniversalTensorSquare.sg30 line 119
  27. lemma OAI.UniversalTensorSquare.sg31 line 123
  28. lemma OAI.UniversalTensorSquare.sg32 line 126
  29. lemma OAI.UniversalTensorSquare.sg33 line 137
  30. lemma OAI.UniversalTensorSquare.sg34 line 148
  31. lemma OAI.UniversalTensorSquare.sg35 line 159
  32. lemma OAI.UniversalTensorSquare.sg36 line 170
  33. lemma OAI.UniversalTensorSquare.sg37 line 181
  34. lemma OAI.UniversalTensorSquare.sg38 line 192
  35. lemma OAI.UniversalTensorSquare.sg39 line 195
  36. lemma OAI.UniversalTensorSquare.sg40 line 199
  37. lemma OAI.UniversalTensorSquare.sg41 line 203
  38. lemma OAI.UniversalTensorSquare.sg42 line 207
  39. lemma OAI.UniversalTensorSquare.sg43 line 211
  40. lemma OAI.UniversalTensorSquare.sg44 line 215
  41. lemma OAI.UniversalTensorSquare.sg48 line 218
  42. lemma OAI.UniversalTensorSquare.sg49 line 221
  43. lemma OAI.UniversalTensorSquare.sg50 line 224
  44. lemma OAI.UniversalTensorSquare.sg54 line 227
  45. lemma OAI.UniversalTensorSquare.sg55 line 230
  46. lemma OAI.UniversalTensorSquare.sg56 line 234
  47. lemma OAI.UniversalTensorSquare.sg57 line 238
  48. lemma OAI.UniversalTensorSquare.sg58 line 242
  49. lemma OAI.UniversalTensorSquare.sg59 line 246
  50. lemma OAI.UniversalTensorSquare.sg60 line 250
  51. lemma OAI.UniversalTensorSquare.sg61 line 254
  52. lemma OAI.UniversalTensorSquare.sg62 line 257
  53. lemma OAI.UniversalTensorSquare.sg64 line 261
  54. lemma OAI.UniversalTensorSquare.sg65 line 265
  55. lemma OAI.UniversalTensorSquare.sg74 line 268
  56. lemma OAI.UniversalTensorSquare.sg75 line 279
  57. lemma OAI.UniversalTensorSquare.sg76 line 290
  58. lemma OAI.UniversalTensorSquare.sg77 line 301
  59. lemma OAI.UniversalTensorSquare.sg78 line 312
  60. lemma OAI.UniversalTensorSquare.sg79 line 323
  61. lemma OAI.UniversalTensorSquare.sg80 line 334
  62. lemma OAI.UniversalTensorSquare.sg81 line 345
  63. lemma OAI.UniversalTensorSquare.sg82 line 356
  64. lemma OAI.UniversalTensorSquare.sg83 line 367
  65. lemma OAI.UniversalTensorSquare.sg85 line 371
  66. lemma OAI.UniversalTensorSquare.sg86 line 375
  67. lemma OAI.UniversalTensorSquare.sg96 line 378
  68. lemma OAI.UniversalTensorSquare.sg97 line 381
  69. lemma OAI.UniversalTensorSquare.sg98 line 385
  70. lemma OAI.UniversalTensorSquare.sg99 line 389
  71. lemma OAI.UniversalTensorSquare.sg100 line 393
  72. lemma OAI.UniversalTensorSquare.sg101 line 397
  73. lemma OAI.UniversalTensorSquare.sg102 line 401
  74. lemma OAI.UniversalTensorSquare.sg103 line 405
  75. lemma OAI.UniversalTensorSquare.sg107 line 408
  76. lemma OAI.UniversalTensorSquare.sg108 line 411
  77. lemma OAI.UniversalTensorSquare.sg109 line 414
  78. lemma OAI.UniversalTensorSquare.sg113 line 417
  79. lemma OAI.UniversalTensorSquare.sg122 line 420
  80. lemma OAI.UniversalTensorSquare.sg123 line 423
  81. lemma OAI.UniversalTensorSquare.sg124 line 427
  82. lemma OAI.UniversalTensorSquare.sg125 line 431
  83. lemma OAI.UniversalTensorSquare.sg126 line 435
  84. lemma OAI.UniversalTensorSquare.sg127 line 439
  85. lemma OAI.UniversalTensorSquare.sg128 line 443
  86. lemma OAI.UniversalTensorSquare.sg129 line 447
  87. lemma OAI.UniversalTensorSquare.sg130 line 451
  88. lemma OAI.UniversalTensorSquare.sg131 line 455
  89. lemma OAI.UniversalTensorSquare.sg141 line 458
  90. lemma OAI.UniversalTensorSquare.sg178 line 461
  91. lemma OAI.UniversalTensorSquare.sg179 line 472
  92. lemma OAI.UniversalTensorSquare.sg180 line 483
  93. lemma OAI.UniversalTensorSquare.sg181 line 494
  94. lemma OAI.UniversalTensorSquare.sg182 line 505
  95. lemma OAI.UniversalTensorSquare.sg183 line 516
  96. lemma OAI.UniversalTensorSquare.sg184 line 527
  97. lemma OAI.UniversalTensorSquare.sg185 line 538
  98. lemma OAI.UniversalTensorSquare.sg186 line 549
  99. lemma OAI.UniversalTensorSquare.sg187 line 560
  100. lemma OAI.UniversalTensorSquare.sg188 line 571
  101. lemma OAI.UniversalTensorSquare.sg189 line 582
  102. lemma OAI.UniversalTensorSquare.sg190 line 593
  103. lemma OAI.UniversalTensorSquare.sg191 line 604
  104. lemma OAI.UniversalTensorSquare.sg192 line 615
  105. lemma OAI.UniversalTensorSquare.sg206 line 618
  106. lemma OAI.UniversalTensorSquare.sg207 line 621
  107. lemma OAI.UniversalTensorSquare.sg208 line 625
  108. lemma OAI.UniversalTensorSquare.sg209 line 629
  109. lemma OAI.UniversalTensorSquare.sg210 line 633
  110. lemma OAI.UniversalTensorSquare.sg211 line 637
  111. lemma OAI.UniversalTensorSquare.sg212 line 641
  112. lemma OAI.UniversalTensorSquare.sg213 line 645
  113. lemma OAI.UniversalTensorSquare.sg214 line 649
  114. lemma OAI.UniversalTensorSquare.sg215 line 653
  115. lemma OAI.UniversalTensorSquare.sg216 line 657
  116. lemma OAI.UniversalTensorSquare.sg217 line 661
  117. lemma OAI.UniversalTensorSquare.sg226 line 664
  118. lemma OAI.UniversalTensorSquare.sg234 line 667
  119. lemma OAI.UniversalTensorSquare.sg235 line 670
  120. lemma OAI.UniversalTensorSquare.sg238 line 673
  121. lemma OAI.UniversalTensorSquare.sg248 line 676
  122. lemma OAI.UniversalTensorSquare.sg249 line 679
  123. lemma OAI.UniversalTensorSquare.sg251 line 683
  124. lemma OAI.UniversalTensorSquare.sg253 line 687
  125. lemma OAI.UniversalTensorSquare.sg256 line 691
  126. lemma OAI.UniversalTensorSquare.sg257 line 695
  127. lemma OAI.UniversalTensorSquare.sg259 line 699
  128. lemma OAI.UniversalTensorSquare.sg269 line 703
  129. lemma OAI.UniversalTensorSquare.sg306 line 706
  130. lemma OAI.UniversalTensorSquare.sg330 line 710
  131. lemma OAI.UniversalTensorSquare.sg331 line 721
  132. lemma OAI.UniversalTensorSquare.sg332 line 732
  133. lemma OAI.UniversalTensorSquare.sg333 line 743
  134. lemma OAI.UniversalTensorSquare.sg334 line 754
  135. lemma OAI.UniversalTensorSquare.sg335 line 765
  136. lemma OAI.UniversalTensorSquare.sg336 line 776
  137. lemma OAI.UniversalTensorSquare.sg337 line 787
  138. lemma OAI.UniversalTensorSquare.sg338 line 798
  139. lemma OAI.UniversalTensorSquare.sg339 line 809
  140. lemma OAI.UniversalTensorSquare.sg340 line 820
  141. lemma OAI.UniversalTensorSquare.sg341 line 831
  142. lemma OAI.UniversalTensorSquare.sg342 line 842
  143. lemma OAI.UniversalTensorSquare.sg343 line 853
  144. lemma OAI.UniversalTensorSquare.sg344 line 864
  145. lemma OAI.UniversalTensorSquare.sg345 line 875
  146. lemma OAI.UniversalTensorSquare.sg346 line 886
  147. lemma OAI.UniversalTensorSquare.sg347 line 897
  148. lemma OAI.UniversalTensorSquare.sg366 line 908
  149. lemma OAI.UniversalTensorSquare.sg367 line 912
  150. lemma OAI.UniversalTensorSquare.sg369 line 916
  151. lemma OAI.UniversalTensorSquare.sg401 line 920
  152. lemma OAI.UniversalTensorSquare.sg403 line 924
  153. lemma OAI.UniversalTensorSquare.sg404 line 928
  154. lemma OAI.UniversalTensorSquare.sg405 line 932
  155. lemma OAI.UniversalTensorSquare.sg406 line 936
  156. lemma OAI.UniversalTensorSquare.sg408 line 940
  157. lemma OAI.UniversalTensorSquare.sg409 line 944
  158. lemma OAI.UniversalTensorSquare.sg410 line 948
  159. lemma OAI.UniversalTensorSquare.sg411 line 952
  160. lemma OAI.UniversalTensorSquare.sg412 line 956
  161. lemma OAI.UniversalTensorSquare.sg421 line 960
  162. lemma OAI.UniversalTensorSquare.sg426 line 963
  163. lemma OAI.UniversalTensorSquare.sg427 line 966
  164. lemma OAI.UniversalTensorSquare.sg431 line 969
  165. lemma OAI.UniversalTensorSquare.sg445 line 972
  166. lemma OAI.UniversalTensorSquare.sg446 line 975
  167. lemma OAI.UniversalTensorSquare.sg454 line 979
  168. lemma OAI.UniversalTensorSquare.sg474 line 982
  169. lemma OAI.UniversalTensorSquare.sg509 line 985
  170. lemma OAI.UniversalTensorSquare.sg516 line 988
  171. lemma OAI.UniversalTensorSquare.sg586 line 992
  172. lemma OAI.UniversalTensorSquare.sg656 line 996
  173. lemma OAI.UniversalTensorSquare.sg657 line 1000
  174. lemma OAI.UniversalTensorSquare.sg658 line 1004
  175. lemma OAI.UniversalTensorSquare.sg659 line 1008
  176. lemma OAI.UniversalTensorSquare.sg660 line 1012
  177. lemma OAI.UniversalTensorSquare.sg661 line 1016
  178. lemma OAI.UniversalTensorSquare.sg662 line 1020
  179. lemma OAI.UniversalTensorSquare.sg663 line 1024
  180. lemma OAI.UniversalTensorSquare.sg664 line 1028
  181. lemma OAI.UniversalTensorSquare.sg665 line 1032
  182. lemma OAI.UniversalTensorSquare.sg666 line 1036
  183. lemma OAI.UniversalTensorSquare.sg667 line 1040
  184. lemma OAI.UniversalTensorSquare.sg668 line 1044
  185. lemma OAI.UniversalTensorSquare.sg669 line 1048
  186. lemma OAI.UniversalTensorSquare.sg670 line 1052
  187. lemma OAI.UniversalTensorSquare.sg671 line 1056
  188. lemma OAI.UniversalTensorSquare.sg672 line 1060
  189. lemma OAI.UniversalTensorSquare.sg718 line 1063
  190. lemma OAI.UniversalTensorSquare.sg720 line 1066
  191. lemma OAI.UniversalTensorSquare.sg730 line 1069
  192. lemma OAI.UniversalTensorSquare.sg757 line 1072
  193. lemma OAI.UniversalTensorSquare.sg789 line 1075
  194. lemma OAI.UniversalTensorSquare.sg849 line 1078
  195. lemma OAI.UniversalTensorSquare.sg850 line 1089
  196. lemma OAI.UniversalTensorSquare.sg851 line 1100
  197. lemma OAI.UniversalTensorSquare.sg852 line 1111
  198. lemma OAI.UniversalTensorSquare.sg853 line 1122
  199. lemma OAI.UniversalTensorSquare.sg854 line 1133
  200. lemma OAI.UniversalTensorSquare.sg855 line 1144
  201. lemma OAI.UniversalTensorSquare.sg856 line 1155
  202. lemma OAI.UniversalTensorSquare.sg857 line 1166
  203. lemma OAI.UniversalTensorSquare.sg858 line 1177
  204. lemma OAI.UniversalTensorSquare.sg859 line 1188
  205. lemma OAI.UniversalTensorSquare.sg860 line 1199
  206. lemma OAI.UniversalTensorSquare.sg861 line 1210
  207. lemma OAI.UniversalTensorSquare.sg862 line 1221
  208. lemma OAI.UniversalTensorSquare.sg863 line 1232
  209. lemma OAI.UniversalTensorSquare.sg864 line 1243
  210. lemma OAI.UniversalTensorSquare.sg865 line 1254
  211. lemma OAI.UniversalTensorSquare.sg866 line 1265
  212. lemma OAI.UniversalTensorSquare.sg867 line 1276
  213. lemma OAI.UniversalTensorSquare.sg868 line 1287
  214. lemma OAI.UniversalTensorSquare.sg869 line 1298
  215. lemma OAI.UniversalTensorSquare.sg870 line 1309
  216. lemma OAI.UniversalTensorSquare.sg871 line 1320
  217. lemma OAI.UniversalTensorSquare.sg910 line 1331
  218. lemma OAI.UniversalTensorSquare.sg996 line 1335
  219. lemma OAI.UniversalTensorSquare.sg1075 line 1339
  220. lemma OAI.UniversalTensorSquare.sg1076 line 1343
  221. lemma OAI.UniversalTensorSquare.sg1077 line 1347
  222. lemma OAI.UniversalTensorSquare.sg1078 line 1351
  223. lemma OAI.UniversalTensorSquare.sg1079 line 1355
  224. lemma OAI.UniversalTensorSquare.sg1080 line 1359
  225. lemma OAI.UniversalTensorSquare.sg1081 line 1363
  226. lemma OAI.UniversalTensorSquare.sg1082 line 1367
  227. lemma OAI.UniversalTensorSquare.sg1083 line 1371
  228. lemma OAI.UniversalTensorSquare.sg1084 line 1375
  229. lemma OAI.UniversalTensorSquare.sg1085 line 1379
  230. lemma OAI.UniversalTensorSquare.sg1086 line 1383
  231. lemma OAI.UniversalTensorSquare.sg1087 line 1387
  232. lemma OAI.UniversalTensorSquare.sg1088 line 1391
  233. lemma OAI.UniversalTensorSquare.sg1089 line 1395
  234. lemma OAI.UniversalTensorSquare.sg1090 line 1399
  235. lemma OAI.UniversalTensorSquare.sg1091 line 1403
  236. lemma OAI.UniversalTensorSquare.sg1131 line 1406
  237. lemma OAI.UniversalTensorSquare.sg1132 line 1410
  238. lemma OAI.UniversalTensorSquare.sg1133 line 1414
  239. lemma OAI.UniversalTensorSquare.sg1134 line 1418
  240. lemma OAI.UniversalTensorSquare.sg1135 line 1422
  241. lemma OAI.UniversalTensorSquare.sg1177 line 1426
  242. lemma OAI.UniversalTensorSquare.sg1180 line 1429
  243. lemma OAI.UniversalTensorSquare.sg1232 line 1432
  244. lemma OAI.UniversalTensorSquare.sg1327 line 1436
  245. lemma OAI.UniversalTensorSquare.sg1478 line 1440
  246. lemma OAI.UniversalTensorSquare.sg1479 line 1444
  247. lemma OAI.UniversalTensorSquare.sg1480 line 1448
  248. lemma OAI.UniversalTensorSquare.sg1481 line 1452
  249. lemma OAI.UniversalTensorSquare.sg1482 line 1456
  250. lemma OAI.UniversalTensorSquare.sg1483 line 1460
  251. lemma OAI.UniversalTensorSquare.sg1484 line 1464
  252. lemma OAI.UniversalTensorSquare.sg1485 line 1468
  253. lemma OAI.UniversalTensorSquare.sg1486 line 1472
  254. lemma OAI.UniversalTensorSquare.sg1487 line 1476
  255. lemma OAI.UniversalTensorSquare.sg1488 line 1480
  256. lemma OAI.UniversalTensorSquare.sg1489 line 1484
  257. lemma OAI.UniversalTensorSquare.sg1490 line 1488
  258. lemma OAI.UniversalTensorSquare.sg1491 line 1492
  259. lemma OAI.UniversalTensorSquare.sg1492 line 1496
  260. lemma OAI.UniversalTensorSquare.sg1493 line 1500
  261. lemma OAI.UniversalTensorSquare.sg1494 line 1504
  262. lemma OAI.UniversalTensorSquare.sg1495 line 1508
  263. lemma OAI.UniversalTensorSquare.sg1496 line 1512
  264. lemma OAI.UniversalTensorSquare.sg1497 line 1516
  265. lemma OAI.UniversalTensorSquare.sg1615 line 1520
  266. lemma OAI.UniversalTensorSquare.sg1650 line 1523
  267. lemma OAI.UniversalTensorSquare.sg1682 line 1527
  268. lemma OAI.UniversalTensorSquare.sg1734 line 1531
  269. lemma OAI.UniversalTensorSquare.sg1754 line 1534
  270. lemma OAI.UniversalTensorSquare.sg1871 line 1538
  271. lemma OAI.UniversalTensorSquare.sg1928 line 1542
  272. lemma OAI.UniversalTensorSquare.sg1930 line 1546
  273. lemma OAI.UniversalTensorSquare.sg1931 line 1550
  274. lemma OAI.UniversalTensorSquare.sg1932 line 1554
  275. lemma OAI.UniversalTensorSquare.sg1933 line 1558
  276. lemma OAI.UniversalTensorSquare.sg1934 line 1562
  277. lemma OAI.UniversalTensorSquare.sg1936 line 1566
  278. lemma OAI.UniversalTensorSquare.sg1937 line 1570
  279. lemma OAI.UniversalTensorSquare.sg1938 line 1574
  280. lemma OAI.UniversalTensorSquare.sg1939 line 1578
  281. lemma OAI.UniversalTensorSquare.sg1940 line 1582
  282. lemma OAI.UniversalTensorSquare.sg1941 line 1586
  283. lemma OAI.UniversalTensorSquare.sg1942 line 1590
  284. lemma OAI.UniversalTensorSquare.sg2015 line 1594
  285. lemma OAI.UniversalTensorSquare.sg2016 line 1598
  286. lemma OAI.UniversalTensorSquare.sg2017 line 1602
  287. lemma OAI.UniversalTensorSquare.sg2018 line 1606
  288. lemma OAI.UniversalTensorSquare.sg2019 line 1610
  289. lemma OAI.UniversalTensorSquare.sg2072 line 1614
  290. lemma OAI.UniversalTensorSquare.sg2105 line 1617
  291. lemma OAI.UniversalTensorSquare.sg2107 line 1620
  292. lemma OAI.UniversalTensorSquare.sg2137 line 1624
  293. lemma OAI.UniversalTensorSquare.sg2251 line 1628
  294. lemma OAI.UniversalTensorSquare.sg2364 line 1632
  295. lemma OAI.UniversalTensorSquare.sg2488 line 1636
  296. lemma OAI.UniversalTensorSquare.sg2489 line 1640
  297. lemma OAI.UniversalTensorSquare.sg2573 line 1644
  298. lemma OAI.UniversalTensorSquare.sg2596 line 1647
  299. lemma OAI.UniversalTensorSquare.sg2626 line 1651
  300. lemma OAI.UniversalTensorSquare.sg2702 line 1655
  301. lemma OAI.UniversalTensorSquare.sg3106 line 1659
  302. lemma OAI.UniversalTensorSquare.sg3239 line 1663
  303. lemma OAI.UniversalTensorSquare.sg3299 line 1666
  304. lemma OAI.UniversalTensorSquare.sg3300 line 1677
  305. lemma OAI.UniversalTensorSquare.sg3301 line 1688
  306. lemma OAI.UniversalTensorSquare.sg3302 line 1699
  307. lemma OAI.UniversalTensorSquare.sg3303 line 1710
  308. lemma OAI.UniversalTensorSquare.sg3304 line 1721
  309. lemma OAI.UniversalTensorSquare.sg3305 line 1732
  310. lemma OAI.UniversalTensorSquare.sg3306 line 1743
  311. lemma OAI.UniversalTensorSquare.sg3521 line 1754
  312. lemma OAI.UniversalTensorSquare.sg3739 line 1758
  313. lemma OAI.UniversalTensorSquare.sg3740 line 1762
  314. lemma OAI.UniversalTensorSquare.sg3742 line 1766
  315. lemma OAI.UniversalTensorSquare.sg3743 line 1770
  316. lemma OAI.UniversalTensorSquare.sg3998 line 1774
  317. lemma OAI.UniversalTensorSquare.sg4063 line 1778
  318. lemma OAI.UniversalTensorSquare.sg4160 line 1782
  319. lemma OAI.UniversalTensorSquare.sg4345 line 1786
  320. lemma OAI.UniversalTensorSquare.sg4804 line 1790
  321. lemma OAI.UniversalTensorSquare.sg4832 line 1794
  322. lemma OAI.UniversalTensorSquare.sg4862 line 1798
  323. lemma OAI.UniversalTensorSquare.sg4930 line 1802
  324. lemma OAI.UniversalTensorSquare.sg5011 line 1806
  325. lemma OAI.UniversalTensorSquare.sg5012 line 1810
  326. lemma OAI.UniversalTensorSquare.sg5013 line 1814
  327. lemma OAI.UniversalTensorSquare.sg5014 line 1818
  328. lemma OAI.UniversalTensorSquare.sg5015 line 1822
  329. lemma OAI.UniversalTensorSquare.sg5016 line 1826
  330. lemma OAI.UniversalTensorSquare.sg5017 line 1830
  331. lemma OAI.UniversalTensorSquare.sg5672 line 1834
  332. lemma OAI.UniversalTensorSquare.sg5735 line 1838
  333. lemma OAI.UniversalTensorSquare.sg5757 line 1842
  334. lemma OAI.UniversalTensorSquare.sg6339 line 1846
  335. lemma OAI.UniversalTensorSquare.sg6389 line 1850
  336. lemma OAI.UniversalTensorSquare.sg6457 line 1854
  337. lemma OAI.UniversalTensorSquare.sg6502 line 1858
  338. lemma OAI.UniversalTensorSquare.sg7812 line 1862
  339. lemma OAI.UniversalTensorSquare.sg7998 line 1866
  340. lemma OAI.UniversalTensorSquare.sg8008 line 1870
  341. lemma OAI.UniversalTensorSquare.sg8780 line 1874
  342. lemma OAI.UniversalTensorSquare.sg10867 line 1878
  343. lemma OAI.UniversalTensorSquare.sg11531 line 1882