openpr_T_v3_1.txt

====================================================================================================
CASE T  PR #20431  (open-pr, v3.1 prompt)
file: Mathlib/RingTheory/AdicCompletion/Basic.lean  line: 535.0
reviewer: @chrisflav  on 2025-02-10T09:08:05Z
advice_kind: design smell: _root_ placement
prompt_tokens: 8132  completion_tokens: 4237
HUMAN reviewer (ground truth):
  > Maybe move these after `end AdicCompletion` to get rid of the ugly `_root_`?
====================================================================================================

[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 #20431 (file: Mathlib/RingTheory/AdicCompletion/Basic.lean):
```
@@ -510,6 +522,29 @@ theorem induction_on {p : AdicCompletion I M → Prop} (x : AdicCompletion I M)
   obtain ⟨f, rfl⟩ := mk_surjective I M x
   exact h f
 
+variable {I M} in
+lemma _root_.IsHausdorff.iff_injective :
+    IsHausdorff I M ↔ Injective (AdicCompletion.of I M) := by
+  simp [injective_iff_map_eq_zero, isHausdorff_iff, SModEq.zero, AdicCompletion.ext_iff]
+
+variable {I M} in
+lemma _root_.IsPrecomplete.iff_surjective :
+    IsPrecomplete I M ↔ Surjective (AdicCompletion.of I M) := by
+  simp [Function.Surjective, (AdicCompletion.mk_surjective I M).forall,
+    AdicCompletion.ext_iff, isPrecomplete_iff, AdicCauchySequence, Subtype.forall,
+    eq_comm (a := Submodule.Quotient.mk _)]
```

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

--- candidate 1 (sim=0.889, past_pr=#25927, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -518,10 +521,238 @@ lemma eval_lift_apply (f : ∀ (n : ℕ), M →ₗ[R] N ⧸ (I ^ n • ⊤ : Sub
... [48 lines above hidden]
+      toIsPrecomplete := surjective_of_iff.mp h.2 },
+   fun h ↦ ⟨injective_of_iff.mpr h.1, surjective_of_iff.mpr h.2⟩⟩
+
+variable (I M) in
+theorem bijective_of [IsAdicComplete I M] : Function.Bijective (of I M) :=
+  bijective_of_iff.mpr ‹_›
+
+variable (I M) in
+/--
+When `M` is `I`-adic complete, the canonical map from `M` to its `I`-adic completion is a linear
+equivalence.
+-/
+def ofLinearEquiv [IsAdicComplete I M] : M ≃ₗ[R] AdicCompletion I M :=
```
PAST COMMENT (from reviewer):
```suggestion
@[simps! apply symm_apply]
def ofLinearEquiv [IsAdicComplete I M] : M ≃ₗ[R] AdicCompletion I M :=
```
Should automatically generate the two lemmas below (the second one is misnamed anyway).

--- candidate 2 (sim=0.889, past_pr=#25927, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -518,6 +517,72 @@ lemma eval_lift_apply (f : ∀ (n : ℕ), M →ₗ[R] N ⧸ (I ^ n • ⊤ : Sub
... [52 lines above hidden]
+      toIsPrecomplete := of_surjective_iff.mp h.2 },
+   fun h ↦ ⟨of_injective_iff.mpr h.1, of_surjective_iff.mpr h.2⟩⟩
+
+variable (I M) in
+theorem of_bijective [IsAdicComplete I M] : Function.Bijective (of I M) :=
+  of_bijective_iff.mpr ‹_›
+
+variable (I M) in
+/--
+When `M` is `I`-adic complete, the canonical map from `M` to its `I`-adic completion is a linear
+equivalence.
+-/
+@[simps! apply symm_apply]
```
PAST COMMENT (from reviewer):
I don't think we want `symm_apply` to be a simp lemma?
```suggestion
@[simps! apply]
```
instead you want the lemmas `ofLinearEquiv_symm_of` and `of_ofLinearEquiv_symm`

--- candidate 3 (sim=0.828, past_pr=#21582, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -48,33 +48,404 @@ class IsAdicComplete extends IsHausdorff I M, IsPrecomplete I M : Prop
... [31 lines above hidden]
+is not defeq to `I ^ n • ⊤`.
+-/
+theorem eq_iff_smodEq' [IsHausdorff I R]
+    {x y : R} :  x = y ↔ ∀ n, x ≡ y [SMOD I ^ n] := by
+  refine ⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩
+  rw [← sub_eq_zero]
+  apply IsHausdorff.haus' (I := I) (x - y)
+  simpa [SModEq.sub_mem] using h
+
+alias ⟨_, eq_of_smodEq'⟩ := eq_iff_smodEq'
+
+variable {a : ℕ → ℕ} (ha : StrictMono a)
+include ha
```
PAST COMMENT (from reviewer):
Can you create a new section here? Even without name, just to make sure that the `include ha` does not leak.

--- candidate 4 (sim=0.810, past_pr=#21582, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -48,33 +48,404 @@ class IsAdicComplete extends IsHausdorff I M, IsPrecomplete I M : Prop
... [220 lines above hidden]
+    have := hL n
+    apply_fun (i n).symm at this
+    simpa only [RingEquiv.symm_apply_apply, mkQ_apply, mk_eq_mk, quotientEquiv_symm_mk,
+      RingEquiv.symm_refl, RingEquiv.refl_apply, i, f'] using this
+  apply IsPrecomplete.of_eq_factorPowSucc
+  intro m
+  have := hf (m := m)
+  apply_fun i m at this
+  simpa [f', i, Submodule.factorPowSucc, Submodule.factorPow,
+      Ideal.quotEquivOfEq_eq_factor] using this
+
+variable {a : ℕ → ℕ} (ha : StrictMono a)
+include ha
```
PAST COMMENT (from reviewer):
Same as above.

--- candidate 5 (sim=0.776, past_pr=#12516, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -201,67 +203,279 @@ instance (priority := 100) of_subsingleton [Subsingleton M] : IsPrecomplete I M
... [256 lines above hidden]
+/-- Every element in the adic completion is represented by a Cauchy sequence. -/
+theorem mk_surjective : Function.Surjective (mk I M) := by
+  intro x
+  choose a ha using fun n ↦ Submodule.Quotient.mk_surjective _ (x.val n)
+  refine ⟨⟨a, ?_⟩, ?_⟩
+  · intro m n hmn
+    rw [SModEq.def, ha m, ← transitionMap_mk I M hmn, ha n, x.property hmn]
+  · ext n
+    simp [ha n]
+
+/-- To show a statement about an element of `adicCompletion I M`, it suffices to check it
+on Cauchy sequences. -/
+theorem inductionOn {p : AdicCompletion I M → Prop} (x : AdicCompletion I M)
```
PAST COMMENT (from reviewer):
```suggestion
theorem induction_on {p : AdicCompletion I M → Prop} (x : AdicCompletion I M)
```

--- candidate 6 (sim=0.775, past_pr=#12516, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -201,67 +210,204 @@ instance (priority := 100) of_subsingleton [Subsingleton M] : IsPrecomplete I M
... [92 lines above hidden]
+    transitionMap I M hmn
+      (Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R M)) x) =
+      Submodule.Quotient.mk (p := (I ^ m • ⊤ : Submodule R M)) x := by
+  simp [transitionMap]
+
+@[simp]
+theorem transitionMap_eq (n : ℕ) : transitionMap I M (Nat.le_refl n) = LinearMap.id := by
+  ext
+  simp
+
+@[simp]
+theorem transitionMap_comp {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
+    transitionMap I M hmn ∘ₗ transitionMap I M hnk = transitionMap I M (hmn.trans hnk) := by
```
PAST COMMENT (from reviewer):
Can you add `(transitionMap I M hmn (transitionMap I M hnk x)) = transitionMap I M (hmn.trans hnk) x` as a simp lemma?

--- candidate 7 (sim=0.749, past_pr=#30058, file=Mathlib/RingTheory/AdicCompletion/Topology.lean) ---
PAST HUNK:
```
@@ -0,0 +1,56 @@
... [36 lines above hidden]
+      simpa using hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mp hu
+    choose N hN using this
+    obtain ⟨L, hL⟩ := H (fun i ↦ u ((Finset.Iic i).sup N))
+      fun _ ↦ hN _ _ (Finset.le_sup (by simpa)) _ (Finset.le_sup (by simp))
+    use L
+    suffices ∀ i, ∃ N, ∀ n, N ≤ n → u n - L ∈ I ^ i by
+      simpa [(hI.hasBasis_nhds L).tendsto_right_iff, sub_eq_neg_add]
+    refine fun i ↦ ⟨(Finset.Iic i).sup N, fun n hn ↦ ?_⟩
+    have := Ideal.add_mem _ (hN i ((Finset.Iic i).sup N) (Finset.le_sup (by simp))
+      n (.trans (Finset.le_sup (by simp)) hn)) (hL i)
+    rwa [sub_add_sub_cancel] at this
+  · intro H f hf
+    obtain ⟨L, hL⟩ := CompleteSpace.complete (f := (Filter.atTop.map f))
```
PAST COMMENT (from reviewer):
```suggestion
    obtain ⟨L, hL⟩ := CompleteSpace.complete (f := Filter.atTop.map f)
```

--- candidate 8 (sim=0.741, past_pr=#26384, file=Mathlib/RingTheory/AdicCompletion/Functoriality.lean) ---
PAST HUNK:
```
@@ -360,4 +364,102 @@ end Pi
... [90 lines above hidden]
+
+theorem surjective_of_mk_map_comp_surjective [IsPrecomplete I R] [haus : IsHausdorff (I.map f) S]
+    (h : Function.Surjective ((Ideal.Quotient.mk (I.map f)).comp f)) :
+    Function.Surjective f := by
+  let _ := f.toAlgebra
+  let fₗ := (Algebra.ofId R S).toLinearMap
+  change Function.Surjective ((restrictScalars R (I.map f)).mkQ ∘ₗ fₗ) at h
+  have : I • ⊤ = restrictScalars R (Ideal.map f I) := by
+    simp only [Ideal.smul_top_eq_map, restrictScalars_inj]
+    rfl
+  have _ := IsHausdorff.map_algebraMap_iff.mp haus
+  apply surjective_of_mkQ_comp_surjective (I := I) (f := fₗ)
+  convert h
```
PAST COMMENT (from reviewer):
Does `exact h` work?

--- candidate 9 (sim=0.739, past_pr=#30058, file=Mathlib/RingTheory/AdicCompletion/Topology.lean) ---
PAST HUNK:
```
@@ -0,0 +1,56 @@
... [19 lines above hidden]
+section UniformSpace
+
+open Topology Uniformity
+
+variable {R : Type*} [CommRing R] [UniformSpace R] [IsUniformAddGroup R]
+  {I : Ideal R} (hI : IsAdic I)
+
+include hI in
+/-- `IsPrecomplete I R` is equivalent to being complete in the adic topology. -/
+lemma IsAdic.isPrecomplete_iff : IsPrecomplete I R ↔ CompleteSpace R := by
+  have := hI.hasBasis_nhds_zero.isCountablyGenerated
+  have : (𝓤 R).IsCountablyGenerated := IsUniformAddGroup.uniformity_countably_generated
+  simp only [_root_.isPrecomplete_iff, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
```
PAST COMMENT (from reviewer):
Would it be a good idea to protect `IsAdic.isPrecomplete_iff`?

--- candidate 10 (sim=0.732, past_pr=#12650, file=Mathlib/RingTheory/AdicCompletion/Exactness.lean) ---
PAST HUNK:
```
@@ -0,0 +1,205 @@
... [71 lines above hidden]
+  let a := mapPreimage hf b
+  refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
+  · refine fun n ↦ SModEq.symm ?_
+    simp only [SModEq.symm, SModEq, mapPreimage, Submodule.Quotient.mk_sub,
+      sub_eq_self, Submodule.Quotient.mk_eq_zero, SetLike.coe_mem, a]
+  · exact _root_.AdicCompletion.ext fun n ↦ congrArg _ ((a n).property)
+
+end Surjectivity
+
+variable {M : Type u} [AddCommGroup M] [Module R M]
+variable {N : Type u} [AddCommGroup N] [Module R N]
+variable {P : Type u} [AddCommGroup P] [Module R P]
+
```
PAST COMMENT (from reviewer):
```suggestion
```

--- candidate 11 (sim=0.731, past_pr=#12650, file=Mathlib/RingTheory/AdicCompletion/Exactness.lean) ---
PAST HUNK:
```
@@ -0,0 +1,205 @@
... [79 lines above hidden]
+
+variable {M : Type u} [AddCommGroup M] [Module R M]
+variable {N : Type u} [AddCommGroup N] [Module R N]
+variable {P : Type u} [AddCommGroup P] [Module R P]
+
+section Injectivity
+
+variable [IsNoetherianRing R] [Module.Finite R N]
+
+open LinearMap
+
+variable (I)
+
```
PAST COMMENT (from reviewer):
```suggestion
variable [IsNoetherianRing R] [Module.Finite R N] (I)

open LinearMap

```

--- candidate 12 (sim=0.727, past_pr=#23027, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -85,8 +85,9 @@ abbrev Hausdorffification : Type _ :=
 to define `AdicCompletion`. -/
 abbrev AdicCompletion.transitionMap {m n : ℕ} (hmn : m ≤ n) := factorPow I M hmn
 
-/-- The completion of a module with respect to an ideal. This is not necessarily Hausdorff.
-In fact, this is only complete if the ideal is finitely generated. -/
+/-- The completion of a module with respect to an ideal. This is Hausdorff but not
+necessarily complete: a typical sufficient condition for completeness is for the ideal to be
+finitely generated. -/
```
PAST COMMENT (from reviewer):
```suggestion
/-- The completion of a module with respect to an ideal. 

This is Hausdorff but not necessarily complete: a classical sufficient condition for completeness is  that `M` be finitely generated [Stacks, 0G1Q]. -/
```

--- candidate 13 (sim=0.700, past_pr=#32064, file=Mathlib/RingTheory/AdicCompletion/Algebra.lean) ---
PAST HUNK:
```
@@ -160,6 +160,24 @@ theorem evalₐ_mk (n : ℕ) (x : AdicCauchySequence I R) :
     evalₐ I n (mk I R x) = Ideal.Quotient.mk (I ^ n) (x.val n) := by
   simp [evalₐ]
 
+variable {I} in
+lemma ext_evalₐ {x y : AdicCompletion I R} (H : ∀ n, evalₐ I n x = evalₐ I n y) : x = y := by
+  ext n
+  have h : (I ^ n • ⊤ : Ideal R) = I ^ n := by ext x; simp
+  exact (Ideal.quotientEquivAlgOfEq R h).injective (H n)
+
+/-- The canonical projection from the `I`-adic completion to `R ⧸ I`. -/
+def evalOneₐ : AdicCompletion I R →ₐ[R] R ⧸ I :=
+  (Ideal.Quotient.factorₐ _ (by simp)).comp (evalₐ _ 1)
```
PAST COMMENT (from reviewer):
Can you provide `evalOneₐ_surjective` as well? Thanks.
It would also be useful to golf `kerProj_surjective`.

--- candidate 14 (sim=0.697, past_pr=#12543, file=Mathlib/RingTheory/AdicCompletion/Functoriality.lean) ---
PAST HUNK:
```
@@ -0,0 +1,352 @@
... [318 lines above hidden]
+end Sum
+
+section Pi
+
+open DirectSum
+
+variable [Fintype ι]
+
+/-- If `ι` is finite, `pi` is a linear equiv. -/
+def piEquivOfFintype :
+    AdicCompletion I (∀ j, M j) ≃ₗ[AdicCompletion I R] ∀ j, AdicCompletion I (M j) :=
+  let f := (congr I (linearEquivFunOnFintype R ι M)).symm
+  let g := (linearEquivFunOnFintype (AdicCompletion I R) ι (fun j ↦ AdicCompletion I (M j)))
```
PAST COMMENT (from reviewer):
```suggestion
  letI f := (congr I (linearEquivFunOnFintype R ι M)).symm
  letI g := (linearEquivFunOnFintype (AdicCompletion I R) ι (fun j ↦ AdicCompletion I (M j)))
```

--- candidate 15 (sim=0.695, past_pr=#29205, file=Mathlib/RingTheory/DedekindDomain/AdicValuation.lean) ---
PAST HUNK:
```
@@ -417,10 +417,6 @@ lemma valuedAdicCompletion_surjective :
     Function.Surjective (Valued.v : (v.adicCompletion K) → ℤᵐ⁰) :=
   Valued.valuedCompletion_surjective_iff.mpr (v.valuation_surjective K)
 
--- Porting note: replaced by `Coe`
--- instance AdicCompletion.hasLiftT : HasLiftT K (v.adicCompletion K) :=
---   (inferInstance : HasLiftT K (@UniformSpace.Completion K v.adicValued.toUniformSpace))
-
```
PAST COMMENT (from reviewer):
I'd like a second pair of eyes, just to confirms this is innocuous.

--- candidate 16 (sim=0.694, past_pr=#12543, file=Mathlib/RingTheory/AdicCompletion/Functoriality.lean) ---
PAST HUNK:
```
@@ -0,0 +1,352 @@
... [6 lines above hidden]
+import Mathlib.RingTheory.AdicCompletion.Basic
+import Mathlib.RingTheory.AdicCompletion.Algebra
+import Mathlib.Algebra.DirectSum.Basic
+
+/-!
+# Functoriality of adic completions
+
+In this file we establish functorial properties of the adic completion.
+
+## Main definitions
+
+- `LinearMap.adicCauchy I f`: the by `f` induced linear map on `I`-adic cauchy sequences
+- `LinearMap.adicCompletion I f`: the by `f` induced linear map on `I`-adic completions
```
PAST COMMENT (from reviewer):
```suggestion
- `LinearMap.adicCauchy I f`: the linear map on `I`-adic cauchy sequences induced by `f`
- `LinearMap.adicCompletion I f`: the by `f` induced linear map on `I`-adic completions
```
Is this what you mean?

--- candidate 17 (sim=0.694, past_pr=#26384, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -71,6 +71,31 @@ theorem IsHausdorff.eq_iff_smodEq [IsHausdorff I M] {x y : M} :
   apply IsHausdorff.haus' (I := I) (x - y)
   simpa [SModEq.sub_mem] using h
 
+theorem IsHausdorff.map_algebraMap_iff [CommRing S] [Algebra R S] :
+    IsHausdorff (I.map (algebraMap R S)) S ↔ IsHausdorff I S := by
+  simp only [isHausdorff_iff, smul_eq_mul, Ideal.mul_top, Ideal.smul_top_eq_map]
+  congr!
+  simp only [← Ideal.map_pow]
+  rfl
+
+lemma IsHausdorff.map [CommRing S] [Module S M] {J : Ideal S} [Algebra R S] [IsScalarTower R S M]
```
PAST COMMENT (from reviewer):
The name  seems weird, shouldn't it be `of_map` or something?

--- candidate 18 (sim=0.693, past_pr=#21563, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -55,6 +55,13 @@ theorem isHausdorff_iff :
     IsHausdorff I M ↔ ∀ x : M, (∀ n : ℕ, x ≡ 0 [SMOD (I ^ n • ⊤ : Submodule R M)]) → x = 0 :=
   ⟨IsHausdorff.haus, fun h => ⟨h⟩⟩
 
+theorem IsHausdorff.eq_iff_smodEq [IsHausdorff I M] {x y : M} :
+    x = y ↔ ∀ n, x ≡ y [SMOD (I ^ n • ⊤ : Submodule R M)] := by
+  refine ⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩
+  rw [← sub_eq_zero]
+  apply IsHausdorff.haus' (I := I) (x - y)
+  simpa only [SModEq.sub_mem, sub_zero] using h
```
PAST COMMENT (from reviewer):
Does `simpa using h` work here? The guideline is not to squeeze if not necessary.

--- candidate 19 (sim=0.686, past_pr=#31295, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -600,6 +604,81 @@ end AdicCompletion
... [40 lines above hidden]
+    (Submodule.Quotient.mk (lift I f h x)) = f n x := by
+  simp only [lift, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
+  rw [← mkQ_apply, ← eval_of]
+  simp
+
+/--
+The composition of lift linear map `lift I f h : M →ₗ[R] N` with the canonical
+projection `N →ₗ[R] N ⧸ (I ^ n • ⊤)` is `f n` .
+-/
+@[simp]
+theorem mkQ_comp_lift {f : (n : ℕ) → M →ₗ[R] N ⧸ (I ^ n • ⊤)}
+    (h : ∀ {m n : ℕ} (hle : m ≤ n), factorPow I N hle ∘ₗ f n = f m) (n : ℕ) :
+    (mkQ (I ^ n • ⊤ : Submodule R N)) ∘ₗ (lift I f h) = f n := by
```
PAST COMMENT (from reviewer):
```suggestion
    mkQ (I ^ n • ⊤ : Submodule R N) ∘ₗ lift I f h = f n := by
```

--- candidate 20 (sim=0.686, past_pr=#31295, file=Mathlib/RingTheory/AdicCompletion/Basic.lean) ---
PAST HUNK:
```
@@ -600,6 +604,81 @@ end AdicCompletion
... [28 lines above hidden]
+theorem of_comp_lift (f : ∀ (n : ℕ), M →ₗ[R] N ⧸ (I ^ n • ⊤ : Submodule R N))
+    (h : ∀ {m n : ℕ} (hle : m ≤ n), factorPow I N hle ∘ₗ f n = f m) :
+    (of I N) ∘ₗ (lift I f h) = AdicCompletion.lift I f h := by
+  ext1; simp
+
+/--
+The composition of lift linear map `lift I f h : M →ₗ[R] N` with the canonical
+projection `N → N ⧸ (I ^ n • ⊤)` is `f n` .
+-/
+@[simp]
+theorem mk_lift {f : (n : ℕ) → M →ₗ[R] N ⧸ (I ^ n • ⊤)}
+    (h : ∀ {m n : ℕ} (hle : m ≤ n), factorPow I N hle ∘ₗ f n = f m) (n : ℕ) (x : M) :
+    (Submodule.Quotient.mk (lift I f h x)) = f n x := by
```
PAST COMMENT (from reviewer):
```suggestion
    Submodule.Quotient.mk (lift I f h x) = f n x := by
```


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"
  ],
  "summary": "No past comments directly apply; only general naming/docstring style observations seem tangentially relevant.",
  "confidence": "low",
  "strong_matches": [],
  "weak_observations": [
    {
      "observation": "Check lemma names fit house style; prior feedback in this file suggested clearer names within the IsHausdorff namespace.",
      "axis": "naming",
      "supporting_past_prs": [
        26384
      ]
    },
    {
      "observation": "Consider adding brief docstrings for new equivalence lemmas to clarify intent.",
      "axis": "docstring",
      "supporting_past_prs": [
        23027
      ]
    }
  ]
}