openpr_I_v3_1.txt

====================================================================================================
CASE I  PR #31425  (open-pr, v3.1 prompt)
file: Mathlib/Topology/Defs/Basic.lean  line: 207.0
reviewer: @eric-wieser  on 2025-11-09T11:31:11Z
advice_kind: needs explanatory comment
prompt_tokens: 5815  completion_tokens: 2865
HUMAN reviewer (ground truth):
  > This line would probably benefit from a comment explaining why, and for the binary one
====================================================================================================

[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 #31425 (file: Mathlib/Topology/Defs/Basic.lean):
```
@@ -195,6 +195,47 @@ scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t
 scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "]" =>
   @Continuous _ _ t₁ t₂
 
+namespace TopologicalSpace
+open Topology Lean Meta PrettyPrinter.Delaborator SubExpr
+
+/-- Delaborate unary notation referring to non-standard topologies. -/
+def delabUnary (mkStx : Term → DelabM Term) : Delab :=
+  withOverApp 2 <| whenPPOption Lean.getPPNotation do
+    let α ← withNaryArg 0 getExpr
+    let .some synthInst ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[α]) | failure
+    let inst ← withNaryArg 1 getExpr
+    if ← Meta.isDefEq inst synthInst then failure
```

RETRIEVED CANDIDATES (top-20 by hunk-embedding similarity, sorted by sim desc):

--- candidate 1 (sim=0.820, past_pr=#35907, file=Mathlib/Topology/Defs/Basic.lean) ---
PAST HUNK:
```
@@ -198,6 +199,68 @@ scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t
... [42 lines above hidden]
+@[app_delab closure] meta def delabClosureOf : Delab :=
+  whenNotPPOption getPPExplicit <|
+  whenPPOption getPPNotation <|
+  withOverApp 2 do
+    let #[_, t] := (← getExpr).getAppArgs | failure
+    if ← isCanonicalTopologyInst t then
+      failure
+    `(closure[$(← withNaryArg 1 delab)])
+
+/--
+Delaborate `@Continuous _ _ t₁ t₂` as `Continuous[t₁, t₂]`
+when either topology is noncanonical.
+-/
```
PAST COMMENT (from reviewer):
I think we should improve this so that it's smart about the situation when *one* of the topologies is canonical, but not both. This should delaborate as `Continuous[_, t₂]` when `t₁` is canonical but `t₂` is not, and as `Continuous[t₁, _]` when `t₂` is canonical but `t₁` is not. Note that *elaboration* of these expressions works.

--- candidate 2 (sim=0.815, past_pr=#35907, file=Mathlib/Topology/Defs/Basic.lean) ---
PAST HUNK:
```
@@ -198,6 +199,68 @@ scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t
... [49 lines above hidden]
+    `(closure[$(← withNaryArg 1 delab)])
+
+/--
+Delaborate `@Continuous _ _ t₁ t₂` as `Continuous[t₁, t₂]`
+when either topology is noncanonical.
+-/
+@[app_delab Continuous] meta def delabContinuousOf : Delab :=
+  whenNotPPOption getPPExplicit <|
+  whenPPOption getPPNotation <|
+  withOverApp 4 do
+    let #[_, _, t₁, t₂] := (← getExpr).getAppArgs | failure
+    if (← isCanonicalTopologyInst t₁) && (← isCanonicalTopologyInst t₂) then
+      failure
```
PAST COMMENT (from reviewer):
In `delabContinuousOf`, both `isCanonicalTopologyInst` checks are executed unconditionally because the monadic binds happen before `&&` is evaluated. If the intent is to skip the second instance check when the first is already noncanonical (since you only `failure` when *both* are canonical), restructure this to short-circuit to avoid unnecessary typeclass search during pretty-printing.
```suggestion
    let c₁ ← isCanonicalTopologyInst t₁
    if c₁ then
      let c₂ ← isCanonicalTopologyInst t₂
      if c₂ then
        failure
```

--- candidate 3 (sim=0.736, past_pr=#10110, file=Mathlib/Topology/Basic.lean) ---
PAST HUNK:
```
@@ -1627,7 +1627,10 @@ scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "
 
 variable {f : X → Y} {s : Set X} {x : X} {y : Y}
```
PAST COMMENT (from reviewer):
Maybe this line should now go below `continuous_def`?

--- candidate 4 (sim=0.699, past_pr=#10648, file=Mathlib/Topology/Defs/Basic.lean) ---
PAST HUNK:
```
@@ -166,3 +166,11 @@ scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t
 /-- Notation for `Continuous` with respect to a non-standard topologies. -/
 scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "]" =>
   @Continuous _ _ t₁ t₂
+
+/-- The property `BaireSpace α` means that the topological space `α` has the Baire property:
+any countable intersection of open dense subsets is dense.
+Formulated here when the source space is ℕ (and subsumed below by `dense_iInter_of_isOpen` working
```
PAST COMMENT (from reviewer):
Not "below" anymore

--- candidate 5 (sim=0.698, past_pr=#22048, file=Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean) ---
PAST HUNK:
```
@@ -228,50 +228,101 @@ elab_rules : term
 
 end deprecated
 
-open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr
+open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr Qq
```
PAST COMMENT (from reviewer):
I think this is also unused?

--- candidate 6 (sim=0.679, past_pr=#8056, file=Mathlib/Topology/Basic.lean) ---
PAST HUNK:
```
@@ -848,7 +848,7 @@ scoped[Topology] notation "𝓝" => nhds
 scoped[Topology] notation "𝓝[" s "] " x:100 => nhdsWithin x s
 
 /-- Notation for the filter of punctured neighborhoods of a point. -/
-scoped[Topology] notation "𝓝[≠] " x:100 => nhdsWithin x {x}ᶜ
+scoped[Topology] notation "𝓝[≠] " x:100 => nhdsWithin x (@singleton _ (Set _) instSingletonSet x)ᶜ
```
PAST COMMENT (from reviewer):
I've tried a few things and I can't get it to work like that.

I did find this workaround though:
```
set_option quotPrecheck false in
/-- Notation for the filter of punctured neighborhoods of a point. -/
scoped[Topology] notation "𝓝[≠] " x:100 => letI z := x; nhdsWithin z ({z}ᶜ)
```
I'm not sure what's going on or why this helps at this point.

--- candidate 7 (sim=0.679, past_pr=#8056, file=Mathlib/Topology/Basic.lean) ---
PAST HUNK:
```
@@ -848,7 +848,7 @@ scoped[Topology] notation "𝓝" => nhds
 scoped[Topology] notation "𝓝[" s "] " x:100 => nhdsWithin x s
 
 /-- Notation for the filter of punctured neighborhoods of a point. -/
-scoped[Topology] notation "𝓝[≠] " x:100 => nhdsWithin x {x}ᶜ
+scoped[Topology] notation "𝓝[≠] " x:100 => nhdsWithin x (@singleton _ (Set _) instSingletonSet x)ᶜ
```
PAST COMMENT (from reviewer):
I'm seeing `nhdsWithin x ({x} : Set _)ᶜ` in the git history -- Eric's suggesting `nhdsWithin x ({x}ᶜ : Set _)`. I'll check if it makes a difference.

--- candidate 8 (sim=0.674, past_pr=#7633, file=Mathlib/Util/PiNotation.lean) ---
PAST HUNK:
```
@@ -59,3 +80,50 @@ def delabPi : Delab := whenPPOption Lean.getPPNotation do
   | _ => pure stx
 
 end PiNotation
+
+section existential
+open Lean Parser Term PrettyPrinter Delaborator
+
+/-- Delaborator for existential quantifier, including extended binders. -/
```
PAST COMMENT (from reviewer):
```suggestion
/-- Delaborator for existential quantifier, including extended binders. -/
-- TODO: reduce the duplication in this code
```

--- candidate 9 (sim=0.674, past_pr=#2145, file=test/Continuity.lean) ---
PAST HUNK:
```
@@ -0,0 +1,22 @@
+import Mathlib.Topology.Basic
```
PAST COMMENT (from reviewer):
I think it's worth a note in a comment that this is not a port of https://github.com/leanprover-community/mathlib/blob/master/test/continuity.lean (yet)

--- candidate 10 (sim=0.673, past_pr=#7964, file=Mathlib/Util/Delaborators.lean) ---
PAST HUNK:
```
@@ -122,9 +132,34 @@ def exists_delab : Delab := whenPPOption Lean.getPPNotation do
... [20 lines above hidden]
-  -- Merging
   match stx with
   | `(∃ $group:bracketedExplicitBinders, ∃ $groups*, $body) => `(∃ $group $groups*, $body)
+  | `(∃ $b:binderIdent, ∃ $[$bs:binderIdent]*, $body) => `(∃ $b:binderIdent $[$bs]*, $body)
   | _ => pure stx
 end existential
+
+open Lean Lean.PrettyPrinter.Delaborator
+
+/-- Delaborator for `∉`. -/
+@[delab app.Not] def delab_not_in := whenPPOption Lean.getPPNotation do
+  let #[f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.getAppFn matches .const `Membership.mem _ do failure
```
PAST COMMENT (from reviewer):
There's `Expr.isAppOf` for this, but we should also check the arity since we can't be sure that expressions being pretty printed are well-formed.
```suggestion
  guard <| f.isAppOfArity ``Membership.mem 5
```

--- candidate 11 (sim=0.659, past_pr=#16946, file=Mathlib/Algebra/BigOperators/Expect.lean) ---
PAST HUNK:
```
@@ -98,7 +101,7 @@ to show the domain type when the expect is over `Finset.univ`. -/
         `(bigOpBinder| $(.mk i):ident)
     `(𝔼 $binder:bigOpBinder, $body)
   else
-    let ss ← withNaryArg 3 <| delab
+    let ss ← withNaryArg 4 <| delab
```
PAST COMMENT (from reviewer):
What's this change doing? Or more specifically, how do I know there won't be n more PRs incrementing the number again :D

--- candidate 12 (sim=0.659, past_pr=#12182, file=Mathlib/Topology/LocallyConstant/Basic.lean) ---
PAST HUNK:
```
@@ -458,7 +458,7 @@ variable [TopologicalSpace Y]
 This definition only makes sense if `f` is continuous,
```
PAST COMMENT (from reviewer):
This is wrong too now, right? Can you reference the refactor PR in the PR description?

--- candidate 13 (sim=0.659, past_pr=#29728, file=Mathlib/Topology/Sets/Closeds.lean) ---
PAST HUNK:
```
@@ -20,6 +22,7 @@ For a topological space `α`,
 
 
 open Order OrderDual Set
+open scoped Topology
```
PAST COMMENT (from reviewer):
I think you can just `open Topology` and remove the `Topology.` below.

--- candidate 14 (sim=0.659, past_pr=#33070, file=Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean) ---
PAST HUNK:
```
@@ -265,7 +265,7 @@ to show the domain type when the product is over `Finset.univ`. -/
   whenPPOption getPPNotation <| withOverApp 5 do
   let #[_, _, _, _, f] := (← getExpr).getAppArgs | failure
   guard f.isLambda
-  let ppDomain ← getPPOption getPPFunBinderTypes
+  let ppDomain ← withAppArg do return getPPFunBinderTypes (← getOptionsAtCurrPos)
```
PAST COMMENT (from reviewer):
I think this is the same as
```suggestion
  let ppDomain ← withAppArg <| getPPOption getPPFunBinderTypes
```

--- candidate 15 (sim=0.656, past_pr=#21205, file=Mathlib/Topology/ContinuousMap/CompactlySupported.lean) ---
PAST HUNK:
```
@@ -46,7 +46,7 @@ scoped[CompactlySupported] notation (priority := 2000)
 @[inherit_doc]
 scoped[CompactlySupported] notation α " →C_c " β => CompactlySupportedContinuousMap α β
 
-open CompactlySupported
+open CompactlySupported Classical
```
PAST COMMENT (from reviewer):
```suggestion
open CompactlySupported
```

--- candidate 16 (sim=0.655, past_pr=#17777, file=Mathlib/Analysis/Calculus/Deriv/Slope.lean) ---
PAST HUNK:
```
@@ -25,23 +25,18 @@ derivative, slope
 -/
 
 
-universe u v w
+universe u v
 
-noncomputable section
-
-open Topology Filter TopologicalSpace
-open Filter Set
+open Topology Filter TopologicalSpace Set
```
PAST COMMENT (from reviewer):
I'd be careful with those: I believe this is a porting artefact, where one of these two lines should be replaced by `open scoped` instead. Can you see which of the `open`s can be downgraded this way, please?

--- candidate 17 (sim=0.653, past_pr=#8613, file=Mathlib/Topology/Category/Profinite/Basic.lean) ---
PAST HUNK:
```
@@ -242,20 +240,31 @@ end DiscreteTopology
 
 end Profinite
 
+/--
+Universe inequalities in Mathlib 3 are expressed through use of `max u v`. Unfortunately,
```
PAST COMMENT (from reviewer):
```suggestion
Many definitions involving universe inequalities in Mathlib are expressed through use of `max u v`. Unfortunately,
```

--- candidate 18 (sim=0.651, past_pr=#31667, file=Mathlib/Analysis/Normed/Lp/WithLp.lean) ---
PAST HUNK:
```
@@ -61,7 +59,7 @@ def WithLp.delabToLp : Delab := delabApp
 
 end Notation
 
-variable (p : ℝ≥0∞) (K : Type uK) (K' : Type uK') (V : Type uV)
+variable (p : ℝ≥0∞) (K K' K'' V V' V'' : Type*)
```
PAST COMMENT (from reviewer):
The issue is that you declared them as explicit in the beginning. Just declare them as implicit to start, and then there's no need to change it.

--- candidate 19 (sim=0.649, past_pr=#1843, file=Mathlib/Topology/Basic.lean) ---
PAST HUNK:
```
@@ -1569,6 +1569,11 @@ structure Continuous (f : α → β) : Prop where
   is_open_preimage : ∀ s, IsOpen s → IsOpen (f ⁻¹' s)
 #align continuous Continuous
 
+set_option quotPrecheck false in
+/-- Notation for `Continuous` with respect to a non-standard topologies. -/
```
PAST COMMENT (from reviewer):
```suggestion
/-- Notation for `Continuous` with respect to non-standard topologies. -/
```

--- candidate 20 (sim=0.648, past_pr=#30606, file=Mathlib/Topology/Continuous.lean) ---
PAST HUNK:
```
@@ -324,18 +324,18 @@ in different definitionally equal ways (omitting some typing information)
 * `Continuous ↿(+)`. (`↿` is notation for recursively uncurrying a function)
 
 However, lemmas with this conclusion are not nice to use in practice because
-1. They confuse the elaborator. The following two examples fail, because of limitations in the
+1. They confuse the elaborator. The following examples fails, because of limitations in the
```
PAST COMMENT (from reviewer):
```suggestion
1. They confuse the elaborator. The following example fails, because of limitations in the
```


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"
  ],
  "summary": "No past comments directly apply; closest observations concern potentially unused or suboptimal `open`s around Topology-related delaborators.",
  "confidence": "low",
  "strong_matches": [],
  "weak_observations": [
    {
      "observation": "Consider removing or scoping unnecessary `open`s (e.g., `open Topology`) if they are not used in this namespace.",
      "axis": "style-syntax",
      "supporting_past_prs": [
        22048,
        29728
      ]
    }
  ]
}