OAI/Combinatorics/Ramsey/CycleClique/Certificates027.lean

GitHub source file

245 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_832_q line 20
  2. def OAI.CycleClique.certificate_832_edges line 21
  3. def OAI.CycleClique.certificate_832_part_0 line 23
  4. def OAI.CycleClique.certificate_832_part_1 line 25
  5. def OAI.CycleClique.certificate_832_part_2 line 27
  6. def OAI.CycleClique.certificate_832 line 29
  7. theorem OAI.CycleClique.certificate_832_checked line 31
  8. theorem OAI.CycleClique.certificate_832_valid line 32
  9. def OAI.CycleClique.certificate_833_q line 34
  10. def OAI.CycleClique.certificate_833_edges line 35
  11. def OAI.CycleClique.certificate_833_part_0 line 37
  12. def OAI.CycleClique.certificate_833_part_1 line 39
  13. def OAI.CycleClique.certificate_833_part_2 line 41
  14. def OAI.CycleClique.certificate_833 line 43
  15. theorem OAI.CycleClique.certificate_833_checked line 45
  16. theorem OAI.CycleClique.certificate_833_valid line 46
  17. def OAI.CycleClique.certificate_834_q line 48
  18. def OAI.CycleClique.certificate_834_edges line 49
  19. def OAI.CycleClique.certificate_834_part_0 line 51
  20. def OAI.CycleClique.certificate_834_part_1 line 53
  21. def OAI.CycleClique.certificate_834_part_2 line 55
  22. def OAI.CycleClique.certificate_834 line 57
  23. theorem OAI.CycleClique.certificate_834_checked line 59
  24. theorem OAI.CycleClique.certificate_834_valid line 60
  25. def OAI.CycleClique.certificate_835_q line 62
  26. def OAI.CycleClique.certificate_835_edges line 63
  27. def OAI.CycleClique.certificate_835_part_0 line 65
  28. def OAI.CycleClique.certificate_835_part_1 line 67
  29. def OAI.CycleClique.certificate_835_part_2 line 69
  30. def OAI.CycleClique.certificate_835 line 71
  31. theorem OAI.CycleClique.certificate_835_checked line 73
  32. theorem OAI.CycleClique.certificate_835_valid line 74
  33. def OAI.CycleClique.certificate_836_q line 76
  34. def OAI.CycleClique.certificate_836_edges line 77
  35. def OAI.CycleClique.certificate_836_part_0 line 79
  36. def OAI.CycleClique.certificate_836 line 81
  37. theorem OAI.CycleClique.certificate_836_checked line 83
  38. theorem OAI.CycleClique.certificate_836_valid line 84
  39. def OAI.CycleClique.certificate_837_q line 86
  40. def OAI.CycleClique.certificate_837_edges line 87
  41. def OAI.CycleClique.certificate_837_part_0 line 89
  42. def OAI.CycleClique.certificate_837 line 91
  43. theorem OAI.CycleClique.certificate_837_checked line 93
  44. theorem OAI.CycleClique.certificate_837_valid line 94
  45. def OAI.CycleClique.certificate_838_q line 96
  46. def OAI.CycleClique.certificate_838_edges line 97
  47. def OAI.CycleClique.certificate_838_part_0 line 99
  48. def OAI.CycleClique.certificate_838_part_1 line 101
  49. def OAI.CycleClique.certificate_838 line 103
  50. theorem OAI.CycleClique.certificate_838_checked line 105
  51. theorem OAI.CycleClique.certificate_838_valid line 106
  52. def OAI.CycleClique.certificate_839_q line 108
  53. def OAI.CycleClique.certificate_839_edges line 109
  54. def OAI.CycleClique.certificate_839_part_0 line 111
  55. def OAI.CycleClique.certificate_839_part_1 line 113
  56. def OAI.CycleClique.certificate_839 line 115
  57. theorem OAI.CycleClique.certificate_839_checked line 117
  58. theorem OAI.CycleClique.certificate_839_valid line 118
  59. def OAI.CycleClique.certificate_840_q line 120
  60. def OAI.CycleClique.certificate_840_edges line 121
  61. def OAI.CycleClique.certificate_840_part_0 line 123
  62. def OAI.CycleClique.certificate_840_part_1 line 125
  63. def OAI.CycleClique.certificate_840 line 127
  64. theorem OAI.CycleClique.certificate_840_checked line 129
  65. theorem OAI.CycleClique.certificate_840_valid line 130
  66. def OAI.CycleClique.certificate_841_q line 132
  67. def OAI.CycleClique.certificate_841_edges line 133
  68. def OAI.CycleClique.certificate_841_part_0 line 135
  69. def OAI.CycleClique.certificate_841_part_1 line 137
  70. def OAI.CycleClique.certificate_841_part_2 line 139
  71. def OAI.CycleClique.certificate_841 line 141
  72. theorem OAI.CycleClique.certificate_841_checked line 143
  73. theorem OAI.CycleClique.certificate_841_valid line 144
  74. def OAI.CycleClique.certificate_842_q line 146
  75. def OAI.CycleClique.certificate_842_edges line 147
  76. def OAI.CycleClique.certificate_842_part_0 line 149
  77. def OAI.CycleClique.certificate_842_part_1 line 151
  78. def OAI.CycleClique.certificate_842_part_2 line 153
  79. def OAI.CycleClique.certificate_842_part_3 line 155
  80. def OAI.CycleClique.certificate_842 line 157
  81. theorem OAI.CycleClique.certificate_842_checked line 159
  82. theorem OAI.CycleClique.certificate_842_valid line 160
  83. def OAI.CycleClique.certificate_843_q line 162
  84. def OAI.CycleClique.certificate_843_edges line 163
  85. def OAI.CycleClique.certificate_843_part_0 line 165
  86. def OAI.CycleClique.certificate_843_part_1 line 167
  87. def OAI.CycleClique.certificate_843_part_2 line 169
  88. def OAI.CycleClique.certificate_843_part_3 line 171
  89. def OAI.CycleClique.certificate_843_part_4 line 173
  90. def OAI.CycleClique.certificate_843 line 175
  91. theorem OAI.CycleClique.certificate_843_checked line 177
  92. theorem OAI.CycleClique.certificate_843_valid line 178
  93. def OAI.CycleClique.certificate_844_q line 180
  94. def OAI.CycleClique.certificate_844_edges line 181
  95. def OAI.CycleClique.certificate_844_part_0 line 183
  96. def OAI.CycleClique.certificate_844_part_1 line 185
  97. def OAI.CycleClique.certificate_844 line 187
  98. theorem OAI.CycleClique.certificate_844_checked line 189
  99. theorem OAI.CycleClique.certificate_844_valid line 190
  100. def OAI.CycleClique.certificate_845_q line 192
  101. def OAI.CycleClique.certificate_845_edges line 193
  102. def OAI.CycleClique.certificate_845_part_0 line 195
  103. def OAI.CycleClique.certificate_845_part_1 line 197
  104. def OAI.CycleClique.certificate_845 line 199
  105. theorem OAI.CycleClique.certificate_845_checked line 201
  106. theorem OAI.CycleClique.certificate_845_valid line 202
  107. def OAI.CycleClique.certificate_846_q line 204
  108. def OAI.CycleClique.certificate_846_edges line 205
  109. def OAI.CycleClique.certificate_846_part_0 line 207
  110. def OAI.CycleClique.certificate_846_part_1 line 209
  111. def OAI.CycleClique.certificate_846 line 211
  112. theorem OAI.CycleClique.certificate_846_checked line 213
  113. theorem OAI.CycleClique.certificate_846_valid line 214
  114. def OAI.CycleClique.certificate_847_q line 216
  115. def OAI.CycleClique.certificate_847_edges line 217
  116. def OAI.CycleClique.certificate_847_part_0 line 219
  117. def OAI.CycleClique.certificate_847_part_1 line 221
  118. def OAI.CycleClique.certificate_847_part_2 line 223
  119. def OAI.CycleClique.certificate_847 line 225
  120. theorem OAI.CycleClique.certificate_847_checked line 227
  121. theorem OAI.CycleClique.certificate_847_valid line 228
  122. def OAI.CycleClique.certificate_848_q line 230
  123. def OAI.CycleClique.certificate_848_edges line 231
  124. def OAI.CycleClique.certificate_848_part_0 line 233
  125. def OAI.CycleClique.certificate_848_part_1 line 235
  126. def OAI.CycleClique.certificate_848_part_2 line 237
  127. def OAI.CycleClique.certificate_848 line 239
  128. theorem OAI.CycleClique.certificate_848_checked line 241
  129. theorem OAI.CycleClique.certificate_848_valid line 242
  130. def OAI.CycleClique.certificate_849_q line 244
  131. def OAI.CycleClique.certificate_849_edges line 245
  132. def OAI.CycleClique.certificate_849_part_0 line 247
  133. def OAI.CycleClique.certificate_849_part_1 line 249
  134. def OAI.CycleClique.certificate_849_part_2 line 251
  135. def OAI.CycleClique.certificate_849_part_3 line 253
  136. def OAI.CycleClique.certificate_849 line 255
  137. theorem OAI.CycleClique.certificate_849_checked line 257
  138. theorem OAI.CycleClique.certificate_849_valid line 258
  139. def OAI.CycleClique.certificate_850_q line 260
  140. def OAI.CycleClique.certificate_850_edges line 261
  141. def OAI.CycleClique.certificate_850_part_0 line 263
  142. def OAI.CycleClique.certificate_850_part_1 line 265
  143. def OAI.CycleClique.certificate_850 line 267
  144. theorem OAI.CycleClique.certificate_850_checked line 269
  145. theorem OAI.CycleClique.certificate_850_valid line 270
  146. def OAI.CycleClique.certificate_851_q line 272
  147. def OAI.CycleClique.certificate_851_edges line 273
  148. def OAI.CycleClique.certificate_851_part_0 line 275
  149. def OAI.CycleClique.certificate_851_part_1 line 277
  150. def OAI.CycleClique.certificate_851_part_2 line 279
  151. def OAI.CycleClique.certificate_851 line 281
  152. theorem OAI.CycleClique.certificate_851_checked line 283
  153. theorem OAI.CycleClique.certificate_851_valid line 284
  154. def OAI.CycleClique.certificate_852_q line 286
  155. def OAI.CycleClique.certificate_852_edges line 287
  156. def OAI.CycleClique.certificate_852_part_0 line 289
  157. def OAI.CycleClique.certificate_852_part_1 line 291
  158. def OAI.CycleClique.certificate_852_part_2 line 293
  159. def OAI.CycleClique.certificate_852 line 295
  160. theorem OAI.CycleClique.certificate_852_checked line 297
  161. theorem OAI.CycleClique.certificate_852_valid line 298
  162. def OAI.CycleClique.certificate_853_q line 300
  163. def OAI.CycleClique.certificate_853_edges line 301
  164. def OAI.CycleClique.certificate_853_part_0 line 303
  165. def OAI.CycleClique.certificate_853_part_1 line 305
  166. def OAI.CycleClique.certificate_853_part_2 line 307
  167. def OAI.CycleClique.certificate_853 line 309
  168. theorem OAI.CycleClique.certificate_853_checked line 311
  169. theorem OAI.CycleClique.certificate_853_valid line 312
  170. def OAI.CycleClique.certificate_854_q line 314
  171. def OAI.CycleClique.certificate_854_edges line 315
  172. def OAI.CycleClique.certificate_854_part_0 line 317
  173. def OAI.CycleClique.certificate_854_part_1 line 319
  174. def OAI.CycleClique.certificate_854_part_2 line 321
  175. def OAI.CycleClique.certificate_854 line 323
  176. theorem OAI.CycleClique.certificate_854_checked line 325
  177. theorem OAI.CycleClique.certificate_854_valid line 326
  178. def OAI.CycleClique.certificate_855_q line 328
  179. def OAI.CycleClique.certificate_855_edges line 329
  180. def OAI.CycleClique.certificate_855_part_0 line 331
  181. def OAI.CycleClique.certificate_855_part_1 line 333
  182. def OAI.CycleClique.certificate_855_part_2 line 335
  183. def OAI.CycleClique.certificate_855 line 337
  184. theorem OAI.CycleClique.certificate_855_checked line 339
  185. theorem OAI.CycleClique.certificate_855_valid line 340
  186. def OAI.CycleClique.certificate_856_q line 342
  187. def OAI.CycleClique.certificate_856_edges line 343
  188. def OAI.CycleClique.certificate_856_part_0 line 345
  189. def OAI.CycleClique.certificate_856_part_1 line 347
  190. def OAI.CycleClique.certificate_856 line 349
  191. theorem OAI.CycleClique.certificate_856_checked line 351
  192. theorem OAI.CycleClique.certificate_856_valid line 352
  193. def OAI.CycleClique.certificate_857_q line 354
  194. def OAI.CycleClique.certificate_857_edges line 355
  195. def OAI.CycleClique.certificate_857_part_0 line 357
  196. def OAI.CycleClique.certificate_857_part_1 line 359
  197. def OAI.CycleClique.certificate_857 line 361
  198. theorem OAI.CycleClique.certificate_857_checked line 363
  199. theorem OAI.CycleClique.certificate_857_valid line 364
  200. def OAI.CycleClique.certificate_858_q line 366
  201. def OAI.CycleClique.certificate_858_edges line 367
  202. def OAI.CycleClique.certificate_858_part_0 line 369
  203. def OAI.CycleClique.certificate_858_part_1 line 371
  204. def OAI.CycleClique.certificate_858 line 373
  205. theorem OAI.CycleClique.certificate_858_checked line 375
  206. theorem OAI.CycleClique.certificate_858_valid line 376
  207. def OAI.CycleClique.certificate_859_q line 378
  208. def OAI.CycleClique.certificate_859_edges line 379
  209. def OAI.CycleClique.certificate_859_part_0 line 381
  210. def OAI.CycleClique.certificate_859_part_1 line 383
  211. def OAI.CycleClique.certificate_859_part_2 line 385
  212. def OAI.CycleClique.certificate_859 line 387
  213. theorem OAI.CycleClique.certificate_859_checked line 389
  214. theorem OAI.CycleClique.certificate_859_valid line 390
  215. def OAI.CycleClique.certificate_860_q line 392
  216. def OAI.CycleClique.certificate_860_edges line 393
  217. def OAI.CycleClique.certificate_860_part_0 line 395
  218. def OAI.CycleClique.certificate_860_part_1 line 397
  219. def OAI.CycleClique.certificate_860_part_2 line 399
  220. def OAI.CycleClique.certificate_860 line 401
  221. theorem OAI.CycleClique.certificate_860_checked line 403
  222. theorem OAI.CycleClique.certificate_860_valid line 404
  223. def OAI.CycleClique.certificate_861_q line 406
  224. def OAI.CycleClique.certificate_861_edges line 407
  225. def OAI.CycleClique.certificate_861_part_0 line 409
  226. def OAI.CycleClique.certificate_861_part_1 line 411
  227. def OAI.CycleClique.certificate_861_part_2 line 413
  228. def OAI.CycleClique.certificate_861_part_3 line 415
  229. def OAI.CycleClique.certificate_861 line 417
  230. theorem OAI.CycleClique.certificate_861_checked line 419
  231. theorem OAI.CycleClique.certificate_861_valid line 420
  232. def OAI.CycleClique.certificate_862_q line 422
  233. def OAI.CycleClique.certificate_862_edges line 423
  234. def OAI.CycleClique.certificate_862_part_0 line 425
  235. def OAI.CycleClique.certificate_862_part_1 line 427
  236. def OAI.CycleClique.certificate_862 line 429
  237. theorem OAI.CycleClique.certificate_862_checked line 431
  238. theorem OAI.CycleClique.certificate_862_valid line 432
  239. def OAI.CycleClique.certificate_863_q line 434
  240. def OAI.CycleClique.certificate_863_edges line 435
  241. def OAI.CycleClique.certificate_863_part_0 line 437
  242. def OAI.CycleClique.certificate_863_part_1 line 439
  243. def OAI.CycleClique.certificate_863 line 441
  244. theorem OAI.CycleClique.certificate_863_checked line 443
  245. theorem OAI.CycleClique.certificate_863_valid line 444