openpr_I_v3_gemini.txt

====================================================================================================
CASE I  PR #31425  (open-pr, v3 prompt, Gemini)
file: Mathlib/Topology/Defs/Basic.lean  line: 207.0
reviewer: @eric-wieser  on 2025-11-09T11:31:11Z
advice_kind: needs explanatory comment
model: gemini-2.5-flash  prompt_tokens: 5969  completion_tokens: 645
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.

Your single most important task is to AVOID "axis-miss" false positives: cases where a past comment and the new code LOOK similar on the surface, but the past reviewer was raising a different KIND of concern than anything the new hunk actually has. A correct silent output is far more valuable than a confident wrong-axis answer.

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)
     - 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`/`⊥`/`⊤`)
  List the concerns that PLAUSIBLY apply to the new hunk. If none are obviously present, say so — don't invent them.

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 1b).
    (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). If this counter-argument is actually compelling (e.g. "the new code does not have that pattern", "the new code *does* have an ext lemma, so this doesn't apply"), DO NOT promote; demote to `weak_observations` or drop.
  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 weak.
    - "medium" — ≥1 strong match survives step 3 BUT needs adaptation or synthesis; counter-argument is plausible but not decisive.
    - "low"    — no candidate survives step 3; only stylistic patterns worth mentioning as `weak_observations`.
    - "none"   — retrieved pool's axes don't match anything plausible about the new hunk; state this and stop.
  When in doubt between "medium" and "low" on a single uncertain candidate, prefer "low" and put that candidate in `weak_observations`. "Confident but wrong-axis" is the #1 failure we are trying to eliminate.

Output JSON ONLY, matching this exact schema:

{
  "new_hunk_plausible_concerns": [<one or more axis labels from Step 1b, or []>],
  "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. Do not promote a candidate whose axis is not in `new_hunk_plausible_concerns`.

[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": [
    "design-smell-architectural",
    "proof-golf",
    "style-syntax",
    "unify-with-existing",
    "correctness-bug"
  ],
  "summary": "The new delaborator's failure condition raises similar design concerns as previously discussed for topology delaborators, and general observations about `open` statements and monadic efficiency also apply.",
  "confidence": "medium",
  "strong_matches": [
    {
      "past_pr": 35907,
      "past_file": "Mathlib/Topology/Defs/Basic.lean",
      "past_concern_axis": "design-smell-architectural",
      "past_comment_excerpt": "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.",
      "applies_because": "The new `delabUnary`'s logic (`if ← Meta.isDefEq inst synthInst then failure`) employs an all-or-nothing `failure` when the explicit instance matches the synthesized canonical one. Past feedback on similar topology delaborators questioned this approach, suggesting more flexible delaboration even when canonical instances are involved, rather than simply failing.",
      "suggested_adaptation": "Consider if the `failure` condition for `delabUnary` should be more nuanced, perhaps allowing a different notation or a more permissive delaboration strategy, as was discussed for `delabContinuousOf`.",
      "why_might_not_apply": "The specific suggestion of partial delaboration (`Continuous[_, t₂]`) does not directly apply to a unary notation."
    }
  ],
  "weak_observations": [
    {
      "observation": "The `open Topology Lean Meta PrettyPrinter.Delaborator SubExpr` line could be reviewed to ensure all `open` statements are necessary and follow style conventions (e.g., `open scoped`).",
      "axis": "imports-module",
      "supporting_past_prs": [
        22048,
        29728,
        21205,
        17777
      ]
    },
    {
      "observation": "For delaborators involving expensive monadic computations like `trySynthInstance` and `isDefEq`, consider restructuring `if` statements for clarity and efficiency, especially if multiple such checks were to be added.",
      "axis": "proof-golf",
      "supporting_past_prs": [
        2,
        14
      ]
    }
  ]
}