OAI/Combinatorics/Ramsey/CycleClique/Certificates006.lean

GitHub source file

315 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_160_q line 20
  2. def OAI.CycleClique.certificate_160_edges line 21
  3. def OAI.CycleClique.certificate_160_part_0 line 23
  4. def OAI.CycleClique.certificate_160 line 25
  5. theorem OAI.CycleClique.certificate_160_checked line 27
  6. theorem OAI.CycleClique.certificate_160_valid line 28
  7. def OAI.CycleClique.certificate_161_q line 30
  8. def OAI.CycleClique.certificate_161_edges line 31
  9. def OAI.CycleClique.certificate_161_part_0 line 33
  10. def OAI.CycleClique.certificate_161 line 35
  11. theorem OAI.CycleClique.certificate_161_checked line 37
  12. theorem OAI.CycleClique.certificate_161_valid line 38
  13. def OAI.CycleClique.certificate_162_q line 40
  14. def OAI.CycleClique.certificate_162_edges line 41
  15. def OAI.CycleClique.certificate_162_part_0 line 43
  16. def OAI.CycleClique.certificate_162_part_1 line 45
  17. def OAI.CycleClique.certificate_162 line 47
  18. theorem OAI.CycleClique.certificate_162_checked line 49
  19. theorem OAI.CycleClique.certificate_162_valid line 50
  20. def OAI.CycleClique.certificate_163_q line 52
  21. def OAI.CycleClique.certificate_163_edges line 53
  22. def OAI.CycleClique.certificate_163_part_0 line 55
  23. def OAI.CycleClique.certificate_163 line 57
  24. theorem OAI.CycleClique.certificate_163_checked line 59
  25. theorem OAI.CycleClique.certificate_163_valid line 60
  26. def OAI.CycleClique.certificate_164_q line 62
  27. def OAI.CycleClique.certificate_164_edges line 63
  28. def OAI.CycleClique.certificate_164_part_0 line 65
  29. def OAI.CycleClique.certificate_164_part_1 line 67
  30. def OAI.CycleClique.certificate_164 line 69
  31. theorem OAI.CycleClique.certificate_164_checked line 71
  32. theorem OAI.CycleClique.certificate_164_valid line 72
  33. def OAI.CycleClique.certificate_165_q line 74
  34. def OAI.CycleClique.certificate_165_edges line 75
  35. def OAI.CycleClique.certificate_165_part_0 line 77
  36. def OAI.CycleClique.certificate_165_part_1 line 79
  37. def OAI.CycleClique.certificate_165 line 81
  38. theorem OAI.CycleClique.certificate_165_checked line 83
  39. theorem OAI.CycleClique.certificate_165_valid line 84
  40. def OAI.CycleClique.certificate_166_q line 86
  41. def OAI.CycleClique.certificate_166_edges line 87
  42. def OAI.CycleClique.certificate_166_part_0 line 89
  43. def OAI.CycleClique.certificate_166 line 91
  44. theorem OAI.CycleClique.certificate_166_checked line 93
  45. theorem OAI.CycleClique.certificate_166_valid line 94
  46. def OAI.CycleClique.certificate_167_q line 96
  47. def OAI.CycleClique.certificate_167_edges line 97
  48. def OAI.CycleClique.certificate_167_part_0 line 99
  49. def OAI.CycleClique.certificate_167_part_1 line 101
  50. def OAI.CycleClique.certificate_167 line 103
  51. theorem OAI.CycleClique.certificate_167_checked line 105
  52. theorem OAI.CycleClique.certificate_167_valid line 106
  53. def OAI.CycleClique.certificate_168_q line 108
  54. def OAI.CycleClique.certificate_168_edges line 109
  55. def OAI.CycleClique.certificate_168_part_0 line 111
  56. def OAI.CycleClique.certificate_168_part_1 line 113
  57. def OAI.CycleClique.certificate_168 line 115
  58. theorem OAI.CycleClique.certificate_168_checked line 117
  59. theorem OAI.CycleClique.certificate_168_valid line 118
  60. def OAI.CycleClique.certificate_169_q line 120
  61. def OAI.CycleClique.certificate_169_edges line 121
  62. def OAI.CycleClique.certificate_169_part_0 line 123
  63. def OAI.CycleClique.certificate_169 line 125
  64. theorem OAI.CycleClique.certificate_169_checked line 127
  65. theorem OAI.CycleClique.certificate_169_valid line 128
  66. def OAI.CycleClique.certificate_170_q line 130
  67. def OAI.CycleClique.certificate_170_edges line 131
  68. def OAI.CycleClique.certificate_170_part_0 line 133
  69. def OAI.CycleClique.certificate_170 line 135
  70. theorem OAI.CycleClique.certificate_170_checked line 137
  71. theorem OAI.CycleClique.certificate_170_valid line 138
  72. def OAI.CycleClique.certificate_171_q line 140
  73. def OAI.CycleClique.certificate_171_edges line 141
  74. def OAI.CycleClique.certificate_171_part_0 line 143
  75. def OAI.CycleClique.certificate_171_part_1 line 145
  76. def OAI.CycleClique.certificate_171 line 147
  77. theorem OAI.CycleClique.certificate_171_checked line 149
  78. theorem OAI.CycleClique.certificate_171_valid line 150
  79. def OAI.CycleClique.certificate_172_q line 152
  80. def OAI.CycleClique.certificate_172_edges line 153
  81. def OAI.CycleClique.certificate_172_part_0 line 155
  82. def OAI.CycleClique.certificate_172_part_1 line 157
  83. def OAI.CycleClique.certificate_172 line 159
  84. theorem OAI.CycleClique.certificate_172_checked line 161
  85. theorem OAI.CycleClique.certificate_172_valid line 162
  86. def OAI.CycleClique.certificate_173_q line 164
  87. def OAI.CycleClique.certificate_173_edges line 165
  88. def OAI.CycleClique.certificate_173_part_0 line 167
  89. def OAI.CycleClique.certificate_173 line 169
  90. theorem OAI.CycleClique.certificate_173_checked line 171
  91. theorem OAI.CycleClique.certificate_173_valid line 172
  92. def OAI.CycleClique.certificate_174_q line 174
  93. def OAI.CycleClique.certificate_174_edges line 175
  94. def OAI.CycleClique.certificate_174_part_0 line 177
  95. def OAI.CycleClique.certificate_174_part_1 line 179
  96. def OAI.CycleClique.certificate_174 line 181
  97. theorem OAI.CycleClique.certificate_174_checked line 183
  98. theorem OAI.CycleClique.certificate_174_valid line 184
  99. def OAI.CycleClique.certificate_175_q line 186
  100. def OAI.CycleClique.certificate_175_edges line 187
  101. def OAI.CycleClique.certificate_175_part_0 line 189
  102. def OAI.CycleClique.certificate_175 line 191
  103. theorem OAI.CycleClique.certificate_175_checked line 193
  104. theorem OAI.CycleClique.certificate_175_valid line 194
  105. def OAI.CycleClique.certificate_176_q line 196
  106. def OAI.CycleClique.certificate_176_edges line 197
  107. def OAI.CycleClique.certificate_176_part_0 line 199
  108. def OAI.CycleClique.certificate_176_part_1 line 201
  109. def OAI.CycleClique.certificate_176 line 203
  110. theorem OAI.CycleClique.certificate_176_checked line 205
  111. theorem OAI.CycleClique.certificate_176_valid line 206
  112. def OAI.CycleClique.certificate_177_q line 208
  113. def OAI.CycleClique.certificate_177_edges line 209
  114. def OAI.CycleClique.certificate_177_part_0 line 211
  115. def OAI.CycleClique.certificate_177_part_1 line 213
  116. def OAI.CycleClique.certificate_177 line 215
  117. theorem OAI.CycleClique.certificate_177_checked line 217
  118. theorem OAI.CycleClique.certificate_177_valid line 218
  119. def OAI.CycleClique.certificate_178_q line 220
  120. def OAI.CycleClique.certificate_178_edges line 221
  121. def OAI.CycleClique.certificate_178_part_0 line 223
  122. def OAI.CycleClique.certificate_178_part_1 line 225
  123. def OAI.CycleClique.certificate_178 line 227
  124. theorem OAI.CycleClique.certificate_178_checked line 229
  125. theorem OAI.CycleClique.certificate_178_valid line 230
  126. def OAI.CycleClique.certificate_179_q line 232
  127. def OAI.CycleClique.certificate_179_edges line 233
  128. def OAI.CycleClique.certificate_179_part_0 line 235
  129. def OAI.CycleClique.certificate_179 line 237
  130. theorem OAI.CycleClique.certificate_179_checked line 239
  131. theorem OAI.CycleClique.certificate_179_valid line 240
  132. def OAI.CycleClique.certificate_180_q line 242
  133. def OAI.CycleClique.certificate_180_edges line 243
  134. def OAI.CycleClique.certificate_180_part_0 line 245
  135. def OAI.CycleClique.certificate_180 line 247
  136. theorem OAI.CycleClique.certificate_180_checked line 249
  137. theorem OAI.CycleClique.certificate_180_valid line 250
  138. def OAI.CycleClique.certificate_181_q line 252
  139. def OAI.CycleClique.certificate_181_edges line 253
  140. def OAI.CycleClique.certificate_181_part_0 line 255
  141. def OAI.CycleClique.certificate_181 line 257
  142. theorem OAI.CycleClique.certificate_181_checked line 259
  143. theorem OAI.CycleClique.certificate_181_valid line 260
  144. def OAI.CycleClique.certificate_182_q line 262
  145. def OAI.CycleClique.certificate_182_edges line 263
  146. def OAI.CycleClique.certificate_182_part_0 line 265
  147. def OAI.CycleClique.certificate_182_part_1 line 267
  148. def OAI.CycleClique.certificate_182 line 269
  149. theorem OAI.CycleClique.certificate_182_checked line 271
  150. theorem OAI.CycleClique.certificate_182_valid line 272
  151. def OAI.CycleClique.certificate_183_q line 274
  152. def OAI.CycleClique.certificate_183_edges line 276
  153. def OAI.CycleClique.certificate_183_E line 278
  154. def OAI.CycleClique.certificate_183_M line 280
  155. def OAI.CycleClique.certificate_183_part_1_E line 282
  156. def OAI.CycleClique.certificate_183_part_1_M line 284
  157. def OAI.CycleClique.certificate_183_part_2_E line 286
  158. def OAI.CycleClique.certificate_183_part_2_M line 288
  159. def OAI.CycleClique.certificate_183_part_3_E line 290
  160. def OAI.CycleClique.certificate_183_part_3_M line 292
  161. def OAI.CycleClique.certificate_183_part_4_E line 294
  162. def OAI.CycleClique.certificate_183_part_4_M line 296
  163. def OAI.CycleClique.certificate_183_part_5_E line 298
  164. def OAI.CycleClique.certificate_183_part_5_M line 300
  165. def OAI.CycleClique.certificate_183_part_6_E line 302
  166. def OAI.CycleClique.certificate_183_part_6_M line 304
  167. def OAI.CycleClique.certificate_183_part_6 line 306
  168. theorem OAI.CycleClique.certificate_183_part_6_checked line 308
  169. def OAI.CycleClique.certificate_183_part_7_E line 310
  170. def OAI.CycleClique.certificate_183_part_7_M line 312
  171. def OAI.CycleClique.certificate_183_part_8_E line 314
  172. def OAI.CycleClique.certificate_183_part_8_M line 316
  173. def OAI.CycleClique.certificate_183_part_8 line 318
  174. theorem OAI.CycleClique.certificate_183_part_8_checked line 320
  175. def OAI.CycleClique.certificate_183_part_9_E line 322
  176. def OAI.CycleClique.certificate_183_part_9_M line 324
  177. def OAI.CycleClique.certificate_183_part_10_E line 326
  178. def OAI.CycleClique.certificate_183_part_10_M line 328
  179. def OAI.CycleClique.certificate_183_part_10 line 330
  180. theorem OAI.CycleClique.certificate_183_part_10_checked line 332
  181. def OAI.CycleClique.certificate_183_part_9 line 334
  182. theorem OAI.CycleClique.certificate_183_part_9_checked line 336
  183. def OAI.CycleClique.certificate_183_part_11_E line 338
  184. def OAI.CycleClique.certificate_183_part_11_M line 340
  185. def OAI.CycleClique.certificate_183_part_12_E line 342
  186. def OAI.CycleClique.certificate_183_part_12_M line 344
  187. def OAI.CycleClique.certificate_183_part_12 line 346
  188. theorem OAI.CycleClique.certificate_183_part_12_checked line 348
  189. def OAI.CycleClique.certificate_183_part_13_E line 350
  190. def OAI.CycleClique.certificate_183_part_13_M line 352
  191. def OAI.CycleClique.certificate_183_part_13 line 354
  192. theorem OAI.CycleClique.certificate_183_part_13_checked line 356
  193. def OAI.CycleClique.certificate_183_part_14_E line 358
  194. def OAI.CycleClique.certificate_183_part_14_M line 360
  195. def OAI.CycleClique.certificate_183_part_14 line 362
  196. theorem OAI.CycleClique.certificate_183_part_14_checked line 364
  197. def OAI.CycleClique.certificate_183_part_15_E line 366
  198. def OAI.CycleClique.certificate_183_part_15_M line 368
  199. def OAI.CycleClique.certificate_183_part_15 line 370
  200. theorem OAI.CycleClique.certificate_183_part_15_checked line 372
  201. def OAI.CycleClique.certificate_183_part_16_E line 374
  202. def OAI.CycleClique.certificate_183_part_16_M line 376
  203. def OAI.CycleClique.certificate_183_part_16 line 378
  204. theorem OAI.CycleClique.certificate_183_part_16_checked line 380
  205. def OAI.CycleClique.certificate_183_part_17_E line 382
  206. def OAI.CycleClique.certificate_183_part_17_M line 384
  207. def OAI.CycleClique.certificate_183_part_18_E line 386
  208. def OAI.CycleClique.certificate_183_part_18_M line 388
  209. def OAI.CycleClique.certificate_183_part_18 line 390
  210. theorem OAI.CycleClique.certificate_183_part_18_checked line 392
  211. def OAI.CycleClique.certificate_183_part_17 line 394
  212. theorem OAI.CycleClique.certificate_183_part_17_checked line 396
  213. def OAI.CycleClique.certificate_183_part_19_E line 398
  214. def OAI.CycleClique.certificate_183_part_19_M line 400
  215. def OAI.CycleClique.certificate_183_part_20_E line 402
  216. def OAI.CycleClique.certificate_183_part_20_M line 404
  217. def OAI.CycleClique.certificate_183_part_20 line 406
  218. theorem OAI.CycleClique.certificate_183_part_20_checked line 408
  219. def OAI.CycleClique.certificate_183_part_21_E line 410
  220. def OAI.CycleClique.certificate_183_part_21_M line 412
  221. def OAI.CycleClique.certificate_183_part_22_E line 414
  222. def OAI.CycleClique.certificate_183_part_22_M line 416
  223. def OAI.CycleClique.certificate_183_part_23_E line 418
  224. def OAI.CycleClique.certificate_183_part_23_M line 420
  225. def OAI.CycleClique.certificate_183_part_24_E line 422
  226. def OAI.CycleClique.certificate_183_part_24_M line 424
  227. def OAI.CycleClique.certificate_183_part_24 line 426
  228. theorem OAI.CycleClique.certificate_183_part_24_checked line 428
  229. def OAI.CycleClique.certificate_183_part_23 line 430
  230. theorem OAI.CycleClique.certificate_183_part_23_checked line 432
  231. def OAI.CycleClique.certificate_183_part_22 line 434
  232. theorem OAI.CycleClique.certificate_183_part_22_checked line 436
  233. def OAI.CycleClique.certificate_183_part_25_E line 438
  234. def OAI.CycleClique.certificate_183_part_25_M line 440
  235. def OAI.CycleClique.certificate_183_part_26_E line 442
  236. def OAI.CycleClique.certificate_183_part_26_M line 444
  237. def OAI.CycleClique.certificate_183_part_26 line 446
  238. theorem OAI.CycleClique.certificate_183_part_26_checked line 448
  239. def OAI.CycleClique.certificate_183_part_25 line 450
  240. theorem OAI.CycleClique.certificate_183_part_25_checked line 452
  241. def OAI.CycleClique.certificate_183_part_21 line 454
  242. theorem OAI.CycleClique.certificate_183_part_21_checked line 456
  243. def OAI.CycleClique.certificate_183_part_19 line 458
  244. theorem OAI.CycleClique.certificate_183_part_19_checked line 460
  245. def OAI.CycleClique.certificate_183_part_11 line 462
  246. theorem OAI.CycleClique.certificate_183_part_11_checked line 464
  247. def OAI.CycleClique.certificate_183_part_7 line 466
  248. theorem OAI.CycleClique.certificate_183_part_7_checked line 468
  249. def OAI.CycleClique.certificate_183_part_5 line 470
  250. theorem OAI.CycleClique.certificate_183_part_5_checked line 472
  251. def OAI.CycleClique.certificate_183_part_4 line 474
  252. theorem OAI.CycleClique.certificate_183_part_4_checked line 476
  253. def OAI.CycleClique.certificate_183_part_3 line 478
  254. theorem OAI.CycleClique.certificate_183_part_3_checked line 480
  255. def OAI.CycleClique.certificate_183_part_2 line 482
  256. theorem OAI.CycleClique.certificate_183_part_2_checked line 484
  257. def OAI.CycleClique.certificate_183_part_1 line 486
  258. theorem OAI.CycleClique.certificate_183_part_1_checked line 488
  259. def OAI.CycleClique.certificate_183 line 490
  260. theorem OAI.CycleClique.certificate_183_checked line 492
  261. theorem OAI.CycleClique.certificate_183_valid line 494
  262. def OAI.CycleClique.certificate_184_q line 496
  263. def OAI.CycleClique.certificate_184_edges line 497
  264. def OAI.CycleClique.certificate_184_part_0 line 499
  265. def OAI.CycleClique.certificate_184 line 501
  266. theorem OAI.CycleClique.certificate_184_checked line 503
  267. theorem OAI.CycleClique.certificate_184_valid line 504
  268. def OAI.CycleClique.certificate_185_q line 506
  269. def OAI.CycleClique.certificate_185_edges line 507
  270. def OAI.CycleClique.certificate_185_part_0 line 509
  271. def OAI.CycleClique.certificate_185_part_1 line 511
  272. def OAI.CycleClique.certificate_185 line 513
  273. theorem OAI.CycleClique.certificate_185_checked line 515
  274. theorem OAI.CycleClique.certificate_185_valid line 516
  275. def OAI.CycleClique.certificate_186_q line 518
  276. def OAI.CycleClique.certificate_186_edges line 519
  277. def OAI.CycleClique.certificate_186_part_0 line 521
  278. def OAI.CycleClique.certificate_186_part_1 line 523
  279. def OAI.CycleClique.certificate_186 line 525
  280. theorem OAI.CycleClique.certificate_186_checked line 527
  281. theorem OAI.CycleClique.certificate_186_valid line 528
  282. def OAI.CycleClique.certificate_187_q line 530
  283. def OAI.CycleClique.certificate_187_edges line 531
  284. def OAI.CycleClique.certificate_187_part_0 line 533
  285. def OAI.CycleClique.certificate_187_part_1 line 535
  286. def OAI.CycleClique.certificate_187 line 537
  287. theorem OAI.CycleClique.certificate_187_checked line 539
  288. theorem OAI.CycleClique.certificate_187_valid line 540
  289. def OAI.CycleClique.certificate_188_q line 542
  290. def OAI.CycleClique.certificate_188_edges line 543
  291. def OAI.CycleClique.certificate_188_part_0 line 545
  292. def OAI.CycleClique.certificate_188 line 547
  293. theorem OAI.CycleClique.certificate_188_checked line 549
  294. theorem OAI.CycleClique.certificate_188_valid line 550
  295. def OAI.CycleClique.certificate_189_q line 552
  296. def OAI.CycleClique.certificate_189_edges line 553
  297. def OAI.CycleClique.certificate_189_part_0 line 555
  298. def OAI.CycleClique.certificate_189_part_1 line 557
  299. def OAI.CycleClique.certificate_189 line 559
  300. theorem OAI.CycleClique.certificate_189_checked line 561
  301. theorem OAI.CycleClique.certificate_189_valid line 562
  302. def OAI.CycleClique.certificate_190_q line 564
  303. def OAI.CycleClique.certificate_190_edges line 565
  304. def OAI.CycleClique.certificate_190_part_0 line 567
  305. def OAI.CycleClique.certificate_190_part_1 line 569
  306. def OAI.CycleClique.certificate_190 line 571
  307. theorem OAI.CycleClique.certificate_190_checked line 573
  308. theorem OAI.CycleClique.certificate_190_valid line 574
  309. def OAI.CycleClique.certificate_191_q line 576
  310. def OAI.CycleClique.certificate_191_edges line 577
  311. def OAI.CycleClique.certificate_191_part_0 line 579
  312. def OAI.CycleClique.certificate_191_part_1 line 581
  313. def OAI.CycleClique.certificate_191 line 583
  314. theorem OAI.CycleClique.certificate_191_checked line 585
  315. theorem OAI.CycleClique.certificate_191_valid line 586