`ComparatorChallenges/SnakyCertificate.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 120 curated AI-written annotations and 1273 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 9 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. Those 9 annotations were revised on 2026-10-14 to bind all of them to exact page-one quotations from 6 pinned OpenAI manuscripts, the matching pinned formalization notes, and named historical primary sources; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. The 3 manuscript-grounded matrix-multiplication annotations were composed from pinned OpenAI manuscripts and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Six additional target-specific annotations for Catalan's constant, the irrationality exponent of pi, dyadic Erdos similarity, Unique Games, quintic Lienard systems, and Yau nodal growth were composed from pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for Seymour's second-neighborhood conjecture, Cannon's conjecture, Koebe circle-domain uniformization, and circle-domain rigidity were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for simple Lebesgue spectrum on the three-torus, Rokhlin multiple mixing, the nine-dimensional Borsuk counterexample, and Tingley's sphere-isometry problem were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the Abhyankar-Sathaye counterexample, the circulant Hadamard conjecture, the Eilenberg-Ganea counterexample, and short Egyptian fractions were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and quotations from Sathaye, Turyn with Storer, Eilenberg with Ganea, and Erdos in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the complete Crouzeix inequality, unrestricted Euclidean five-coloring, the general Mahler conjecture, and Thompson F nonamenability were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, the matching formalization notes, and linked historical sources by Crouzeix, de Grey, Mahler, Cannon, Floyd, and Parry; no human review is claimed. Four additional target-specific annotations for algorithmic strong thin trees, Barnette's Hamiltonian-cycle conjecture, the explicit Artin CAT(0) counterexample, and generalized amplitude-damping capacity were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, matching formalization notes, and linked historical sources by Anari with Goddyn, Arts with Hopman and Timmermans, Charney, and Khatri with Sharma and Wilde; no human review is claimed. Fourteen solution-level annotations for Seymour's second-neighborhood theorem were added on 2026-10-14 from the pinned 15-page manuscript, covering the exact-neighborhood model, minimal-counterexample reduction, subset deficit, transitive blowup, pruning, extremal contradiction, and proof-bearing final theorem. The subset and blowup annotations also bind exact quotations from Tyler Seacrest (2019) and Brantner, Brockman, Kay, and Snively (2009); no human review is claimed. Thirty-seven declaration-level annotations were added on 2026-10-14 for the rest of ComparatorChallenges/AlgorithmicThinTrees.lean, covering its multigraph semantics, stack-machine cost model, explicit and binary-multiplicity encodings, output certificate, and complete algorithmic proposition. They are bound to the pinned OpenAI manuscript and linked earlier thin-tree sources by Luis Goddyn, Nima Anari, and Shayan Oveis Gharan; the annotation explicitly preserves that the concluding comparator theorem still has body by sorry, and no human review is claimed. Thirty-one supporting declarations in ComparatorChallenges/UniqueGamesTheorem.lean were upgraded or added on 2026-10-14, completing curated coverage of all thirty-two declarations in that file. The annotations cover the finite game model, Boolean formula and parser, binary-vector translations, explicit output serialization, finite-alphabet machine contract, and gap theorem; they distinguish manuscript-backed mathematics from Lean-specific canonical parsing and unary game output encoding, bind exact OpenAI manuscript quotations, and credit Subhash Khot through his 2010 survey. The comparator theorem remains explicitly labeled as having body by sorry; no human review is claimed. The source-derived generator was hardened on 2026-10-14 so a formalization note covering multiple comparator results no longer copies its combined Scope prose onto each declaration; those targets now use declaration-specific source comments when available and otherwise remain explicitly bounded to the exact Lean statement. The remaining source-derived annotations were generated mechanically from pinned formalization notes and source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

671 declarations, 1 contain sorry, 0 declared as axioms

instance OAI.SnakyCertificate.rotationModulus_neZero line 7
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:7 (same declaration text).
instance OAI.SnakyCertificate.digitModulus_neZero line 9
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:9 (same declaration text).
abbrev OAI.SnakyCertificate.Cell line 11
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:11 (same declaration text).
def OAI.SnakyCertificate.origin line 13
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:13 (same declaration text).
def OAI.SnakyCertificate.snaky line 15
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:15 (same declaration text).
def OAI.SnakyCertificate.orient line 17
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:17 (same declaration text).
def OAI.SnakyCertificate.placement line 28
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:28 (same declaration text).
def OAI.SnakyCertificate.basePoint line 30
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:30 (same declaration text).
def OAI.SnakyCertificate.baseEnvelope line 32
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:32 (same declaration text).
def OAI.SnakyCertificate.baseRequired line 35
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:35 (same declaration text).
structure OAI.SnakyCertificate.Term line 37
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:37 (same declaration text).
def OAI.SnakyCertificate.Term.shift line 44
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:44 (same declaration text).
structure OAI.SnakyCertificate.Entry line 46
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:46 (same declaration text).
def OAI.SnakyCertificate.emptyEntry line 51
Also declared: OAI/Combinatorics/SnakyCertificate/Basic.lean:51 (same declaration text).
def OAI.SnakyCertificate.entry_6 line 53
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:7 (same declaration text).
def OAI.SnakyCertificate.entry_7 line 55
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:9 (same declaration text).
def OAI.SnakyCertificate.entry_8 line 57
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:11 (same declaration text).
def OAI.SnakyCertificate.entry_9 line 59
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:13 (same declaration text).
def OAI.SnakyCertificate.entry_10 line 61
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:15 (same declaration text).
def OAI.SnakyCertificate.entry_11 line 63
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:17 (same declaration text).
def OAI.SnakyCertificate.entry_12 line 65
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:19 (same declaration text).
def OAI.SnakyCertificate.entry_13 line 67
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:21 (same declaration text).
def OAI.SnakyCertificate.entry_14 line 69
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:23 (same declaration text).
def OAI.SnakyCertificate.entry_15 line 71
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:25 (same declaration text).
def OAI.SnakyCertificate.entry_16 line 73
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:27 (same declaration text).
def OAI.SnakyCertificate.entry_17 line 75
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:29 (same declaration text).
def OAI.SnakyCertificate.entry_18 line 77
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:31 (same declaration text).
def OAI.SnakyCertificate.entry_19 line 79
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:33 (same declaration text).
def OAI.SnakyCertificate.entry_20 line 81
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:35 (same declaration text).
def OAI.SnakyCertificate.entry_21 line 83
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:37 (same declaration text).
def OAI.SnakyCertificate.entry_22 line 85
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:39 (same declaration text).
def OAI.SnakyCertificate.entry_23 line 87
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:41 (same declaration text).
def OAI.SnakyCertificate.entry_24 line 89
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:43 (same declaration text).
def OAI.SnakyCertificate.entry_25 line 91
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:45 (same declaration text).
def OAI.SnakyCertificate.entry_26 line 93
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:47 (same declaration text).
def OAI.SnakyCertificate.entry_27 line 95
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:49 (same declaration text).
def OAI.SnakyCertificate.entry_28 line 97
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:51 (same declaration text).
def OAI.SnakyCertificate.entry_29 line 99
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:53 (same declaration text).
def OAI.SnakyCertificate.entry_30 line 101
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:55 (same declaration text).
def OAI.SnakyCertificate.entry_31 line 103
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:57 (same declaration text).
def OAI.SnakyCertificate.entry_32 line 105
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:59 (same declaration text).
def OAI.SnakyCertificate.entry_33 line 107
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:61 (same declaration text).
def OAI.SnakyCertificate.entry_34 line 109
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:63 (same declaration text).
def OAI.SnakyCertificate.entry_35 line 111
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:65 (same declaration text).
def OAI.SnakyCertificate.entry_36 line 113
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:67 (same declaration text).
def OAI.SnakyCertificate.entry_37 line 115
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:69 (same declaration text).
def OAI.SnakyCertificate.entry_38 line 117
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:71 (same declaration text).
def OAI.SnakyCertificate.entry_39 line 119
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:73 (same declaration text).
def OAI.SnakyCertificate.entry_40 line 121
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:75 (same declaration text).
def OAI.SnakyCertificate.entry_41 line 123
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:77 (same declaration text).
def OAI.SnakyCertificate.entry_42 line 125
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:79 (same declaration text).
def OAI.SnakyCertificate.entry_43 line 127
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:81 (same declaration text).
def OAI.SnakyCertificate.entry_44 line 129
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:83 (same declaration text).
def OAI.SnakyCertificate.entry_45 line 131
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:85 (same declaration text).
def OAI.SnakyCertificate.entry_46 line 133
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:87 (same declaration text).
def OAI.SnakyCertificate.entry_47 line 135
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:89 (same declaration text).
def OAI.SnakyCertificate.entry_48 line 137
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:91 (same declaration text).
def OAI.SnakyCertificate.entry_49 line 139
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:93 (same declaration text).
def OAI.SnakyCertificate.entry_50 line 141
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:95 (same declaration text).
def OAI.SnakyCertificate.entry_51 line 143
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:97 (same declaration text).
def OAI.SnakyCertificate.entry_52 line 145
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:99 (same declaration text).
def OAI.SnakyCertificate.entry_53 line 147
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:101 (same declaration text).
def OAI.SnakyCertificate.entry_54 line 149
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:103 (same declaration text).
def OAI.SnakyCertificate.entry_55 line 151
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:105 (same declaration text).
def OAI.SnakyCertificate.entry_56 line 153
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:107 (same declaration text).
def OAI.SnakyCertificate.entry_57 line 155
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:109 (same declaration text).
def OAI.SnakyCertificate.entry_58 line 157
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:111 (same declaration text).
def OAI.SnakyCertificate.entry_59 line 159
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:113 (same declaration text).
def OAI.SnakyCertificate.entry_60 line 161
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:115 (same declaration text).
def OAI.SnakyCertificate.entry_61 line 163
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:117 (same declaration text).
def OAI.SnakyCertificate.entry_62 line 165
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:119 (same declaration text).
def OAI.SnakyCertificate.entry_63 line 167
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:121 (same declaration text).
def OAI.SnakyCertificate.entry_64 line 169
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:123 (same declaration text).
def OAI.SnakyCertificate.entry_65 line 171
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:125 (same declaration text).
def OAI.SnakyCertificate.entry_66 line 173
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:127 (same declaration text).
def OAI.SnakyCertificate.entry_67 line 175
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:129 (same declaration text).
def OAI.SnakyCertificate.entry_68 line 177
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:131 (same declaration text).
def OAI.SnakyCertificate.entry_69 line 179
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:133 (same declaration text).
def OAI.SnakyCertificate.entry_70 line 181
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:135 (same declaration text).
def OAI.SnakyCertificate.entry_71 line 183
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:137 (same declaration text).
def OAI.SnakyCertificate.entry_72 line 185
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:139 (same declaration text).
def OAI.SnakyCertificate.entry_73 line 187
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:141 (same declaration text).
def OAI.SnakyCertificate.entry_74 line 189
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:143 (same declaration text).
def OAI.SnakyCertificate.entry_75 line 191
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:145 (same declaration text).
def OAI.SnakyCertificate.entry_76 line 193
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:147 (same declaration text).
def OAI.SnakyCertificate.entry_77 line 195
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:149 (same declaration text).
def OAI.SnakyCertificate.entry_78 line 197
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:151 (same declaration text).
def OAI.SnakyCertificate.entry_79 line 199
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:153 (same declaration text).
def OAI.SnakyCertificate.entry_80 line 201
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:155 (same declaration text).
def OAI.SnakyCertificate.entry_81 line 203
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:157 (same declaration text).
def OAI.SnakyCertificate.entry_82 line 205
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:159 (same declaration text).
def OAI.SnakyCertificate.entry_83 line 207
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:161 (same declaration text).
def OAI.SnakyCertificate.entry_84 line 209
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:163 (same declaration text).
def OAI.SnakyCertificate.entry_85 line 211
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:165 (same declaration text).
def OAI.SnakyCertificate.entry_86 line 213
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:167 (same declaration text).
def OAI.SnakyCertificate.entry_87 line 215
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:169 (same declaration text).
def OAI.SnakyCertificate.entry_88 line 217
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:171 (same declaration text).
def OAI.SnakyCertificate.entry_89 line 219
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:173 (same declaration text).
def OAI.SnakyCertificate.entry_90 line 221
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:175 (same declaration text).
def OAI.SnakyCertificate.entry_91 line 223
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:177 (same declaration text).
def OAI.SnakyCertificate.entry_92 line 225
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:179 (same declaration text).
def OAI.SnakyCertificate.entry_93 line 227
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:181 (same declaration text).
def OAI.SnakyCertificate.entry_94 line 229
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:183 (same declaration text).
def OAI.SnakyCertificate.entry_95 line 231
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:185 (same declaration text).
def OAI.SnakyCertificate.entry_96 line 233
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:187 (same declaration text).
def OAI.SnakyCertificate.entry_97 line 235
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:189 (same declaration text).
def OAI.SnakyCertificate.entry_98 line 237
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:191 (same declaration text).
def OAI.SnakyCertificate.entry_99 line 239
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:193 (same declaration text).
def OAI.SnakyCertificate.entry_100 line 241
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:195 (same declaration text).
def OAI.SnakyCertificate.entry_101 line 243
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:197 (same declaration text).
def OAI.SnakyCertificate.entry_102 line 245
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:199 (same declaration text).
def OAI.SnakyCertificate.entry_103 line 247
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:201 (same declaration text).
def OAI.SnakyCertificate.entry_104 line 249
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:203 (same declaration text).
def OAI.SnakyCertificate.entry_105 line 251
Also declared: OAI/Combinatorics/SnakyCertificate/Entries00.lean:205 (same declaration text).
def OAI.SnakyCertificate.entry_106 line 253
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:7 (same declaration text).
def OAI.SnakyCertificate.entry_107 line 255
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:9 (same declaration text).
def OAI.SnakyCertificate.entry_108 line 257
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:11 (same declaration text).
def OAI.SnakyCertificate.entry_109 line 259
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:13 (same declaration text).
def OAI.SnakyCertificate.entry_110 line 261
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:15 (same declaration text).
def OAI.SnakyCertificate.entry_111 line 263
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:17 (same declaration text).
def OAI.SnakyCertificate.entry_112 line 265
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:19 (same declaration text).
def OAI.SnakyCertificate.entry_113 line 267
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:21 (same declaration text).
def OAI.SnakyCertificate.entry_114 line 269
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:23 (same declaration text).
def OAI.SnakyCertificate.entry_115 line 271
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:25 (same declaration text).
def OAI.SnakyCertificate.entry_116 line 273
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:27 (same declaration text).
def OAI.SnakyCertificate.entry_117 line 275
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:29 (same declaration text).
def OAI.SnakyCertificate.entry_118 line 277
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:31 (same declaration text).
def OAI.SnakyCertificate.entry_119 line 279
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:33 (same declaration text).
def OAI.SnakyCertificate.entry_120 line 281
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:35 (same declaration text).
def OAI.SnakyCertificate.entry_121 line 283
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:37 (same declaration text).
def OAI.SnakyCertificate.entry_122 line 285
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:39 (same declaration text).
def OAI.SnakyCertificate.entry_123 line 287
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:41 (same declaration text).
def OAI.SnakyCertificate.entry_124 line 289
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:43 (same declaration text).
def OAI.SnakyCertificate.entry_125 line 291
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:45 (same declaration text).
def OAI.SnakyCertificate.entry_126 line 293
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:47 (same declaration text).
def OAI.SnakyCertificate.entry_127 line 295
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:49 (same declaration text).
def OAI.SnakyCertificate.entry_128 line 297
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:51 (same declaration text).
def OAI.SnakyCertificate.entry_129 line 299
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:53 (same declaration text).
def OAI.SnakyCertificate.entry_130 line 301
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:55 (same declaration text).
def OAI.SnakyCertificate.entry_131 line 303
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:57 (same declaration text).
def OAI.SnakyCertificate.entry_132 line 305
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:59 (same declaration text).
def OAI.SnakyCertificate.entry_133 line 307
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:61 (same declaration text).
def OAI.SnakyCertificate.entry_134 line 309
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:63 (same declaration text).
def OAI.SnakyCertificate.entry_135 line 311
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:65 (same declaration text).
def OAI.SnakyCertificate.entry_136 line 313
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:67 (same declaration text).
def OAI.SnakyCertificate.entry_137 line 315
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:69 (same declaration text).
def OAI.SnakyCertificate.entry_138 line 317
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:71 (same declaration text).
def OAI.SnakyCertificate.entry_139 line 319
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:73 (same declaration text).
def OAI.SnakyCertificate.entry_140 line 321
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:75 (same declaration text).
def OAI.SnakyCertificate.entry_141 line 323
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:77 (same declaration text).
def OAI.SnakyCertificate.entry_142 line 325
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:79 (same declaration text).
def OAI.SnakyCertificate.entry_143 line 327
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:81 (same declaration text).
def OAI.SnakyCertificate.entry_144 line 329
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:83 (same declaration text).
def OAI.SnakyCertificate.entry_145 line 331
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:85 (same declaration text).
def OAI.SnakyCertificate.entry_146 line 333
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:87 (same declaration text).
def OAI.SnakyCertificate.entry_147 line 335
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:89 (same declaration text).
def OAI.SnakyCertificate.entry_148 line 337
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:91 (same declaration text).
def OAI.SnakyCertificate.entry_149 line 339
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:93 (same declaration text).
def OAI.SnakyCertificate.entry_150 line 341
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:95 (same declaration text).
def OAI.SnakyCertificate.entry_151 line 343
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:97 (same declaration text).
def OAI.SnakyCertificate.entry_152 line 345
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:99 (same declaration text).
def OAI.SnakyCertificate.entry_153 line 347
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:101 (same declaration text).
def OAI.SnakyCertificate.entry_154 line 349
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:103 (same declaration text).
def OAI.SnakyCertificate.entry_155 line 351
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:105 (same declaration text).
def OAI.SnakyCertificate.entry_156 line 353
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:107 (same declaration text).
def OAI.SnakyCertificate.entry_157 line 355
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:109 (same declaration text).
def OAI.SnakyCertificate.entry_158 line 357
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:111 (same declaration text).
def OAI.SnakyCertificate.entry_159 line 359
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:113 (same declaration text).
def OAI.SnakyCertificate.entry_160 line 361
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:115 (same declaration text).
def OAI.SnakyCertificate.entry_161 line 363
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:117 (same declaration text).
def OAI.SnakyCertificate.entry_162 line 365
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:119 (same declaration text).
def OAI.SnakyCertificate.entry_163 line 367
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:121 (same declaration text).
def OAI.SnakyCertificate.entry_164 line 369
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:123 (same declaration text).
def OAI.SnakyCertificate.entry_165 line 371
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:125 (same declaration text).
def OAI.SnakyCertificate.entry_166 line 373
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:127 (same declaration text).
def OAI.SnakyCertificate.entry_167 line 375
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:129 (same declaration text).
def OAI.SnakyCertificate.entry_168 line 377
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:131 (same declaration text).
def OAI.SnakyCertificate.entry_169 line 379
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:133 (same declaration text).
def OAI.SnakyCertificate.entry_170 line 381
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:135 (same declaration text).
def OAI.SnakyCertificate.entry_171 line 383
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:137 (same declaration text).
def OAI.SnakyCertificate.entry_172 line 385
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:139 (same declaration text).
def OAI.SnakyCertificate.entry_173 line 387
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:141 (same declaration text).
def OAI.SnakyCertificate.entry_174 line 389
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:143 (same declaration text).
def OAI.SnakyCertificate.entry_175 line 391
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:145 (same declaration text).
def OAI.SnakyCertificate.entry_176 line 393
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:147 (same declaration text).
def OAI.SnakyCertificate.entry_177 line 395
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:149 (same declaration text).
def OAI.SnakyCertificate.entry_178 line 397
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:151 (same declaration text).
def OAI.SnakyCertificate.entry_179 line 399
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:153 (same declaration text).
def OAI.SnakyCertificate.entry_180 line 401
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:155 (same declaration text).
def OAI.SnakyCertificate.entry_181 line 403
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:157 (same declaration text).
def OAI.SnakyCertificate.entry_182 line 405
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:159 (same declaration text).
def OAI.SnakyCertificate.entry_183 line 407
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:161 (same declaration text).
def OAI.SnakyCertificate.entry_184 line 409
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:163 (same declaration text).
def OAI.SnakyCertificate.entry_185 line 411
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:165 (same declaration text).
def OAI.SnakyCertificate.entry_186 line 413
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:167 (same declaration text).
def OAI.SnakyCertificate.entry_187 line 415
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:169 (same declaration text).
def OAI.SnakyCertificate.entry_188 line 417
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:171 (same declaration text).
def OAI.SnakyCertificate.entry_189 line 419
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:173 (same declaration text).
def OAI.SnakyCertificate.entry_190 line 421
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:175 (same declaration text).
def OAI.SnakyCertificate.entry_191 line 423
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:177 (same declaration text).
def OAI.SnakyCertificate.entry_192 line 425
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:179 (same declaration text).
def OAI.SnakyCertificate.entry_193 line 427
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:181 (same declaration text).
def OAI.SnakyCertificate.entry_194 line 429
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:183 (same declaration text).
def OAI.SnakyCertificate.entry_195 line 431
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:185 (same declaration text).
def OAI.SnakyCertificate.entry_196 line 433
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:187 (same declaration text).
def OAI.SnakyCertificate.entry_197 line 435
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:189 (same declaration text).
def OAI.SnakyCertificate.entry_198 line 437
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:191 (same declaration text).
def OAI.SnakyCertificate.entry_199 line 439
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:193 (same declaration text).
def OAI.SnakyCertificate.entry_200 line 441
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:195 (same declaration text).
def OAI.SnakyCertificate.entry_201 line 443
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:197 (same declaration text).
def OAI.SnakyCertificate.entry_202 line 445
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:199 (same declaration text).
def OAI.SnakyCertificate.entry_203 line 447
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:201 (same declaration text).
def OAI.SnakyCertificate.entry_204 line 449
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:203 (same declaration text).
def OAI.SnakyCertificate.entry_205 line 451
Also declared: OAI/Combinatorics/SnakyCertificate/Entries01.lean:205 (same declaration text).
def OAI.SnakyCertificate.entry_206 line 453
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:7 (same declaration text).
def OAI.SnakyCertificate.entry_207 line 455
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:9 (same declaration text).
def OAI.SnakyCertificate.entry_208 line 457
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:11 (same declaration text).
def OAI.SnakyCertificate.entry_209 line 459
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:13 (same declaration text).
def OAI.SnakyCertificate.entry_210 line 461
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:15 (same declaration text).
def OAI.SnakyCertificate.entry_211 line 463
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:17 (same declaration text).
def OAI.SnakyCertificate.entry_212 line 465
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:19 (same declaration text).
def OAI.SnakyCertificate.entry_213 line 467
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:21 (same declaration text).
def OAI.SnakyCertificate.entry_214 line 469
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:23 (same declaration text).
def OAI.SnakyCertificate.entry_215 line 471
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:25 (same declaration text).
def OAI.SnakyCertificate.entry_216 line 473
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:27 (same declaration text).
def OAI.SnakyCertificate.entry_217 line 475
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:29 (same declaration text).
def OAI.SnakyCertificate.entry_218 line 477
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:31 (same declaration text).
def OAI.SnakyCertificate.entry_219 line 479
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:33 (same declaration text).
def OAI.SnakyCertificate.entry_220 line 481
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:35 (same declaration text).
def OAI.SnakyCertificate.entry_221 line 483
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:37 (same declaration text).
def OAI.SnakyCertificate.entry_222 line 485
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:39 (same declaration text).
def OAI.SnakyCertificate.entry_223 line 487
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:41 (same declaration text).
def OAI.SnakyCertificate.entry_224 line 489
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:43 (same declaration text).
def OAI.SnakyCertificate.entry_225 line 491
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:45 (same declaration text).
def OAI.SnakyCertificate.entry_226 line 493
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:47 (same declaration text).
def OAI.SnakyCertificate.entry_227 line 495
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:49 (same declaration text).
def OAI.SnakyCertificate.entry_228 line 497
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:51 (same declaration text).
def OAI.SnakyCertificate.entry_229 line 499
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:53 (same declaration text).
def OAI.SnakyCertificate.entry_230 line 501
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:55 (same declaration text).
def OAI.SnakyCertificate.entry_231 line 503
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:57 (same declaration text).
def OAI.SnakyCertificate.entry_232 line 505
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:59 (same declaration text).
def OAI.SnakyCertificate.entry_233 line 507
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:61 (same declaration text).
def OAI.SnakyCertificate.entry_234 line 509
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:63 (same declaration text).
def OAI.SnakyCertificate.entry_235 line 511
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:65 (same declaration text).
def OAI.SnakyCertificate.entry_236 line 513
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:67 (same declaration text).
def OAI.SnakyCertificate.entry_237 line 515
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:69 (same declaration text).
def OAI.SnakyCertificate.entry_238 line 517
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:71 (same declaration text).
def OAI.SnakyCertificate.entry_239 line 519
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:73 (same declaration text).
def OAI.SnakyCertificate.entry_240 line 521
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:75 (same declaration text).
def OAI.SnakyCertificate.entry_241 line 523
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:77 (same declaration text).
def OAI.SnakyCertificate.entry_242 line 525
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:79 (same declaration text).
def OAI.SnakyCertificate.entry_243 line 527
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:81 (same declaration text).
def OAI.SnakyCertificate.entry_244 line 529
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:83 (same declaration text).
def OAI.SnakyCertificate.entry_245 line 531
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:85 (same declaration text).
def OAI.SnakyCertificate.entry_246 line 533
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:87 (same declaration text).
def OAI.SnakyCertificate.entry_247 line 535
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:89 (same declaration text).
def OAI.SnakyCertificate.entry_248 line 537
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:91 (same declaration text).
def OAI.SnakyCertificate.entry_249 line 539
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:93 (same declaration text).
def OAI.SnakyCertificate.entry_250 line 541
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:95 (same declaration text).
def OAI.SnakyCertificate.entry_251 line 543
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:97 (same declaration text).
def OAI.SnakyCertificate.entry_252 line 545
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:99 (same declaration text).
def OAI.SnakyCertificate.entry_253 line 547
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:101 (same declaration text).
def OAI.SnakyCertificate.entry_254 line 549
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:103 (same declaration text).
def OAI.SnakyCertificate.entry_255 line 551
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:105 (same declaration text).
def OAI.SnakyCertificate.entry_256 line 553
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:107 (same declaration text).
def OAI.SnakyCertificate.entry_257 line 555
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:109 (same declaration text).
def OAI.SnakyCertificate.entry_258 line 557
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:111 (same declaration text).
def OAI.SnakyCertificate.entry_259 line 559
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:113 (same declaration text).
def OAI.SnakyCertificate.entry_260 line 561
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:115 (same declaration text).
def OAI.SnakyCertificate.entry_261 line 563
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:117 (same declaration text).
def OAI.SnakyCertificate.entry_262 line 565
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:119 (same declaration text).
def OAI.SnakyCertificate.entry_263 line 567
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:121 (same declaration text).
def OAI.SnakyCertificate.entry_264 line 569
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:123 (same declaration text).
def OAI.SnakyCertificate.entry_265 line 571
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:125 (same declaration text).
def OAI.SnakyCertificate.entry_266 line 573
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:127 (same declaration text).
def OAI.SnakyCertificate.entry_267 line 575
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:129 (same declaration text).
def OAI.SnakyCertificate.entry_268 line 577
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:131 (same declaration text).
def OAI.SnakyCertificate.entry_269 line 579
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:133 (same declaration text).
def OAI.SnakyCertificate.entry_270 line 581
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:135 (same declaration text).
def OAI.SnakyCertificate.entry_271 line 583
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:137 (same declaration text).
def OAI.SnakyCertificate.entry_272 line 585
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:139 (same declaration text).
def OAI.SnakyCertificate.entry_273 line 587
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:141 (same declaration text).
def OAI.SnakyCertificate.entry_274 line 589
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:143 (same declaration text).
def OAI.SnakyCertificate.entry_275 line 591
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:145 (same declaration text).
def OAI.SnakyCertificate.entry_276 line 593
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:147 (same declaration text).
def OAI.SnakyCertificate.entry_277 line 595
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:149 (same declaration text).
def OAI.SnakyCertificate.entry_278 line 597
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:151 (same declaration text).
def OAI.SnakyCertificate.entry_279 line 599
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:153 (same declaration text).
def OAI.SnakyCertificate.entry_280 line 601
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:155 (same declaration text).
def OAI.SnakyCertificate.entry_281 line 603
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:157 (same declaration text).
def OAI.SnakyCertificate.entry_282 line 605
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:159 (same declaration text).
def OAI.SnakyCertificate.entry_283 line 607
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:161 (same declaration text).
def OAI.SnakyCertificate.entry_284 line 609
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:163 (same declaration text).
def OAI.SnakyCertificate.entry_285 line 611
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:165 (same declaration text).
def OAI.SnakyCertificate.entry_286 line 613
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:167 (same declaration text).
def OAI.SnakyCertificate.entry_287 line 615
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:169 (same declaration text).
def OAI.SnakyCertificate.entry_288 line 617
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:171 (same declaration text).
def OAI.SnakyCertificate.entry_289 line 619
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:173 (same declaration text).
def OAI.SnakyCertificate.entry_290 line 621
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:175 (same declaration text).
def OAI.SnakyCertificate.entry_291 line 623
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:177 (same declaration text).
def OAI.SnakyCertificate.entry_292 line 625
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:179 (same declaration text).
def OAI.SnakyCertificate.entry_293 line 627
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:181 (same declaration text).
def OAI.SnakyCertificate.entry_294 line 629
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:183 (same declaration text).
def OAI.SnakyCertificate.entry_295 line 631
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:185 (same declaration text).
def OAI.SnakyCertificate.entry_296 line 633
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:187 (same declaration text).
def OAI.SnakyCertificate.entry_297 line 635
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:189 (same declaration text).
def OAI.SnakyCertificate.entry_298 line 637
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:191 (same declaration text).
def OAI.SnakyCertificate.entry_299 line 639
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:193 (same declaration text).
def OAI.SnakyCertificate.entry_300 line 641
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:195 (same declaration text).
def OAI.SnakyCertificate.entry_301 line 643
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:197 (same declaration text).
def OAI.SnakyCertificate.entry_302 line 645
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:199 (same declaration text).
def OAI.SnakyCertificate.entry_303 line 647
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:201 (same declaration text).
def OAI.SnakyCertificate.entry_304 line 649
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:203 (same declaration text).
def OAI.SnakyCertificate.entry_305 line 651
Also declared: OAI/Combinatorics/SnakyCertificate/Entries02.lean:205 (same declaration text).
def OAI.SnakyCertificate.entry_306 line 653
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:7 (same declaration text).
def OAI.SnakyCertificate.entry_307 line 655
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:9 (same declaration text).
def OAI.SnakyCertificate.entry_308 line 657
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:11 (same declaration text).
def OAI.SnakyCertificate.entry_309 line 659
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:13 (same declaration text).
def OAI.SnakyCertificate.entry_310 line 661
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:15 (same declaration text).
def OAI.SnakyCertificate.entry_311 line 663
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:17 (same declaration text).
def OAI.SnakyCertificate.entry_312 line 665
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:19 (same declaration text).
def OAI.SnakyCertificate.entry_313 line 667
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:21 (same declaration text).
def OAI.SnakyCertificate.entry_314 line 669
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:23 (same declaration text).
def OAI.SnakyCertificate.entry_315 line 671
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:25 (same declaration text).
def OAI.SnakyCertificate.entry_316 line 673
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:27 (same declaration text).
def OAI.SnakyCertificate.entry_317 line 675
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:29 (same declaration text).
def OAI.SnakyCertificate.entry_318 line 677
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:31 (same declaration text).
def OAI.SnakyCertificate.entry_319 line 679
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:33 (same declaration text).
def OAI.SnakyCertificate.entry_320 line 681
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:35 (same declaration text).
def OAI.SnakyCertificate.entry_321 line 683
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:37 (same declaration text).
def OAI.SnakyCertificate.entry_322 line 685
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:39 (same declaration text).
def OAI.SnakyCertificate.entry_323 line 687
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:41 (same declaration text).
def OAI.SnakyCertificate.entry_324 line 689
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:43 (same declaration text).
def OAI.SnakyCertificate.entry_325 line 691
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:45 (same declaration text).
def OAI.SnakyCertificate.entry_326 line 693
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:47 (same declaration text).
def OAI.SnakyCertificate.entry_327 line 695
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:49 (same declaration text).
def OAI.SnakyCertificate.entry_328 line 697
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:51 (same declaration text).
def OAI.SnakyCertificate.entry_329 line 699
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:53 (same declaration text).
def OAI.SnakyCertificate.entry_330 line 701
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:55 (same declaration text).
def OAI.SnakyCertificate.entry_331 line 703
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:57 (same declaration text).
def OAI.SnakyCertificate.entry_332 line 705
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:59 (same declaration text).
def OAI.SnakyCertificate.entry_333 line 707
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:61 (same declaration text).
def OAI.SnakyCertificate.entry_334 line 709
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:63 (same declaration text).
def OAI.SnakyCertificate.entry_335 line 711
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:65 (same declaration text).
def OAI.SnakyCertificate.entry_336 line 713
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:67 (same declaration text).
def OAI.SnakyCertificate.entry_337 line 715
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:69 (same declaration text).
def OAI.SnakyCertificate.entry_338 line 717
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:71 (same declaration text).
def OAI.SnakyCertificate.entry_339 line 719
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:73 (same declaration text).
def OAI.SnakyCertificate.entry_340 line 721
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:75 (same declaration text).
def OAI.SnakyCertificate.entry_341 line 723
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:77 (same declaration text).
def OAI.SnakyCertificate.entry_342 line 725
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:79 (same declaration text).
def OAI.SnakyCertificate.entry_343 line 727
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:81 (same declaration text).
def OAI.SnakyCertificate.entry_344 line 729
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:83 (same declaration text).
def OAI.SnakyCertificate.entry_345 line 731
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:85 (same declaration text).
def OAI.SnakyCertificate.entry_346 line 733
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:87 (same declaration text).
def OAI.SnakyCertificate.entry_347 line 735
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:89 (same declaration text).
def OAI.SnakyCertificate.entry_348 line 737
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:91 (same declaration text).
def OAI.SnakyCertificate.entry_349 line 739
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:93 (same declaration text).
def OAI.SnakyCertificate.entry_350 line 741
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:95 (same declaration text).
def OAI.SnakyCertificate.entry_351 line 743
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:97 (same declaration text).
def OAI.SnakyCertificate.entry_352 line 745
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:99 (same declaration text).
def OAI.SnakyCertificate.entry_353 line 747
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:101 (same declaration text).
def OAI.SnakyCertificate.entry_354 line 749
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:103 (same declaration text).
def OAI.SnakyCertificate.entry_355 line 751
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:105 (same declaration text).
def OAI.SnakyCertificate.entry_356 line 753
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:107 (same declaration text).
def OAI.SnakyCertificate.entry_357 line 755
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:109 (same declaration text).
def OAI.SnakyCertificate.entry_358 line 757
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:111 (same declaration text).
def OAI.SnakyCertificate.entry_359 line 759
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:113 (same declaration text).
def OAI.SnakyCertificate.entry_360 line 761
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:115 (same declaration text).
def OAI.SnakyCertificate.entry_361 line 763
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:117 (same declaration text).
def OAI.SnakyCertificate.entry_362 line 765
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:119 (same declaration text).
def OAI.SnakyCertificate.entry_363 line 767
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:121 (same declaration text).
def OAI.SnakyCertificate.entry_364 line 769
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:123 (same declaration text).
def OAI.SnakyCertificate.entry_365 line 771
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:125 (same declaration text).
def OAI.SnakyCertificate.entry_366 line 773
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:127 (same declaration text).
def OAI.SnakyCertificate.entry_367 line 775
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:129 (same declaration text).
def OAI.SnakyCertificate.entry_368 line 777
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:131 (same declaration text).
def OAI.SnakyCertificate.entry_369 line 779
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:133 (same declaration text).
def OAI.SnakyCertificate.entry_370 line 781
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:135 (same declaration text).
def OAI.SnakyCertificate.entry_371 line 783
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:137 (same declaration text).
def OAI.SnakyCertificate.entry_372 line 785
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:139 (same declaration text).
def OAI.SnakyCertificate.entry_373 line 787
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:141 (same declaration text).
def OAI.SnakyCertificate.entry_374 line 789
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:143 (same declaration text).
def OAI.SnakyCertificate.entry_375 line 791
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:145 (same declaration text).
def OAI.SnakyCertificate.entry_376 line 793
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:147 (same declaration text).
def OAI.SnakyCertificate.entry_377 line 795
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:149 (same declaration text).
def OAI.SnakyCertificate.entry_378 line 797
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:151 (same declaration text).
def OAI.SnakyCertificate.entry_379 line 799
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:153 (same declaration text).
def OAI.SnakyCertificate.entry_380 line 801
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:155 (same declaration text).
def OAI.SnakyCertificate.entry_381 line 803
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:157 (same declaration text).
def OAI.SnakyCertificate.entry_382 line 805
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:159 (same declaration text).
def OAI.SnakyCertificate.entry_383 line 807
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:161 (same declaration text).
def OAI.SnakyCertificate.entry_384 line 809
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:163 (same declaration text).
def OAI.SnakyCertificate.entry_385 line 811
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:165 (same declaration text).
def OAI.SnakyCertificate.entry_386 line 813
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:167 (same declaration text).
def OAI.SnakyCertificate.entry_387 line 815
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:169 (same declaration text).
def OAI.SnakyCertificate.entry_388 line 817
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:171 (same declaration text).
def OAI.SnakyCertificate.entry_389 line 819
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:173 (same declaration text).
def OAI.SnakyCertificate.entry_390 line 821
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:175 (same declaration text).
def OAI.SnakyCertificate.entry_391 line 823
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:177 (same declaration text).
def OAI.SnakyCertificate.entry_392 line 825
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:179 (same declaration text).
def OAI.SnakyCertificate.entry_393 line 827
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:181 (same declaration text).
def OAI.SnakyCertificate.entry_394 line 829
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:183 (same declaration text).
def OAI.SnakyCertificate.entry_395 line 831
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:185 (same declaration text).
def OAI.SnakyCertificate.entry_396 line 833
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:187 (same declaration text).
def OAI.SnakyCertificate.entry_397 line 835
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:189 (same declaration text).
def OAI.SnakyCertificate.entry_398 line 837
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:191 (same declaration text).
def OAI.SnakyCertificate.entry_399 line 839
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:193 (same declaration text).
def OAI.SnakyCertificate.entry_400 line 841
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:195 (same declaration text).
def OAI.SnakyCertificate.entry_401 line 843
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:197 (same declaration text).
def OAI.SnakyCertificate.entry_402 line 845
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:199 (same declaration text).
def OAI.SnakyCertificate.entry_403 line 847
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:201 (same declaration text).
def OAI.SnakyCertificate.entry_404 line 849
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:203 (same declaration text).
def OAI.SnakyCertificate.entry_405 line 851
Also declared: OAI/Combinatorics/SnakyCertificate/Entries03.lean:205 (same declaration text).
def OAI.SnakyCertificate.entry_406 line 853
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:7 (same declaration text).
def OAI.SnakyCertificate.entry_407 line 855
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:9 (same declaration text).
def OAI.SnakyCertificate.entry_408 line 857
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:11 (same declaration text).
def OAI.SnakyCertificate.entry_409 line 859
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:13 (same declaration text).
def OAI.SnakyCertificate.entry_410 line 861
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:15 (same declaration text).
def OAI.SnakyCertificate.entry_411 line 863
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:17 (same declaration text).
def OAI.SnakyCertificate.entry_412 line 865
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:19 (same declaration text).
def OAI.SnakyCertificate.entry_413 line 867
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:21 (same declaration text).
def OAI.SnakyCertificate.entry_414 line 869
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:23 (same declaration text).
def OAI.SnakyCertificate.entry_415 line 871
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:25 (same declaration text).
def OAI.SnakyCertificate.entry_416 line 873
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:27 (same declaration text).
def OAI.SnakyCertificate.entry_417 line 875
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:29 (same declaration text).
def OAI.SnakyCertificate.entry_418 line 877
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:31 (same declaration text).
def OAI.SnakyCertificate.entry_419 line 879
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:33 (same declaration text).
def OAI.SnakyCertificate.entry_420 line 881
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:35 (same declaration text).
def OAI.SnakyCertificate.entry_421 line 883
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:37 (same declaration text).
def OAI.SnakyCertificate.entry_422 line 885
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:39 (same declaration text).
def OAI.SnakyCertificate.entry_423 line 887
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:41 (same declaration text).
def OAI.SnakyCertificate.entry_424 line 889
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:43 (same declaration text).
def OAI.SnakyCertificate.entry_425 line 891
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:45 (same declaration text).
def OAI.SnakyCertificate.entry_426 line 893
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:47 (same declaration text).
def OAI.SnakyCertificate.entry_427 line 895
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:49 (same declaration text).
def OAI.SnakyCertificate.entry_428 line 897
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:51 (same declaration text).
def OAI.SnakyCertificate.entry_429 line 899
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:53 (same declaration text).
def OAI.SnakyCertificate.entry_430 line 901
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:55 (same declaration text).
def OAI.SnakyCertificate.entry_431 line 903
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:57 (same declaration text).
def OAI.SnakyCertificate.entry_432 line 905
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:59 (same declaration text).
def OAI.SnakyCertificate.entry_433 line 907
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:61 (same declaration text).
def OAI.SnakyCertificate.entry_434 line 909
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:63 (same declaration text).
def OAI.SnakyCertificate.entry_435 line 911
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:65 (same declaration text).
def OAI.SnakyCertificate.entry_436 line 913
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:67 (same declaration text).
def OAI.SnakyCertificate.entry_437 line 915
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:69 (same declaration text).
def OAI.SnakyCertificate.entry_438 line 917
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:71 (same declaration text).
def OAI.SnakyCertificate.entry_439 line 919
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:73 (same declaration text).
def OAI.SnakyCertificate.entry_440 line 921
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:75 (same declaration text).
def OAI.SnakyCertificate.entry_441 line 923
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:77 (same declaration text).
def OAI.SnakyCertificate.entry_442 line 925
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:79 (same declaration text).
def OAI.SnakyCertificate.entry_443 line 927
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:81 (same declaration text).
def OAI.SnakyCertificate.entry_444 line 929
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:83 (same declaration text).
def OAI.SnakyCertificate.entry_445 line 931
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:85 (same declaration text).
def OAI.SnakyCertificate.entry_446 line 933
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:87 (same declaration text).
def OAI.SnakyCertificate.entry_447 line 935
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:89 (same declaration text).
def OAI.SnakyCertificate.entry_448 line 937
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:91 (same declaration text).
def OAI.SnakyCertificate.entry_449 line 939
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:93 (same declaration text).
def OAI.SnakyCertificate.entry_450 line 941
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:95 (same declaration text).
def OAI.SnakyCertificate.entry_451 line 943
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:97 (same declaration text).
def OAI.SnakyCertificate.entry_452 line 945
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:99 (same declaration text).
def OAI.SnakyCertificate.entry_453 line 947
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:101 (same declaration text).
def OAI.SnakyCertificate.entry_454 line 949
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:103 (same declaration text).
def OAI.SnakyCertificate.entry_455 line 951
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:105 (same declaration text).
def OAI.SnakyCertificate.entry_456 line 953
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:107 (same declaration text).
def OAI.SnakyCertificate.entry_457 line 955
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:109 (same declaration text).
def OAI.SnakyCertificate.entry_458 line 957
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:111 (same declaration text).
def OAI.SnakyCertificate.entry_459 line 959
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:113 (same declaration text).
def OAI.SnakyCertificate.entry_460 line 961
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:115 (same declaration text).
def OAI.SnakyCertificate.entry_461 line 963
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:117 (same declaration text).
def OAI.SnakyCertificate.entry_462 line 965
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:119 (same declaration text).
def OAI.SnakyCertificate.entry_463 line 967
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:121 (same declaration text).
def OAI.SnakyCertificate.entry_464 line 969
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:123 (same declaration text).
def OAI.SnakyCertificate.entry_465 line 971
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:125 (same declaration text).
def OAI.SnakyCertificate.entry_466 line 973
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:127 (same declaration text).
def OAI.SnakyCertificate.entry_467 line 975
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:129 (same declaration text).
def OAI.SnakyCertificate.entry_468 line 977
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:131 (same declaration text).
def OAI.SnakyCertificate.entry_469 line 979
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:133 (same declaration text).
def OAI.SnakyCertificate.entry_470 line 981
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:135 (same declaration text).
def OAI.SnakyCertificate.entry_471 line 983
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:137 (same declaration text).
def OAI.SnakyCertificate.entry_472 line 985
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:139 (same declaration text).
def OAI.SnakyCertificate.entry_473 line 987
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:141 (same declaration text).
def OAI.SnakyCertificate.entry_474 line 989
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:143 (same declaration text).
def OAI.SnakyCertificate.entry_475 line 991
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:145 (same declaration text).
def OAI.SnakyCertificate.entry_476 line 993
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:147 (same declaration text).
def OAI.SnakyCertificate.entry_477 line 995
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:149 (same declaration text).
def OAI.SnakyCertificate.entry_478 line 997
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:151 (same declaration text).
def OAI.SnakyCertificate.entry_479 line 999
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:153 (same declaration text).
def OAI.SnakyCertificate.entry_480 line 1001
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:155 (same declaration text).
def OAI.SnakyCertificate.entry_481 line 1003
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:157 (same declaration text).
def OAI.SnakyCertificate.entry_482 line 1005
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:159 (same declaration text).
def OAI.SnakyCertificate.entry_483 line 1007
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:161 (same declaration text).
def OAI.SnakyCertificate.entry_484 line 1009
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:163 (same declaration text).
def OAI.SnakyCertificate.entry_485 line 1011
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:165 (same declaration text).
def OAI.SnakyCertificate.entry_486 line 1013
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:167 (same declaration text).
def OAI.SnakyCertificate.entry_487 line 1015
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:169 (same declaration text).
def OAI.SnakyCertificate.entry_488 line 1017
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:171 (same declaration text).
def OAI.SnakyCertificate.entry_489 line 1019
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:173 (same declaration text).
def OAI.SnakyCertificate.entry_490 line 1021
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:175 (same declaration text).
def OAI.SnakyCertificate.entry_491 line 1023
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:177 (same declaration text).
def OAI.SnakyCertificate.entry_492 line 1025
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:179 (same declaration text).
def OAI.SnakyCertificate.entry_493 line 1027
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:181 (same declaration text).
def OAI.SnakyCertificate.entry_494 line 1029
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:183 (same declaration text).
def OAI.SnakyCertificate.entry_495 line 1031
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:185 (same declaration text).
def OAI.SnakyCertificate.entry_496 line 1033
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:187 (same declaration text).
def OAI.SnakyCertificate.entry_497 line 1035
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:189 (same declaration text).
def OAI.SnakyCertificate.entry_498 line 1037
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:191 (same declaration text).
def OAI.SnakyCertificate.entry_499 line 1039
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:193 (same declaration text).
def OAI.SnakyCertificate.entry_500 line 1041
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:195 (same declaration text).
def OAI.SnakyCertificate.entry_501 line 1043
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:197 (same declaration text).
def OAI.SnakyCertificate.entry_502 line 1045
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:199 (same declaration text).
def OAI.SnakyCertificate.entry_503 line 1047
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:201 (same declaration text).
def OAI.SnakyCertificate.entry_504 line 1049
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:203 (same declaration text).
def OAI.SnakyCertificate.entry_505 line 1051
Also declared: OAI/Combinatorics/SnakyCertificate/Entries04.lean:205 (same declaration text).
def OAI.SnakyCertificate.entry_506 line 1053
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:7 (same declaration text).
def OAI.SnakyCertificate.entry_507 line 1055
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:9 (same declaration text).
def OAI.SnakyCertificate.entry_508 line 1057
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:11 (same declaration text).
def OAI.SnakyCertificate.entry_509 line 1059
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:13 (same declaration text).
def OAI.SnakyCertificate.entry_510 line 1061
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:15 (same declaration text).
def OAI.SnakyCertificate.entry_511 line 1063
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:17 (same declaration text).
def OAI.SnakyCertificate.entry_512 line 1065
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:19 (same declaration text).
def OAI.SnakyCertificate.entry_513 line 1067
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:21 (same declaration text).
def OAI.SnakyCertificate.entry_514 line 1069
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:23 (same declaration text).
def OAI.SnakyCertificate.entry_515 line 1071
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:25 (same declaration text).
def OAI.SnakyCertificate.entry_516 line 1073
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:27 (same declaration text).
def OAI.SnakyCertificate.entry_517 line 1075
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:29 (same declaration text).
def OAI.SnakyCertificate.entry_518 line 1077
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:31 (same declaration text).
def OAI.SnakyCertificate.entry_519 line 1079
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:33 (same declaration text).
def OAI.SnakyCertificate.entry_520 line 1081
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:35 (same declaration text).
def OAI.SnakyCertificate.entry_521 line 1083
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:37 (same declaration text).
def OAI.SnakyCertificate.entry_522 line 1085
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:39 (same declaration text).
def OAI.SnakyCertificate.entry_523 line 1087
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:41 (same declaration text).
def OAI.SnakyCertificate.entry_524 line 1089
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:43 (same declaration text).
def OAI.SnakyCertificate.entry_525 line 1091
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:45 (same declaration text).
def OAI.SnakyCertificate.entry_526 line 1093
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:47 (same declaration text).
def OAI.SnakyCertificate.entry_527 line 1095
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:49 (same declaration text).
def OAI.SnakyCertificate.entry_528 line 1097
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:51 (same declaration text).
def OAI.SnakyCertificate.entry_529 line 1099
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:53 (same declaration text).
def OAI.SnakyCertificate.entry_530 line 1101
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:55 (same declaration text).
def OAI.SnakyCertificate.entry_531 line 1103
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:57 (same declaration text).
def OAI.SnakyCertificate.entry_532 line 1105
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:59 (same declaration text).
def OAI.SnakyCertificate.entry_533 line 1107
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:61 (same declaration text).
def OAI.SnakyCertificate.entry_534 line 1109
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:63 (same declaration text).
def OAI.SnakyCertificate.entry_535 line 1111
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:65 (same declaration text).
def OAI.SnakyCertificate.entry_536 line 1113
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:67 (same declaration text).
def OAI.SnakyCertificate.entry_537 line 1115
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:69 (same declaration text).
def OAI.SnakyCertificate.entry_538 line 1117
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:71 (same declaration text).
def OAI.SnakyCertificate.entry_539 line 1119
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:73 (same declaration text).
def OAI.SnakyCertificate.entry_540 line 1121
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:75 (same declaration text).
def OAI.SnakyCertificate.entry_541 line 1123
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:77 (same declaration text).
def OAI.SnakyCertificate.entry_542 line 1125
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:79 (same declaration text).
def OAI.SnakyCertificate.entry_543 line 1127
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:81 (same declaration text).
def OAI.SnakyCertificate.entry_544 line 1129
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:83 (same declaration text).
def OAI.SnakyCertificate.entry_545 line 1131
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:85 (same declaration text).
def OAI.SnakyCertificate.entry_546 line 1133
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:87 (same declaration text).
def OAI.SnakyCertificate.entry_547 line 1135
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:89 (same declaration text).
def OAI.SnakyCertificate.entry_548 line 1137
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:91 (same declaration text).
def OAI.SnakyCertificate.entry_549 line 1139
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:93 (same declaration text).
def OAI.SnakyCertificate.entry_550 line 1141
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:95 (same declaration text).
def OAI.SnakyCertificate.entry_551 line 1143
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:97 (same declaration text).
def OAI.SnakyCertificate.entry_552 line 1145
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:99 (same declaration text).
def OAI.SnakyCertificate.entry_553 line 1147
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:101 (same declaration text).
def OAI.SnakyCertificate.entry_554 line 1149
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:103 (same declaration text).
def OAI.SnakyCertificate.entry_555 line 1151
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:105 (same declaration text).
def OAI.SnakyCertificate.entry_556 line 1153
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:107 (same declaration text).
def OAI.SnakyCertificate.entry_557 line 1155
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:109 (same declaration text).
def OAI.SnakyCertificate.entry_558 line 1157
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:111 (same declaration text).
def OAI.SnakyCertificate.entry_559 line 1159
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:113 (same declaration text).
def OAI.SnakyCertificate.entry_560 line 1161
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:115 (same declaration text).
def OAI.SnakyCertificate.entry_561 line 1163
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:117 (same declaration text).
def OAI.SnakyCertificate.entry_562 line 1165
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:119 (same declaration text).
def OAI.SnakyCertificate.entry_563 line 1167
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:121 (same declaration text).
def OAI.SnakyCertificate.entry_564 line 1169
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:123 (same declaration text).
def OAI.SnakyCertificate.entry_565 line 1171
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:125 (same declaration text).
def OAI.SnakyCertificate.entry_566 line 1173
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:127 (same declaration text).
def OAI.SnakyCertificate.entry_567 line 1175
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:129 (same declaration text).
def OAI.SnakyCertificate.entry_568 line 1177
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:131 (same declaration text).
def OAI.SnakyCertificate.entry_569 line 1179
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:133 (same declaration text).
def OAI.SnakyCertificate.entry_570 line 1181
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:135 (same declaration text).
def OAI.SnakyCertificate.entry_571 line 1183
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:137 (same declaration text).
def OAI.SnakyCertificate.entry_572 line 1185
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:139 (same declaration text).
def OAI.SnakyCertificate.entry_573 line 1187
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:141 (same declaration text).
def OAI.SnakyCertificate.entry_574 line 1189
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:143 (same declaration text).
def OAI.SnakyCertificate.entry_575 line 1191
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:145 (same declaration text).
def OAI.SnakyCertificate.entry_576 line 1193
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:147 (same declaration text).
def OAI.SnakyCertificate.entry_577 line 1195
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:149 (same declaration text).
def OAI.SnakyCertificate.entry_578 line 1197
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:151 (same declaration text).
def OAI.SnakyCertificate.entry_579 line 1199
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:153 (same declaration text).
def OAI.SnakyCertificate.entry_580 line 1201
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:155 (same declaration text).
def OAI.SnakyCertificate.entry_581 line 1203
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:157 (same declaration text).
def OAI.SnakyCertificate.entry_582 line 1205
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:159 (same declaration text).
def OAI.SnakyCertificate.entry_583 line 1207
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:161 (same declaration text).
def OAI.SnakyCertificate.entry_584 line 1209
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:163 (same declaration text).
def OAI.SnakyCertificate.entry_585 line 1211
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:165 (same declaration text).
def OAI.SnakyCertificate.entry_586 line 1213
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:167 (same declaration text).
def OAI.SnakyCertificate.entry_587 line 1215
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:169 (same declaration text).
def OAI.SnakyCertificate.entry_588 line 1217
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:171 (same declaration text).
def OAI.SnakyCertificate.entry_589 line 1219
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:173 (same declaration text).
def OAI.SnakyCertificate.entry_590 line 1221
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:175 (same declaration text).
def OAI.SnakyCertificate.entry_591 line 1223
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:177 (same declaration text).
def OAI.SnakyCertificate.entry_592 line 1225
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:179 (same declaration text).
def OAI.SnakyCertificate.entry_593 line 1227
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:181 (same declaration text).
def OAI.SnakyCertificate.entry_594 line 1229
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:183 (same declaration text).
def OAI.SnakyCertificate.entry_595 line 1231
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:185 (same declaration text).
def OAI.SnakyCertificate.entry_596 line 1233
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:187 (same declaration text).
def OAI.SnakyCertificate.entry_597 line 1235
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:189 (same declaration text).
def OAI.SnakyCertificate.entry_598 line 1237
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:191 (same declaration text).
def OAI.SnakyCertificate.entry_599 line 1239
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:193 (same declaration text).
def OAI.SnakyCertificate.entry_600 line 1241
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:195 (same declaration text).
def OAI.SnakyCertificate.entry_601 line 1243
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:197 (same declaration text).
def OAI.SnakyCertificate.entry_602 line 1245
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:199 (same declaration text).
def OAI.SnakyCertificate.entry_603 line 1247
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:201 (same declaration text).
def OAI.SnakyCertificate.entry_604 line 1249
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:203 (same declaration text).
def OAI.SnakyCertificate.entry_605 line 1251
Also declared: OAI/Combinatorics/SnakyCertificate/Entries05.lean:205 (same declaration text).
def OAI.SnakyCertificate.entry_606 line 1253
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:7 (same declaration text).
def OAI.SnakyCertificate.entry_607 line 1255
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:9 (same declaration text).
def OAI.SnakyCertificate.entry_608 line 1257
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:11 (same declaration text).
def OAI.SnakyCertificate.entry_609 line 1259
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:13 (same declaration text).
def OAI.SnakyCertificate.entry_610 line 1261
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:15 (same declaration text).
def OAI.SnakyCertificate.entry_611 line 1263
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:17 (same declaration text).
def OAI.SnakyCertificate.entry_612 line 1265
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:19 (same declaration text).
def OAI.SnakyCertificate.entry_613 line 1267
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:21 (same declaration text).
def OAI.SnakyCertificate.entry_614 line 1269
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:23 (same declaration text).
def OAI.SnakyCertificate.entry_615 line 1271
Also declared: OAI/Combinatorics/SnakyCertificate/Entries06.lean:25 (same declaration text).
def OAI.SnakyCertificate.tableChunk_0 line 1273
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:13 (same declaration text).
def OAI.SnakyCertificate.tableChunk_1 line 1275
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:15 (same declaration text).
def OAI.SnakyCertificate.tableChunk_2 line 1277
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:17 (same declaration text).
def OAI.SnakyCertificate.tableChunk_3 line 1279
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:19 (same declaration text).
def OAI.SnakyCertificate.tableChunk_4 line 1281
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:21 (same declaration text).
def OAI.SnakyCertificate.tableChunk_5 line 1283
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:23 (same declaration text).
def OAI.SnakyCertificate.tableChunk_6 line 1285
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:25 (same declaration text).
def OAI.SnakyCertificate.tableChunk_7 line 1287
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:27 (same declaration text).
def OAI.SnakyCertificate.tableChunk_8 line 1289
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:29 (same declaration text).
def OAI.SnakyCertificate.tableChunk_9 line 1291
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:31 (same declaration text).
def OAI.SnakyCertificate.tableChunk_10 line 1293
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:33 (same declaration text).
def OAI.SnakyCertificate.tableChunk_11 line 1295
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:35 (same declaration text).
def OAI.SnakyCertificate.tableChunk_12 line 1297
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:37 (same declaration text).
def OAI.SnakyCertificate.tableChunk_13 line 1299
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:39 (same declaration text).
def OAI.SnakyCertificate.tableChunk_14 line 1301
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:41 (same declaration text).
def OAI.SnakyCertificate.tableChunk_15 line 1303
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:43 (same declaration text).
def OAI.SnakyCertificate.tableChunk_16 line 1305
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:45 (same declaration text).
def OAI.SnakyCertificate.tableChunk_17 line 1307
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:47 (same declaration text).
def OAI.SnakyCertificate.tableChunk_18 line 1309
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:49 (same declaration text).
def OAI.SnakyCertificate.tableChunk_19 line 1311
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:51 (same declaration text).
def OAI.SnakyCertificate.tableChunk_20 line 1313
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:53 (same declaration text).
def OAI.SnakyCertificate.tableChunk_21 line 1315
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:55 (same declaration text).
def OAI.SnakyCertificate.tableChunk_22 line 1317
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:57 (same declaration text).
def OAI.SnakyCertificate.tableChunk_23 line 1319
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:59 (same declaration text).
def OAI.SnakyCertificate.tableChunk_24 line 1321
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:61 (same declaration text).
def OAI.SnakyCertificate.tableChunk_25 line 1323
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:63 (same declaration text).
def OAI.SnakyCertificate.tableChunk_26 line 1325
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:65 (same declaration text).
def OAI.SnakyCertificate.tableChunk_27 line 1327
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:67 (same declaration text).
def OAI.SnakyCertificate.tableChunk_28 line 1329
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:69 (same declaration text).
def OAI.SnakyCertificate.tableChunk_29 line 1331
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:71 (same declaration text).
def OAI.SnakyCertificate.tableChunk_30 line 1333
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:73 (same declaration text).
def OAI.SnakyCertificate.table line 1335
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:75 (same declaration text).
def OAI.SnakyCertificate.entryAt line 1337
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:77 (same declaration text).
def OAI.SnakyCertificate.TableValid line 1339
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:79 (same declaration text).
def OAI.SnakyCertificate.placementCount line 1344
Also declared: OAI/Combinatorics/SnakyCertificate/Table.lean:84 (same declaration text).
structure OAI.SnakyCertificate.RowData line 1346
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:7 (same declaration text).
def OAI.SnakyCertificate.emptyRow line 1352
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:13 (same declaration text).
def OAI.SnakyCertificate.baseRow line 1354
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:15 (same declaration text).
def OAI.SnakyCertificate.placeRow line 1356
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:17 (same declaration text).
def OAI.SnakyCertificate.unionA line 1360
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:21 (same declaration text).
def OAI.SnakyCertificate.unionH line 1362
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:23 (same declaration text).
def OAI.SnakyCertificate.commonH line 1364
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:25 (same declaration text).
def OAI.SnakyCertificate.forkRow line 1369
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:30 (same declaration text).
def OAI.SnakyCertificate.rowAt line 1373
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:34 (same declaration text).
def OAI.SnakyCertificate.Output line 1379
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:40 (same declaration text).
def OAI.SnakyCertificate.AllRows line 1383
Also declared: OAI/Combinatorics/SnakyCertificate/Rows.lean:44 (same declaration text).
theorem OAI.SnakyCertificate.certificate_correct Challenge statement: Reconstruction of the 35-move Snaky certificate sorry line 1387
L4DEL explanation
This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.
1. The linked formalization note covers 3 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
2. The repository's comparator configuration selects OAI.Combinatorics.SnakyCertificate.Main as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Combinatorics/SnakyCertificate/Main.lean:50 (same statement text; different proof or body). Qualify references as OAI.SnakyCertificate.certificate_correct@path.
```
theorem certificate_correct :
    TableValid ∧ placementCount = 1837 ∧
    Output 557 (-1, 0) 118 19 {p | p.1 ≤ -3 ∧ p.2 ≤ -2} ∧
    Output 595 (-1, 0) 222 27 {p | p.1 = -2 ∧ p.2 ≤ -2} ∧
    Output 603 (-1, 0) 275 27 {p | p.1 ≤ -3 ∧ p.2 = 0} ∧
    Output 615 (1, 0) 686 34 {(1, -1)} ∧
    AllRows := by
…
```
Mentions: OAI.SnakyCertificate.TableValid, OAI.SnakyCertificate.placementCount, OAI.SnakyCertificate.Output, OAI.SnakyCertificate.AllRows