openpr_W_v2_sweep2.txt

====================================================================================================
CASE W  PR #34007  (open-pr, v2 prompt, sweep2)
file: Mathlib/Algebra/Module/Submodule/Dual.lean  line: 49.0
reviewer: @joelriou  on 2026-01-30T19:34:13Z
advice_kind: generalize: two modules M₁/M₂ not one
prompt_tokens: 7041  completion_tokens: 2297
HUMAN reviewer (ground truth):
  > We already have similar definitions in a slightly less general context at https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/SesquilinearForm/Basic.html#Submodule.orthogonalBilin and https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.html#LinearMap.BilinForm.orthogonal
  > It would seem sensible to me to unify all of these.
====================================================================================================

[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.

Compared to a naive matcher you must do TWO extra things, because the answer is often only derivable by combining evidence:

A. STRUCTURAL PATTERN EXTRACTION. Past comments often contain `suggestion` code blocks (```suggestion ... ```) or inline code-shape rewrites. These suggested code snippets ARE concrete advice, not just commentary. Treat them as first-class evidence about preferred Lean/mathlib idioms (e.g.: term-mode constructor `:= ⟨_, _, _⟩` vs `by use _; exact _`, `instance` vs `theorem` for class-membership statements, `refine ⟨..., ?_⟩` vs `use ...; constructor`, `@[simp]` / `@[to_additive]` attributes, naming conventions, docstring phrasing, etc.).

B. CROSS-CANDIDATE SYNTHESIS. The applicable advice for the new hunk may require combining evidence from multiple candidates. Example: candidate X's context tells you that an identifier in the new hunk is a `class`; candidate Y shows the term-mode `instance ... := ⟨...⟩` template for proving class membership. Together they support the conclusion: "the new theorem proving class membership should be rewritten as an `instance` with a term-mode constructor". List supporting PRs for any synthesised finding.

Reasoning protocol (do this internally before producing JSON):

  1. STRUCTURAL FEATURES OF THE NEW HUNK. Identify each: tactic-mode vs term-mode? Uses `by use ...; exact ...`? Uses `use ...; constructor`? Declares an `instance` / a `theorem` / a `lemma` / a `def` / a `class`? Has `@[simp]`, `@[to_additive]`, `@[deprecated]`? Uses anonymous functions `fun x =>` vs `↦`? Has a docstring `/-- ... -/` of any specific shape?

  2. PATTERN INVENTORY FROM CANDIDATES. For each candidate, note any concrete pattern shown in its suggested-code or comment (term-mode template, attribute recommendation, naming convention, idiomatic rewrite, terminology preference, etc.). Also note which candidates' past hunks define or use identifiers that appear in the new hunk (these are clues about whether something is a class, an instance, an alias, etc.).

  3. APPLICABILITY CHECK. For each pattern from step 2, ask: does the new hunk's structure (step 1) instantiate the same shape that this pattern was applied to? If yes, that's a STRONG match. If two patterns combine to support a finding, list both supporting PRs.

  4. STRICT REFUSAL. If after this analysis no candidate (alone or in combination) gives concrete, well-grounded advice for the specific code in the new hunk, output an empty `strong_matches` list. Do not paper over with generic advice. Generic style observations belong in `weak_observations`, clearly marked. Do not invent advice that isn't traceable to specific past PRs in the retrieval pool.

Confidence:
  - "high"  — at least one strong match is grounded in concrete suggested-code or explicit prose from a candidate, and the new hunk clearly fits the same shape
  - "medium" — at least one strong match exists but requires synthesis or adaptation; OR a single candidate gives related but not identical advice
  - "low"   — only loose stylistic patterns; nothing actionable
  - "none"  — retrieved pool is unrelated; do not press an answer

Output JSON ONLY, matching this exact schema:

{
  "summary": "<one sentence describing what we found>",
  "confidence": "high"|"medium"|"low"|"none",
  "strong_matches": [
    {
      "past_pr": <int>,
      "past_file": "<string>",
      "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>",
      "suggested_adaptation": "<one sentence on what the reviewer might say on the new hunk>",
      "supporting_past_prs": [<int>, ...]
    }
  ],
  "weak_observations": [
    {
      "observation": "<short string>",
      "supporting_past_prs": [<int>, ...]
    }
  ]
}

Quote short — under 40 words per excerpt. Be precise about which PR(s) support each finding via supporting_past_prs.

[USER]
----------------------------------------------------------------------------------------------------
NEW HUNK from open PR #34007 (file: Mathlib/Algebra/Module/Submodule/Dual.lean):
```
@@ -0,0 +1,235 @@
... [9 lines above hidden]
+public import Mathlib.LinearAlgebra.Pi
+
+/-!
+# The algebraic dual of a submodule
+
+Given a bilinear pairing `p` between two `R`-modules `M` and `N` and a set `s` in `M`, we define
+`Submodule.dual p s` to be the submodule in `N` consisting of all points `y` such that
+`0 = p x y` for all `x ∈ s`.
+
+See also `PointedCone.dual`.
+
+## Main declarations
+
+- `Submodule.dual` is the dual submodule of a set `s` w.r.t. a bilinear pairing `p`.
+
+## Notes
+
+- In case that the pairing is `Dual.eval R M`, the dual of a submodule `S` is identical to the
+  dual annihilator `S` (see `dual_dualAnnihilator`).
+- In case that the pairing is `LinealMap.id`, the dual of a submodule `S` is identical to the
+  dual coannihilator `S` (see `dual_dualCoannihilator`).
+
+-/
+
+@[expose] public section
+
+assert_not_exists TopologicalSpace Real Cardinal
+
+open Module Set LinearMap
+
+namespace Submodule
+
+variable {R : Type*} [CommSemiring R]
+variable {M : Type*} [AddCommMonoid M] [Module R M]
+variable {N : Type*} [AddCommMonoid N] [Module R N]
+variable {p : M →ₗ[R] N →ₗ[R] R} {s t : Set M}
+
+variable (p s) in
+/-- The dual span of a set `s` with respect to a bilinear pairing `p` is the submodule
+  consisting of the points `y` such that for all points `x ∈ s` we have `0 = p x y`. -/
+def dual : Submodule R N where
```

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

--- candidate 1 (sim=0.794, past_pr=#24149, file=Mathlib/Geometry/Convex/Cone/Dual.lean) ---
PAST HUNK:
```
@@ -0,0 +1,90 @@
... [67 lines above hidden]
+/-- The dual cone of `s` equals the intersection of dual cones of the points in `s`. -/
+lemma dual_eq_iInter_dual_singleton (s : Set M) :
+    dual p s = ⋂ i : s, (dual p {i.val} : Set N) := by ext; simp
+
+/-- Any set is a subset of its double dual cone. -/
+lemma subset_dual_dual : s ⊆ dual p.flip (dual p s) := fun _x hx _y hy ↦ hy hx
+
+variable (s) in
+@[simp] lemma dual_dual_flip_dual : dual p (dual p.flip (dual p s)) = dual p s :=
+  le_antisymm (dual_le_dual subset_dual_dual) subset_dual_dual
+
+@[simp] lemma dual_flip_dual_dual_flip (s : Set N) :
+    dual p.flip (dual p (dual p.flip s)) = dual p.flip s := dual_dual_flip_dual _
```
PAST COMMENT (from reviewer):
Is there some way to phrase these instead as "the double dual of every Y cone is itself" (in both forms), and "every dual is Y", rather than as a triple dual? (I'm guessing the answer is "yes it's coming", in which case let's have a TODO for it)

--- candidate 2 (sim=0.793, past_pr=#8997, file=Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean) ---
PAST HUNK:
```
@@ -0,0 +1,130 @@
... [45 lines above hidden]
+/-- The natural paring of `B.dualSubmodule N` and `N`.
+This is bundled as a bilinear map in `BilinForm.dualSubmoduleToDual`. -/
+noncomputable
+def dualSubmoduleParing {N : Submodule R M} (x : B.dualSubmodule N) (y : N) : R :=
+  (x.prop y y.prop).choose
+
+@[simp]
+lemma dualSubmoduleParing_spec {N : Submodule R M} (x : B.dualSubmodule N) (y : N) :
+    algebraMap R S (B.dualSubmoduleParing x y) = B x y :=
+  (x.prop y y.prop).choose_spec
+
+/-- The natural paring of `B.dualSubmodule N` and `N`. -/
+-- TODO: Show that this is perfect when `N` is a lattice.
```
PAST COMMENT (from reviewer):
```suggestion
-- TODO: Show that this is perfect when `N` is a lattice and `B` is nondegenerate.
```
Or something like that.

--- candidate 3 (sim=0.785, past_pr=#8997, file=Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean) ---
PAST HUNK:
```
@@ -0,0 +1,130 @@
... [70 lines above hidden]
+      (by simp [← Algebra.smul_def]) }
+
+lemma dualSubmoduleToDual_injective (hB : B.Nondegenerate) [NoZeroSMulDivisors R S]
+    (N : Submodule R M) (hN : Submodule.span S (N : Set M) = ⊤) :
+    Function.Injective (B.dualSubmoduleToDual N) := by
+  intro x y e
+  ext
+  apply LinearMap.ker_eq_bot.mp hB.ker_eq_bot
+  apply LinearMap.ext_on hN
+  intro z hz
+  simpa using congr_arg (algebraMap R S) (LinearMap.congr_fun e ⟨z, hz⟩)
+
+lemma dualSubmodule_span_of_basis {ι} [Fintype ι] [DecidableEq ι] [FiniteDimensional S M]
```
PAST COMMENT (from reviewer):
You can write
```
let _ : FiniteDimensional S M := ...
```
before the `:` and it should be happy (not 100% sure the syntax is exactly that, but it is similar, and I forgot if we want `let` or `letI` here).

--- candidate 4 (sim=0.774, past_pr=#6437, file=Mathlib/Analysis/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2023 Apurva Nakade All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Apurva Nakade
+-/
+import Mathlib.Analysis.Convex.Cone.Dual
+import Mathlib.Algebra.Order.Nonneg.Module
+import Mathlib.Algebra.Module.Submodule.Basic
+
+
```
PAST COMMENT (from reviewer):
```suggestion

```

--- candidate 5 (sim=0.759, past_pr=#32920, file=Mathlib/Algebra/Module/Submodule/Union.lean) ---
PAST HUNK:
```
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Module.Submodule.Lattice
 public import Mathlib.Data.Set.Card
-public import Mathlib.LinearAlgebra.Dual.Defs
+public import Mathlib.LinearAlgebra.Dual.Lemmas
```
PAST COMMENT (from reviewer):
Can you keep `Mathlib.LinearAlgebra.Dual.Defs` as public and then privately import `Mathlib.LinearAlgebra.Dual.Lemmas` since it's only used in the proof?

Reason for this is that importing `.Lemmas` could cause problems downstream if this gets imported somewhere (probably because of too many instances?). For example, `RingTheory/Spectrum/Prime/Polynomial` is one of those files that gets problems.
This came up in https://github.com/leanprover-community/mathlib4/pull/32671/files#r2616327511.

--- candidate 6 (sim=0.757, past_pr=#32920, file=Mathlib/Algebra/Module/Submodule/Union.lean) ---
PAST HUNK:
```
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Module.Submodule.Lattice
 public import Mathlib.Data.Set.Card
-public import Mathlib.LinearAlgebra.Dual.Defs
+public import Mathlib.LinearAlgebra.Dual.Lemmas
```
PAST COMMENT (from reviewer):
What made you change your mind? :eyes:

--- candidate 7 (sim=0.744, past_pr=#20084, file=Mathlib/Analysis/Normed/Module/Dual.lean) ---
PAST HUNK:
```
@@ -152,9 +152,19 @@ def polar (𝕜 : Type*) [NontriviallyNormedField 𝕜] {E : Type*} [SeminormedA
... [3 lines above hidden]
 
+/-- Given a subset `s` in a normed space `E` (over a field `𝕜`) closed under scalar multiplication,
+ the polar `polarSubmodule 𝕜 s` is the submodule of `Dual 𝕜 E` consisting of those functionals which
+evaluate to zero at all points `z ∈ s`. -/
+def polarSubmodule (𝕜 : Type*) [NontriviallyNormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E]
+    [NormedSpace 𝕜 E] {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
+    Submodule 𝕜 (Dual 𝕜 E) := (dualPairing 𝕜 E).flip.polarSubmodule m
+
 variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
+lemma polarSubmodule_eq_polar (m : SubMulAction 𝕜 E) :
+    SetLike.coe (polarSubmodule 𝕜 m) = polar 𝕜 m := rfl
```
PAST COMMENT (from reviewer):
```suggestion
    (polarSubmodule 𝕜 m : Set (Submodule 𝕜 (Dual 𝕜 E))) = polar 𝕜 m := rfl
```

--- candidate 8 (sim=0.741, past_pr=#24244, file=Mathlib/RingTheory/Regular/Depth.lean) ---
PAST HUNK:
```
@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2025 Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan, Yi Song
+-/
+import Mathlib.Algebra.Module.FinitePresentation
+import Mathlib.LinearAlgebra.Dual.Lemmas
```
PAST COMMENT (from reviewer):
This (`Mathlib.LinearAlgebra.Dual.Lemmas`) is a common superfluous import by `#min_import`. Can you confirm if this is actually necessary or not?

--- candidate 9 (sim=0.740, past_pr=#16707, file=Mathlib/Analysis/InnerProductSpace/Dual.lean) ---
PAST HUNK:
```
@@ -69,6 +70,61 @@ variable {E}
 theorem toDualMap_apply {x y : E} : toDualMap 𝕜 E x y = ⟪x, y⟫ :=
   rfl
 
+section NullSubmodule
+
+open SeparationQuotient LinearMap
+
+variable (E)
+
+/-- The null space with respect to the norm. -/
+def nullSubmodule : Submodule 𝕜 E where
```
PAST COMMENT (from reviewer):
Because you've defined this here, you're assuming that `E` is an inner product space and `𝕜` is `RCLike`, but there's no reason the definition needs to be anywhere near this restrictive. You're going to want to define `nullSubmodule` in a separate file, and then prove the results specific to inner product spaces here. In fact, I think it's only the `ker` results that stay in this file.

--- candidate 10 (sim=0.739, past_pr=#27645, file=Mathlib/Geometry/Convex/Cone/TensorProduct.lean) ---
PAST HUNK:
```
@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2025 Bjørn Solheim. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bjørn Solheim
+-/
+import Mathlib.Geometry.Convex.Cone.Dual
+import Mathlib.LinearAlgebra.TensorProduct.Basic
+import Mathlib.LinearAlgebra.Dual.Lemmas
```
PAST COMMENT (from reviewer):
```suggestion
import Mathlib.LinearAlgebra.Dual.Lemmas
import Mathlib.LinearAlgebra.TensorProduct.Basic
```

--- candidate 11 (sim=0.730, past_pr=#29241, file=Mathlib/Analysis/Convex/Cone/Dual.lean) ---
PAST HUNK:
```
@@ -139,7 +139,7 @@ theorem hyperplane_separation_point (C : ProperCone ℝ E) (hx₀ : x₀ ∉ C)
 @[simp] theorem dual_flip_dual (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [p.IsContPerfPair] (C : ProperCone ℝ E) :
     dual p.flip (dual p (C : Set E)) = C := by
   refine le_antisymm (fun x ↦ ?_) subset_dual_dual
-  simp only [mem_toPointedCone, mem_dual, SetLike.mem_coe]
+  simp only [ClosedSubmodule.mem_toSubmodule_iff, mem_dual, SetLike.mem_coe, flip_apply]
```
PAST COMMENT (from reviewer):
I'd prefer to keep the original `simp only` because the lemma it uses is more meaningful in this context.

--- candidate 12 (sim=0.728, past_pr=#23945, file=Mathlib/LinearAlgebra/Dual/Lemmas.lean) ---
PAST HUNK:
```
@@ -289,6 +289,11 @@ namespace Submodule
 
 open Module
 
+@[simp]
+theorem dualCoannihilator_top {K M : Type*} [Field K] [AddCommGroup M] [Module K M] :
+    (⊤ : Submodule K (Module.Dual K M)).dualCoannihilator = ⊥ := by
+  rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]
+
 variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M}
```
PAST COMMENT (from reviewer):
Let's move this down so that we can use the `variable`s and generalise as follows:
```suggestion
variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M}

@[simp]
theorem dualCoannihilator_top [Projective R M] :
    (⊤ : Submodule R (Module.Dual R M)).dualCoannihilator = ⊥ := by
  rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]
```

--- candidate 13 (sim=0.722, past_pr=#16707, file=Mathlib/Analysis/InnerProductSpace/Dual.lean) ---
PAST HUNK:
```
@@ -69,6 +70,61 @@ variable {E}
 theorem toDualMap_apply {x y : E} : toDualMap 𝕜 E x y = ⟪x, y⟫ :=
   rfl
 
+section NullSubmodule
+
+open SeparationQuotient LinearMap
+
+variable (E)
+
```
PAST COMMENT (from reviewer):
You don't want this to be explicit everywhere. Similarly, `𝕜` should only be explicit when the hypotheses don't mention `𝕜`, but the conclusion does (e.g., `inner_eq_zero_of_left`.
```suggestion
variable (E) in
```

--- candidate 14 (sim=0.721, past_pr=#18559, file=Mathlib/LinearAlgebra/PerfectPairing.lean) ---
PAST HUNK:
```
@@ -129,6 +161,135 @@ include p in
... [27 lines above hidden]
+      simpa only [apply_toDualLeft_symm_apply] using hg _ (LinearMap.mem_range_self j n)
+    rw [hm, ← LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm,
+      toDualLeft_apply] at hm'
+    simpa [← hF, ← LinearMap.congr_fun hm' (j n)]
+
+/-- The restriction of a perfect pairing to submodules (expressed as injections to provide
+definitional control). -/
+@[simps]
+def restrict {M' N' : Type*} [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N']
+    (i : M' →ₗ[R] M) (hi : Injective i)
+    (j : N' →ₗ[R] N) (hj : Injective j)
+    (hM : IsCompl (LinearMap.range i) ((LinearMap.range j).dualAnnihilator.map p.toDualLeft.symm))
+    (hN : IsCompl (LinearMap.range j) ((LinearMap.range i).dualAnnihilator.map p.toDualRight.symm)):
```
PAST COMMENT (from reviewer):
```suggestion
    (hN : IsCompl (LinearMap.range j) ((LinearMap.range i).dualAnnihilator.map p.toDualRight.symm)) :
```

--- candidate 15 (sim=0.718, past_pr=#35323, file=Mathlib/Geometry/Convex/Cone/Dual.lean) ---
PAST HUNK:
```
@@ -86,20 +89,45 @@ lemma dual_eq_iInter_dual_singleton (s : Set M) :
... [30 lines above hidden]
   | mem _y h => exact hx h
   | zero => simp
   | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
   | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
 
+@[simp] lemma dual_sup (C D : PointedCone R M) : dual p (C ⊔ D : PointedCone R M) = dual p (C ∪ D)
+  := by simp [← dual_span]
+
+lemma dual_id (s : Set M) : dual p s = dual .id (p '' s) := by ext; simp
+
+lemma dual_id_map (C : PointedCone R M) : dual p C = dual .id (map p C) := by ext; simp
+
+lemma dual_eval (s : Set M) : dual p s = comap p.flip (dual (Module.Dual.eval R M) s) := by
```
PAST COMMENT (from reviewer):
Surely the RHS is more complicated than the RHS, so this should be turned around?

--- candidate 16 (sim=0.717, past_pr=#27699, file=Mathlib/Topology/Algebra/Module/StrongDual.lean) ---
PAST HUNK:
```
@@ -0,0 +1,168 @@
... [2 lines above hidden]
+Copyright (c) 2020 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth
+-/
+import Mathlib.Topology.Algebra.Module.LinearMap
+import Mathlib.Analysis.LocallyConvex.Polar
+
+/-!
+# The topological strong dual of a module
+
+## Main definitions
+
+- `strongDualPairing`: The StrongDual pairing as a bilinear form.
```
PAST COMMENT (from reviewer):
```suggestion
- `strongDualPairing`: The strong dual pairing as a bilinear form.
```

--- candidate 17 (sim=0.717, past_pr=#35323, file=Mathlib/Geometry/Convex/Cone/Dual.lean) ---
PAST HUNK:
```
@@ -86,20 +89,45 @@ lemma dual_eq_iInter_dual_singleton (s : Set M) :
... [30 lines above hidden]
   | mem _y h => exact hx h
   | zero => simp
   | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
   | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
 
+@[simp] lemma dual_sup (C D : PointedCone R M) : dual p (C ⊔ D : PointedCone R M) = dual p (C ∪ D)
+  := by simp [← dual_span]
+
+lemma dual_id (s : Set M) : dual p s = dual .id (p '' s) := by ext; simp
+
+lemma dual_id_map (C : PointedCone R M) : dual p C = dual .id (map p C) := by ext; simp
+
+lemma dual_eval (s : Set M) : dual p s = comap p.flip (dual (Module.Dual.eval R M) s) := by
```
PAST COMMENT (from reviewer):
If your lemma aren't standard simplification lemmas, then I would highly suggest:
1. You explain how they are supposed to be used in their docstring
2. You follow the semantic naming convention rather than the syntactic one

--- candidate 18 (sim=0.713, past_pr=#27699, file=Mathlib/Topology/Algebra/Module/StrongDual.lean) ---
PAST HUNK:
```
@@ -0,0 +1,173 @@
... [44 lines above hidden]
+
+@[simp]
+theorem dualPairing_apply {v : StrongDual R M} {x : M} : strongDualPairing R M v x = v x :=
+  rfl
+
+@[deprecated (since := "2025-08-3")] alias NormedSpace.dualPairing_apply := dualPairing_apply
+
+end
+
+section
+
+variable (R : Type*) [SeminormedCommRing R]
+variable (M : Type*) [TopologicalSpace M] [AddCommGroup M] [Module R M]
```
PAST COMMENT (from reviewer):
```suggestion
variable (R M : Type*) [SeminormedCommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M]
```

--- candidate 19 (sim=0.712, past_pr=#20084, file=Mathlib/Analysis/Normed/Module/Dual.lean) ---
PAST HUNK:
```
@@ -152,12 +152,26 @@ def polar (𝕜 : Type*) [NontriviallyNormedField 𝕜] {E : Type*} [SeminormedA
... [10 lines above hidden]
+
 variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
+lemma polarSubmodule_eq_polar (m : SubMulAction 𝕜 E) :
+    (polarSubmodule 𝕜 m : Set (Dual 𝕜 E)) = polar 𝕜 m := rfl
+
 theorem mem_polar_iff {x' : Dual 𝕜 E} (s : Set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1 :=
   Iff.rfl
 
+lemma mem_polarSubmodule {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
+    polarSubmodule 𝕜 m = { y : Dual 𝕜 E | ∀ x ∈ m, y x  = 0 } :=
+  (dualPairing 𝕜 E).flip.polar_subMulAction _
```
PAST COMMENT (from reviewer):
```suggestion
lemma polarSubmodule_eq_setOf {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
    polarSubmodule 𝕜 m = { y : Dual 𝕜 E | ∀ x ∈ m, y x = 0 } :=
  (dualPairing 𝕜 E).flip.polar_subMulAction _

lemma mem_polarSubmodule {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) (y : Dual 𝕜 E) :
    y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x  = 0 :=
  Iff.rfl
```

(untested)

--- candidate 20 (sim=0.705, past_pr=#33323, file=Mathlib/Algebra/Module/Submodule/Lattice.lean) ---
PAST HUNK:
```
@@ -22,7 +22,8 @@ This file defines the lattice structure on submodules, `Submodule.CompleteLattic
 defined as `{0}` and `⊓` defined as intersection of the underlying carrier.
 If `p` and `q` are submodules of a module, `p ≤ q` means that `p ⊆ q`.
 
-Many results about operations on this lattice structure are defined in `LinearAlgebra/Basic.lean`,
+Many results about operations on this lattice structure are defined in
+`Mathlib/LinearAlgebra/Span/Defs.lean`,
 most notably those which use `span`.
```
PAST COMMENT (from reviewer):
I don't think this comment is really helping anyone and is in danger of breaking again, let's just excise it.
```suggestion
```


Decide which candidates' comments genuinely apply to the NEW hunk. If none, say so. Output JSON only.

[ASSISTANT]
----------------------------------------------------------------------------------------------------
{
  "summary": "No concrete past reviewer suggestion clearly applies; only a weak stylistic parallel about using `variable (...) in` for scoping.",
  "confidence": "none",
  "strong_matches": [],
  "weak_observations": [
    {
      "observation": "Using `variable (p s) in` to scope explicit parameters matches prior advice to localize explicit variables (e.g., `variable (E) in`).",
      "supporting_past_prs": [
        16707
      ]
    },
    {
      "observation": "Be mindful about `public import` vs `private import` for potentially heavy dependencies; past reviews suggested keeping heavier `.Lemmas` private. Not directly triggered here but a general caution.",
      "supporting_past_prs": [
        32920,
        24244
      ]
    }
  ]
}