-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathopenpr_J_v3_1.txt
More file actions
507 lines (461 loc) · 22.1 KB
/
Copy pathopenpr_J_v3_1.txt
File metadata and controls
507 lines (461 loc) · 22.1 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
====================================================================================================
CASE J PR #36698 (open-pr, v3.1 prompt)
file: Mathlib/Combinatorics/Enumerative/LatinSquare.lean line: 257.0
reviewer: @vlad902 on 2026-03-17T07:34:52Z
advice_kind: refactor (suggestion block)
prompt_tokens: 5980 completion_tokens: 1783
HUMAN reviewer (ground truth):
> ```suggestion
> once_per_row i' :=
> h.bijective.comp (A.once_per_row (f.symm i') |>.comp g.symm.bijective)
> ```
====================================================================================================
[SYSTEM]
----------------------------------------------------------------------------------------------------
You are an expert reviewer for the Lean 4 / mathlib4 mathematical library. Given a NEW code hunk from an open pull request and a set of historically retrieved (past_hunk, past_comment) pairs, your job is to identify which past reviewer feedback would also apply to the new hunk.
Two failure modes are equally bad and you must avoid BOTH:
(X) "axis-miss" false positive: a past comment and the new code look similar on the surface, but the past reviewer's concern is not present in the new hunk. (Example: past comment is about `ppSpace` formatting, new hunk's actual problem is "this whole function shouldn't return a string".)
(Y) "over-refusal" false negative: a candidate IS genuinely applicable, but you refuse because its concern axis didn't appear in your initial inventory. (Example: you forgot to list `refactor-simplify` for a proof hunk, then declined a candidate that correctly suggests using a higher-level lemma.)
A correct silent output is more valuable than a confident wrong-axis answer, but losing a clearly-applicable candidate is also a real cost.
Read carefully before producing JSON. Follow the four steps below in order.
STEP 1 — STRUCTURAL + SEMANTIC READING OF THE NEW HUNK.
1a. Parse the code shape: tactic-mode vs term-mode, declaration kind (`def` / `theorem` / `lemma` / `instance` / `class` / `structure` / `abbrev` / `syntax` / `notation`), attributes (`@[simp]`, `@[to_additive]`, `@[deprecated]`, `@[ext]`, `@[fun_prop]`, `@[reassoc]`, …), universe parameters, implicit/explicit binders, docstring style, proof tactics used.
1b. Inventory what *could* be criticized about THIS specific hunk. Pick as many as apply from this list of "concern axes":
- correctness-bug (code doesn't typecheck / is logically wrong)
- naming (lemma/def name doesn't follow conventions)
- docstring (missing, unclear, typo, wrong phrasing)
- attribute (missing/wrong `@[simp]` / `@[to_additive]` …)
- style-syntax (`fun x ↦` vs `fun x =>`, `by use _; exact _` vs `⟨_, _⟩`, whitespace/`ppSpace`, notation preference)
- proof-golf (the proof tactics could be shorter/nicer)
- refactor-simplify (same statement provable with less machinery, e.g. use a dedicated higher-level lemma instead of manual rewriting)
- generalize-signature (hypotheses too strong; remove/weaken a typeclass)
- design-smell-architectural (this API shape is wrong; returning a string, unnecessary instance, redundant definition, etc.)
- imports-module (superfluous imports, module structure)
- namespace-organization (`_root_`, namespace boundary, file placement)
- automation-tactic (should use / should teach `aesop_cat`, `gcongr`, `positivity`, etc.)
- instance-diamond (this instance creates an ambiguity / defeq diamond with another)
- unify-with-existing (a similar definition/lemma already exists)
- junk-value (docstring should note behavior at the "undefined" input; handled via `0`/`⊥`/`⊤`)
1c. DEFAULT-INCLUDE RULE. For ANY non-trivial proof or definition hunk (i.e. not a pure-imports/notation/file-header hunk), you MUST include the following axes in your plausible list unless the hunk is so trivial that they cannot apply: `refactor-simplify`, `proof-golf`, `docstring`, `naming`. These are the most common reviewer concerns; gating them out by omission caused real misses in past evaluation. Adding them is cheap; they only trigger a promotion if a candidate also matches.
1d. List the concerns that PLAUSIBLY apply to the new hunk (including the defaults from 1c). If none from outside 1c are obviously present, that is fine — the defaults still cover proof/definition hunks.
STEP 2 — PER-CANDIDATE CONCERN CLASSIFICATION.
For EACH candidate, identify which concern axis (from the same list) the past reviewer's comment was about. Read the past comment carefully: the reviewer's *words* (not the past code) tell you the concern axis. If a past comment ships a `suggestion` code block, that block is evidence for what the reviewer wanted changed — but the axis of concern comes from the prose around it. Ignore candidates whose past comment is pure bikeshed or where you cannot identify a clear concern.
STEP 3 — AXIS MATCH + APPLICABILITY CHECK.
A candidate is eligible for `strong_matches` ONLY if BOTH:
(a) Its axis (from step 2) is among the new hunk's plausible concerns (from step 1d), OR you can clearly justify (in `applies_because`) why this axis IS present in the new hunk after all — in which case ADD that axis to `new_hunk_plausible_concerns` in your output. Late additions are allowed but should be the exception, not the rule.
(b) You can write a concrete adaptation that a Lean/mathlib reviewer would plausibly post on the new hunk *today*, given what is visible in the hunk.
Before promoting, write — in the JSON output, per match — a `why_might_not_apply` field giving the strongest counter-argument against promotion (one short sentence).
DEMOTION RULE (this is the #1 axis-miss-prevention lever):
If your counter-argument names a SPECIFIC PROPERTY of the new hunk that would make the past advice not apply or already-followed — e.g. "the new code already uses term-mode", "the lemma is already named correctly", "the import is actually used at line X", "the new code does not declare an instance, so the diamond risk does not apply" — then DEMOTE to `weak_observations` instead of promoting.
Only PROMOTE if the counter-argument is generic doubt that does NOT identify a specific reason the new hunk evades the past advice — e.g. "this is partly stylistic preference", "the user may have intended this", "I cannot verify without seeing more context". Generic doubt does not block promotion; specific evasion does.
Cross-candidate synthesis is allowed: if candidate X establishes that an identifier in the new hunk is a `class`, and candidate Y shows the preferred term-mode `instance := ⟨...⟩` template, they jointly support a promotion. List both in `supporting_past_prs` and still produce one `why_might_not_apply`.
STEP 4 — CONFIDENCE AND OUTPUT.
Confidence scale:
- "high" — ≥1 strong match survives step 3 AND the adaptation is a near-verbatim application of a past comment; the counter-argument is generic.
- "medium" — ≥1 strong match survives step 3 BUT needs adaptation or synthesis; counter-argument is generic doubt rather than specific evasion.
- "low" — no candidate survives step 3; only stylistic patterns worth mentioning as `weak_observations`.
- "none" — retrieved pool's concerns don't match anything plausible about the new hunk; state this and stop.
Output JSON ONLY, matching this exact schema:
{
"new_hunk_plausible_concerns": [<axis labels from Step 1d, plus any added in Step 3a>],
"summary": "<one sentence describing what we found>",
"confidence": "high"|"medium"|"low"|"none",
"strong_matches": [
{
"past_pr": <int>,
"past_file": "<string>",
"past_concern_axis": "<axis label from the list>",
"past_comment_excerpt": "<verbatim short quote from the past comment OR the relevant snippet from its suggestion block>",
"applies_because": "<one or two sentences linking past code/comment to the new hunk's structure AND explaining why the concern axis matches>",
"suggested_adaptation": "<one sentence on what the reviewer might say on the new hunk>",
"why_might_not_apply": "<one short sentence — strongest counter-argument against this promotion>",
"supporting_past_prs": [<int>, ...]
}
],
"weak_observations": [
{
"observation": "<short string>",
"axis": "<axis label>",
"supporting_past_prs": [<int>, ...]
}
]
}
Quote short — under 40 words per excerpt. Do not invent axis labels outside the list.
[USER]
----------------------------------------------------------------------------------------------------
NEW HUNK from open PR #36698 (file: Mathlib/Combinatorics/Enumerative/LatinSquare.lean):
```
@@ -0,0 +1,933 @@
... [217 lines above hidden]
+ exact Group.mulLeft_bijective (G := G),
+ once_per_column := by
+ simp only [OncePerColumn, Matrix.col]
+ exact Group.mulRight_bijective (G := G)
+ }
+
+
+@[expose] public section Equivalence
+
+/-- Given relabeling maps for the rows, columns, and symbols,
+ produce the relabeled Latin rectangle. -/
+@[reducible]
+def renameLatinRectangle
+ (f : m ≃ m')
+ (g : n ≃ n')
+ (h : α ≃ β)
+ (A : LatinRectangle m n α) :
+ LatinRectangle m' n' β := {
+ M := fun i' j' ↦ h (A.M (f.symm i') (g.symm j')),
+ exactly_n_symbols := by
+ have g' : Fintype.card n = Fintype.card n' := Fintype.card_congr g
+ have h' : Fintype.card α = Fintype.card β := Fintype.card_congr h
+ have k' := A.exactly_n_symbols
+ omega,
+ once_per_row := by
+ simp only [OncePerRow, Matrix.row]
+ have h' := A.once_per_row
+ simp only [OncePerRow, Matrix.row] at h'
+ intro i'
+ specialize h' (f.symm i') --(h.symm b')
+ have h_comp :
+ (fun j' ↦ h (LatinRectangle.M (f.symm i') (g.symm j'))) =
+ h ∘ (LatinRectangle.M (f.symm i')) ∘ g.symm := by
+ ext
+ simp
+ rw [h_comp]
+ apply Function.Bijective.comp
+ · exact Equiv.bijective h
+ · apply Function.Bijective.comp
+ · exact h'
+ · exact Equiv.bijective g.symm,
```
RETRIEVED CANDIDATES (top-20 by hunk-embedding similarity, sorted by sim desc):
--- candidate 1 (sim=0.662, past_pr=#10834, file=NatNumberCategories) ---
PAST HUNK:
```
@@ -0,0 +1,416 @@
+/-
+Copyright (c) 2024 Colin Jones. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Colin Jones
+-/
+import Mathlib
```
PAST COMMENT (from reviewer):
This file is supposed to be part of Mathlib, it can't import mathlib without creating an infinite loop. Just import the files you need:
```suggestion
import Mathlib.Algebra.GeomSum
import Mathlib.NumberTheory.Divisors
import Mathlib.Tactic.NormNum.Prime
import Mathlib.Analysis.Normed.Field.Basic
```
--- candidate 2 (sim=0.648, past_pr=#2960, file=Mathlib/Data/Matrix/Basic.lean) ---
PAST HUNK:
```
@@ -0,0 +1,2829 @@
... [2476 lines above hidden]
+ invFun M := M.submatrix eₘ eₙ
+ left_inv M := by simp
+ right_inv M := by simp
+#align matrix.reindex Matrix.reindex
+
+@[simp]
+theorem reindex_apply (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) :
+ reindex eₘ eₙ M = M.submatrix eₘ.symm eₙ.symm :=
+ rfl
+#align matrix.reindex_apply Matrix.reindex_apply
+
+-- @[simp] -- Porting note: simp can prove this
+theorem reindex_refl_refl (A : Matrix m n α) : reindex (Equiv.refl _) (Equiv.refl _) A = A :=
```
PAST COMMENT (from reviewer):
Whoops, this one was probably meant to say something else. That's out of scope here though.
--- candidate 3 (sim=0.648, past_pr=#28708, file=Mathlib/Data/Matrix/Stochastic.lean) ---
PAST HUNK:
```
@@ -0,0 +1,250 @@
+/-
+Copyright (c) 2025 Steven Herbert. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Steven Herbert
+-/
+
+import Mathlib.Data.Matrix.Basic
```
PAST COMMENT (from reviewer):
```suggestion
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Mul
```
--- candidate 4 (sim=0.642, past_pr=#1874, file=Mathlib/GroupTheory/Coset.lean) ---
PAST HUNK:
```
@@ -0,0 +1,891 @@
... [859 lines above hidden]
+
+end Subgroup
+
+namespace QuotientGroup
+
+variable [Group α]
+
+/-- If `s` is a subgroup of the group `α`, and `t` is a subset of `α ⧸ s`, then there is a
+(typically non-canonical) bijection between the preimage of `t` in `α` and the product `s × t`. -/
+@[to_additive "If `s` is a subgroup of the additive group `α`, and `t` is a subset of `α ⧸ s`, then
+ there is a (typically non-canonical) bijection between the preimage of `t` in `α` and the product
+ `s × t`."]
+noncomputable def preimageMkEquivSubgroupTimesSet (s : Subgroup α) (t : Set (α ⧸ s)) :
```
PAST COMMENT (from reviewer):
```suggestion
noncomputable def preimageMkEquivSubgroupProdSet (s : Subgroup α) (t : Set (α ⧸ s)) :
```
--- candidate 5 (sim=0.641, past_pr=#1874, file=Mathlib/GroupTheory/Coset.lean) ---
PAST HUNK:
```
@@ -0,0 +1,891 @@
... [876 lines above hidden]
+ leftRel_apply.mp (@Quotient.exact' _ (leftRel s) _ _ <| Quotient.out_eq' _)⟩,
+ ⟨QuotientGroup.mk a, a.2⟩⟩
+ invFun a :=
+ ⟨Quotient.out' a.2.1 * a.1.1,
+ show QuotientGroup.mk _ ∈ t by
+ rw [mk_mul_of_mem _ a.1.2, out_eq']
+ exact a.2.2⟩
+ left_inv := fun ⟨a, ha⟩ => Subtype.eq <| show _ * _ = a by simp
+ right_inv := fun ⟨⟨a, ha⟩, ⟨x, hx⟩⟩ => by ext <;> simp [ha]
+#align quotient_group.preimage_mk_equiv_subgroup_times_set
+ QuotientGroup.preimageMkEquivSubgroupTimesSet
+#align quotient_add_group.preimage_mk_equiv_add_subgroup_times_set
+ QuotientAddGroup.preimageMkEquivAddSubgroupTimesSet
```
PAST COMMENT (from reviewer):
```suggestion
#align quotient_group.preimage_mk_equiv_subgroup_times_set QuotientGroup.preimageMkEquivSubgroupProdSet
#align quotient_add_group.preimage_mk_equiv_add_subgroup_times_set QuotientAddGroup.preimageMkEquivAddSubgroupProdSet
```
--- candidate 6 (sim=0.640, past_pr=#21148, file=Mathlib/RingTheory/MatrixAlgebra.lean) ---
PAST HUNK:
```
@@ -4,23 +4,90 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison, Eric Wieser
-/
import Mathlib.Data.Matrix.Basis
+import Mathlib.Data.Matrix.Composition
```
PAST COMMENT (from reviewer):
maybe open a new file just to make the large import happy?
--- candidate 7 (sim=0.640, past_pr=#21148, file=Mathlib/RingTheory/MatrixAlgebra.lean) ---
PAST HUNK:
```
@@ -4,23 +4,90 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison, Eric Wieser
-/
import Mathlib.Data.Matrix.Basis
+import Mathlib.Data.Matrix.Composition
```
PAST COMMENT (from reviewer):
I wouldn't mind it so much if it was just this file and `PolynomialAlgebra`, but it does bump the imports of `Localization.Algebra` and its downstream files by quite a bit too. I wouldn't expect those to even know about matrices.
Maybe we should be flipping the import direction `MatrixAlgebra -> PolynomialAlgebra`?
--- candidate 8 (sim=0.637, past_pr=#6526, file=Mathlib/Algebra/Ring/UnitEquivs.lean) ---
PAST HUNK:
```
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2021 Johan Commelin. All rights reserved.
```
PAST COMMENT (from reviewer):
Is this a copy-paste error?
```suggestion
Copyright (c) 2023 Eric Rodriguez. All rights reserved.
```
Same remark for `Authors` field on line 4, though maybe this is co-authored?
--- candidate 9 (sim=0.636, past_pr=#28100, file=Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean) ---
PAST HUNK:
```
@@ -14,6 +15,79 @@ see `LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean`.
namespace Matrix
+open Matrix LinearMap
+
+variable {R n : Type*} [Fintype n]
```
PAST COMMENT (from reviewer):
```suggestion
variable {R V : Type*} [AddCommGroup V]
```
--- candidate 10 (sim=0.635, past_pr=#9428, file=Mathlib/AlgebraicTopology/SingularSet.lean) ---
PAST HUNK:
```
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2024 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Scott Morrison, Adam Topaz
```
PAST COMMENT (from reviewer):
Ah, I guess [we've argued this before](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Copyright.20header/near/280420005). I always take it to be the year the oldest definition/lemma of the file was created.
--- candidate 11 (sim=0.635, past_pr=#9428, file=Mathlib/AlgebraicTopology/SingularSet.lean) ---
PAST HUNK:
```
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2024 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Scott Morrison, Adam Topaz
```
PAST COMMENT (from reviewer):
Can you make sure the year is correct?
--- candidate 12 (sim=0.635, past_pr=#35467, file=Mathlib/Combinatorics/Quiver/Schreier.lean) ---
PAST HUNK:
```
@@ -0,0 +1,771 @@
... [5 lines above hidden]
+-/
+module
+
+public import Mathlib.Combinatorics.Quiver.Basic
+public import Mathlib.Combinatorics.Quiver.SingleObj
+public import Mathlib.Combinatorics.Quiver.Covering
+public import Mathlib.Combinatorics.Quiver.Symmetric
+public import Mathlib.Combinatorics.Quiver.ConnectedComponent
+public import Mathlib.GroupTheory.GroupAction.Quotient
+public import Mathlib.GroupTheory.QuotientGroup.Basic
+public import Mathlib.Algebra.Group.Subgroup.Basic
+public import Mathlib.GroupTheory.FreeGroup.Basic
+public import Mathlib.Tactic.Group
```
PAST COMMENT (from reviewer):
Can you use `#min_imports` at the bottom of the file and replace these with what it suggests?
(these aren't minimized, e.g. `Quiver.SingleObj` imports `Quiver.Symmetric`)
--- candidate 13 (sim=0.630, past_pr=#6205, file=Mathlib/Algebra/Order/LatticeGroup.lean) ---
PAST HUNK:
```
@@ -59,12 +61,10 @@ lattices.
lattice, ordered, group
-/
-
--- Needed for squares
-- Needed for squares
```
PAST COMMENT (from reviewer):
What does this comment mean?
--- candidate 14 (sim=0.629, past_pr=#7385, file=Mathlib/MeasureTheory/Measure/Trim.lean) ---
PAST HUNK:
```
@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
```
PAST COMMENT (from reviewer):
Is this correct? I thought we've had `trim` for much longer than 9 months
--- candidate 15 (sim=0.629, past_pr=#11667, file=Mathlib/Combinatorics/SimpleGraph/Matching.lean) ---
PAST HUNK:
```
@@ -36,45 +36,42 @@ one edge, and the edges of the subgraph represent the paired vertices.
* Tutte's Theorem
-* Hall's Marriage Theorem (see combinatorics.hall)
+* Hall's Marriage Theorem (see `Combinatorics.Hall.Basic`)
```
PAST COMMENT (from reviewer):
```suggestion
* Hall's Marriage Theorem (see Combinatorics.Hall.Basic)
```
I *think* this is the correct syntax for the linkifier to work
--- candidate 16 (sim=0.627, past_pr=#9511, file=Mathlib/Algebra/Ring/Ext.lean) ---
PAST HUNK:
```
@@ -0,0 +1,528 @@
+/-
+Copyright (c) 2024 Raghuram Sundararajan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Raghuram Sundararajan
+-/
+import Mathlib.Algebra.Ring.Defs
+import Mathlib.Algebra.Group.Ext
+-- import Mathlib
```
PAST COMMENT (from reviewer):
A commented-out line that is no longer needed can be safely deleted (we can always check the commits to get it back).
```suggestion
```
--- candidate 17 (sim=0.627, past_pr=#13401, file=Mathlib/GroupTheory/Congruence/BigOperators.lean) ---
PAST HUNK:
```
@@ -6,24 +6,42 @@ Authors: Amelia Livingston
import Mathlib.GroupTheory.Congruence.Basic
import Mathlib.Algebra.BigOperators.Group.Finset
+import Mathlib.Algebra.BigOperators.Group.Multiset
+import Mathlib.Algebra.BigOperators.Group.List
```
PAST COMMENT (from reviewer):
The first imports the other two
```suggestion
import Mathlib.Algebra.BigOperators.Group.Finset
```
--- candidate 18 (sim=0.627, past_pr=#14623, file=Mathlib/Combinatorics/SimpleGraph/Connectivity.lean) ---
PAST HUNK:
```
@@ -3,7 +3,10 @@ Copyright (c) 2021 Kyle Miller. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
+import Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Combinatorics.SimpleGraph.Subgraph
+import Mathlib.Data.Fintype.Card
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
```
PAST COMMENT (from reviewer):
That is quite some new imports in an already long file. Maybe put the new lemmas (and any already existing related lemmas) in a new file?
I also don't see how the new imports are actually used in the new lemmas?
--- candidate 19 (sim=0.626, past_pr=#30047, file=Mathlib/Combinatorics/SimpleGraph/EdgeLabelling.lean) ---
PAST HUNK:
```
@@ -0,0 +1,227 @@
+/-
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta, Olivia Röhrig
+-/
+import Mathlib.Combinatorics.SimpleGraph.Maps
+import Mathlib.Combinatorics.SimpleGraph.Finite
+import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Data.ZMod.Defs
```
PAST COMMENT (from reviewer):
I think we shouldn't need this import
--- candidate 20 (sim=0.626, past_pr=#30047, file=Mathlib/Combinatorics/SimpleGraph/EdgeLabelling.lean) ---
PAST HUNK:
```
@@ -0,0 +1,227 @@
+/-
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta, Olivia Röhrig
+-/
+import Mathlib.Combinatorics.SimpleGraph.Maps
+import Mathlib.Combinatorics.SimpleGraph.Finite
+import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Data.ZMod.Defs
```
PAST COMMENT (from reviewer):
(to be clear, I mean just the very last line - github doesn't let me select just one line to comment on!)
Decide which candidates' comments genuinely apply to the NEW hunk. If none, say so. Output JSON only.
[ASSISTANT]
----------------------------------------------------------------------------------------------------
{
"new_hunk_plausible_concerns": [
"refactor-simplify",
"proof-golf",
"docstring",
"naming",
"style-syntax",
"correctness-bug"
],
"summary": "None of the retrieved past review comments (mostly about imports, naming with Prod/Times, headers) clearly apply to this new definition/proof snippet.",
"confidence": "none",
"strong_matches": [],
"weak_observations": []
}