openpr_L_v2.txt

====================================================================================================
CASE L  PR #35287  (open-pr, v2 prompt)
file: Mathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean  line: 58.0
reviewer: @robin-carlier  on 2026-02-14T10:13:08Z
advice_kind: additional instances suggestion
prompt_tokens: 9986  completion_tokens: 3249
HUMAN reviewer (ground truth):
  > Additionally, you could consider adding extra instances like
  > ```lean
  > instance {x y : WalkingIso.{u}} : Unique (x ⟶ y) := inferInstanceAs (Unique Unit)
  > ```
====================================================================================================

[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 #35287 (file: Mathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean):
```
@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2024 Johns Hopkins Category Theory Seminar, Arnoud van der Leer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johns Hopkins Category Theory Seminar, Arnoud van der Leer
+-/
+module
+
+import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
+import Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
+
+/-!
+# The Coherent Isomorphism
+
+In this file, we define two related types.
+
+We first define the free walking or free-living isomorphism `WalkingIso`: the category with
+two objects `zero` and `one`, and morphisms `zero ⟶ one` and `one ⟶ zero`.
+We show that the type of functor from `WalkingIso` into any category is equivalent to the type of
+isomorphisms in that category.
+
+Then we define the simplicial set `coherentIso` as the nerve of `WalkingIso`.
+Since the morphism types in `WalkingIso` are given by `unit`, the `n`-simplices of `coherentIso` are
+equivalent to `Fin 2`-vectors of length `n + 1`. This shows that the `n`-simplices of `coherentIso`
+have decidable equality.
+Lastly, we show that `hom : coherentIso _⦋1⦌` (the edge from `zero` to `one`) is an isomorphism,
+and `isIsoOfEqMapHom` concludes from this that for any simplicial set `X`,
+any morphism `g : coherentIso ⟶ X` and any `f : X _⦋1⦌`,
+if `g` sends `hom` to `f`, then `f` is an isomorphism.
+
+-/
+
+@[expose] public section
+
+universe u v
+
+open CategoryTheory
+
+namespace CategoryTheory
+
+/-- This is the free-living isomorphism as a category with objects called `zero` and `one`. -/
+def WalkingIso : Type u := ULift (Fin 2)
+
+@[match_pattern]
+def WalkingIso.zero : WalkingIso := ULift.up (0 : Fin 2)
+
+@[match_pattern]
+def WalkingIso.one : WalkingIso := ULift.up (1 : Fin 2)
+
+open WalkingIso
+
+namespace WalkingIso
+
+/-- The free isomorphism is the codiscrete category on two objects. -/
+instance : Category (WalkingIso) where
+  Hom _ _ := Unit
+  id _ := ⟨⟩
+  comp _ _ := ⟨⟩
+
```

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

--- candidate 1 (sim=0.685, past_pr=#26446, file=Mathlib/CategoryTheory/Localization/Construction.lean) ---
PAST HUNK:
```
@@ -343,7 +343,10 @@ def counitIso : inverse W D ⋙ functor W D ≅ 𝟭 (W.FunctorsInverting D) :=
         exact fac G hG
       · rintro ⟨G₁, hG₁⟩ ⟨G₂, hG₂⟩ f
         ext
-        apply NatTransExtension.app_eq)
+        dsimp
+        rw [NatTransExtension.app_eq, InducedCategory.eqToHom_hom,
+          InducedCategory.eqToHom_hom]
+        simp)
```
PAST COMMENT (from reviewer):
I don't understand why `simp` isn't picking up `InducedCategory.eqToHom_hom`. It's not that serious but could you make a comment to highlight this technical debt?

--- candidate 2 (sim=0.685, past_pr=#5409, file=Mathlib/AlgebraicTopology/SplitSimplicialObject.lean) ---
PAST HUNK:
```
@@ -258,11 +258,18 @@ attribute [instance] Splitting.map_isIso
 #align simplicial_object.splitting.map_is_iso SimplicialObject.Splitting.map_isIso
 
 /-- The isomorphism on simplices given by the axiom `Splitting.map_isIso` -/
-@[simps!]
 def iso (Δ : SimplexCategoryᵒᵖ) : coprod s.N Δ ≅ X.obj Δ :=
   asIso (Splitting.map X s.ι Δ)
 #align simplicial_object.splitting.iso SimplicialObject.Splitting.iso
 
+@[simp]
+theorem iso_hom (Δ : SimplexCategoryᵒᵖ) : (iso s Δ).hom = Splitting.map X s.ι Δ :=
+  rfl
+
+@[simp]
+theorem iso_inv (Δ : SimplexCategoryᵒᵖ) : (iso s Δ).inv = inv (Splitting.map X s.ι Δ) :=
+  rfl
+
```
PAST COMMENT (from reviewer):
Because `Splitting.map` is unfolded in `simps` lemmas.
I wonder why `Splitting.map` isn't unfolded in the old Lean.

--- candidate 3 (sim=0.682, past_pr=#749, file=Mathlib/CategoryTheory/Iso.lean) ---
PAST HUNK:
```
@@ -0,0 +1,603 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
+Ported by: Scott Morrison
+-/
+import Mathlib.CategoryTheory.Functor.Basic
+
+/-!
+# Isomorphisms
+
+This file defines isomorphisms between objects of a category.
+
+## Main definitions
+
+- `structure Iso` : a bundled isomorphism between two objects of a category;
+- `class IsIso` : an unbundled version of `iso`;
+  note that `IsIso f` is a `Prop`, and only asserts the existence of an inverse.
+  Of course, this inverse is unique, so it doesn't cost us much to use choice to retrieve it.
+- `inv f`, for the inverse of a morphism with `[IsIso f]`
+- `as_iso` : convert from `IsIso` to `Iso` (noncomputable);
```
PAST COMMENT (from reviewer):
```suggestion
- `asIso` : convert from `IsIso` to `Iso` (noncomputable);
```

--- candidate 4 (sim=0.682, past_pr=#30467, file=Mathlib/CategoryTheory/Iso.lean) ---
PAST HUNK:
```
@@ -222,7 +222,10 @@ def homFromEquiv (α : X ≅ Y) {Z : C} : (X ⟶ Z) ≃ (Y ⟶ Z) where
 
 end Iso
 
-/-- `IsIso` typeclass expressing that a morphism is invertible. -/
+/-- The `IsIso` typeclass expresses that a morphism is invertible.
+
+Given a morphism `f` with `IsIso f`, one can view `f` as an isomorphism via `asIso f` and get
+the inverse using `inf v`. -/
```
PAST COMMENT (from reviewer):
You inferted two letters I'm avraid :)
```suggestion
the inverse using `inv f`. -/
```

--- candidate 5 (sim=0.681, past_pr=#36613, file=Mathlib/CategoryTheory/ConcreteCategory/Forget.lean) ---
PAST HUNK:
```
@@ -143,26 +148,7 @@ lemma ConcreteCategory.forget₂_comp_apply [HasForget₂ C D] {X Y Z : C}
   rw [Functor.map_comp, CategoryTheory.comp_apply]
 
 instance hom_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] :
-    IsIso (C := Type _) ⇑(ConcreteCategory.hom f) :=
+    IsIso (C := Type _) (TypeCat.ofHom ((ConcreteCategory.hom f))) :=
```
PAST COMMENT (from reviewer):
```suggestion
    IsIso (C := Type _) (TypeCat.ofHom (ConcreteCategory.hom f)) :=
```

--- candidate 6 (sim=0.680, past_pr=#8013, file=Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean) ---
PAST HUNK:
```
@@ -148,6 +171,431 @@ instance (priority := 100) hasCoreflexiveEqualizers_of_hasEqualizers [HasEqualiz
 
 end Limits
 
-open Limits
+end CategoryTheory
+
+namespace CategoryTheory
+
+universe v v₂ u u₂
+
+namespace Limits
+
+/-- The type of objects for the diagram indexing reflexive (co)equalizers -/
+inductive WalkingReflexivePair : Type where
+  | zero
+  | one
+  deriving DecidableEq, Inhabited
+
+open WalkingReflexivePair
+
+namespace WalkingReflexivePair
+
+/-- The type of morphisms for the diagram indexing reflexive (co)equalizers -/
+inductive Hom : (WalkingReflexivePair → WalkingReflexivePair → Type)
+  | left : Hom one zero
+  | right : Hom one zero
+  | reflexion : Hom zero one
+  | leftCompReflexion : Hom one one
+  | rightCompReflexion : Hom one one
+  | id (X : WalkingReflexivePair) : Hom X X
+  deriving DecidableEq
+
+attribute [-simp, nolint simpNF] Hom.id.sizeOf_spec
+attribute [-simp, nolint simpNF] Hom.leftCompReflexion.sizeOf_spec
+attribute [-simp, nolint simpNF] Hom.rightCompReflexion.sizeOf_spec
+
+/-- Composition of morphisms in the diagram indexing reflexive (co)equalizers -/
+def Hom.comp :
+    ∀ { X Y Z : WalkingReflexivePair } (_ : Hom X Y)
+      (_ : Hom Y Z), Hom X Z
+  | _, _, _, id _, h => h
+  | _, _, _, h, id _ => h
+  | _, _, _, reflexion, left => id zero
+  | _, _, _, reflexion, right => id zero
+  | _, _, _, reflexion, rightCompReflexion => reflexion
+  | _, _, _, reflexion, leftCompReflexion => reflexion
+  | _, _, _, left, reflexion => leftCompReflexion
+  | _, _, _, right, reflexion => rightCompReflexion
+  | _, _, _, 
... [truncated]
```
PAST COMMENT (from reviewer):
```suggestion
def inclusionWalkingReflexivePairEquivObjIso (G : ReflexiveCofork F) :
```

--- candidate 7 (sim=0.680, past_pr=#8013, file=Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean) ---
PAST HUNK:
```
@@ -148,6 +171,431 @@ instance (priority := 100) hasCoreflexiveEqualizers_of_hasEqualizers [HasEqualiz
 
 end Limits
 
-open Limits
+end CategoryTheory
+
+namespace CategoryTheory
+
+universe v v₂ u u₂
+
+namespace Limits
+
+/-- The type of objects for the diagram indexing reflexive (co)equalizers -/
+inductive WalkingReflexivePair : Type where
+  | zero
+  | one
+  deriving DecidableEq, Inhabited
+
+open WalkingReflexivePair
+
+namespace WalkingReflexivePair
+
+/-- The type of morphisms for the diagram indexing reflexive (co)equalizers -/
+inductive Hom : (WalkingReflexivePair → WalkingReflexivePair → Type)
+  | left : Hom one zero
+  | right : Hom one zero
+  | reflexion : Hom zero one
+  | leftCompReflexion : Hom one one
+  | rightCompReflexion : Hom one one
+  | id (X : WalkingReflexivePair) : Hom X X
+  deriving DecidableEq
+
+attribute [-simp, nolint simpNF] Hom.id.sizeOf_spec
+attribute [-simp, nolint simpNF] Hom.leftCompReflexion.sizeOf_spec
+attribute [-simp, nolint simpNF] Hom.rightCompReflexion.sizeOf_spec
+
+/-- Composition of morphisms in the diagram indexing reflexive (co)equalizers -/
+def Hom.comp :
+    ∀ { X Y Z : WalkingReflexivePair } (_ : Hom X Y)
+      (_ : Hom Y Z), Hom X Z
+  | _, _, _, id _, h => h
+  | _, _, _, h, id _ => h
+  | _, _, _, reflexion, left => id zero
+  | _, _, _, reflexion, right => id zero
+  | _, _, _, reflexion, rightCompReflexion => reflexion
+  | _, _, _, reflexion, leftCompReflexion => reflexion
+  | _, _, _, left, reflexion => leftCompReflexion
+  | _, _, _, right, reflexion => rightCompReflexion
+  | _, _, _, 
... [truncated]
```
PAST COMMENT (from reviewer):
Here, we need a specific docstring saying this is an isomorphism.

--- candidate 8 (sim=0.678, past_pr=#7845, file=Mathlib/CategoryTheory/Yoneda.lean) ---
PAST HUNK:
```
@@ -504,4 +504,5 @@ lemma isIso_of_yoneda_map_bijective {X Y : C} (f : X ⟶ Y)
   obtain ⟨g, hg : g ≫ f = 𝟙 Y⟩ := (hf Y).2 (𝟙 Y)
   exact ⟨g, (hf _).1 (by aesop_cat), hg⟩
 
+attribute [nolint simpNF] CategoryTheory.yonedaEquiv_yoneda_map
```
PAST COMMENT (from reviewer):
This can be deleted safely

--- candidate 9 (sim=0.678, past_pr=#35731, file=Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean) ---
PAST HUNK:
```
@@ -809,19 +809,11 @@ theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ 
 theorem eq_id_of_mono {x : SimplexCategory} (i : x ⟶ x) [Mono i] : i = 𝟙 _ := by
   suffices IsIso i by
     apply eq_id_of_isIso
-  apply isIso_of_bijective
-  dsimp
-  rw [Fintype.bijective_iff_injective_and_card i.toOrderHom, ← mono_iff_injective,
-    eq_self_iff_true, and_true]
-  infer_instance
+  exact (isIso_iff_of_mono i).mpr rfl
```
PAST COMMENT (from reviewer):
I think that works.

--- candidate 10 (sim=0.677, past_pr=#35731, file=Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean) ---
PAST HUNK:
```
@@ -809,19 +809,11 @@ theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ 
 theorem eq_id_of_mono {x : SimplexCategory} (i : x ⟶ x) [Mono i] : i = 𝟙 _ := by
   suffices IsIso i by
     apply eq_id_of_isIso
-  apply isIso_of_bijective
-  dsimp
-  rw [Fintype.bijective_iff_injective_and_card i.toOrderHom, ← mono_iff_injective,
-    eq_self_iff_true, and_true]
-  infer_instance
+  exact (isIso_iff_of_mono i).mpr rfl
```
PAST COMMENT (from reviewer):
Can this be merged with the `suffices` block? Same below.

--- candidate 11 (sim=0.677, past_pr=#33822, file=Mathlib/CategoryTheory/NatIso.lean) ---
PAST HUNK:
```
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.CategoryTheory.Functor.Category
 public import Mathlib.CategoryTheory.Iso
```
PAST COMMENT (from reviewer):
```suggestion
```
This import should now be redundant

--- candidate 12 (sim=0.676, past_pr=#35901, file=Mathlib/CategoryTheory/Sites/Hypercover/One.lean) ---
PAST HUNK:
```
@@ -608,6 +658,148 @@ def isoMk {S : C} {E F : PreOneHypercover S}
     intro i j k
     simpa using E.isoMk_aux s₀ s₁ h₁ k
 
+section
+
+variable {S : C} {E F : PreOneHypercover.{w} S} (e : E ≅ F)
+
+@[simp]
+lemma hom_inv_s₀_apply (i : E.I₀) : e.inv.s₀ (e.hom.s₀ i) = i :=
+  congr($(e.hom_inv_id).s₀ i)
+
+@[simp]
+lemma inv_hom_s₀_apply (i : F.I₀) : e.hom.s₀ (e.inv.s₀ i) = i :=
+  congr($(e.inv_hom_id).s₀ i)
+
+@[simp]
+lemma hom_inv_s₁_apply {i j : E.I₀} (k : E.I₁ i j) :
+    e.inv.s₁ (e.hom.s₁ k) = E.congrIndexOneOfEq (by simp) (by simp) k := by
+  obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.hom_inv_id
+  simpa using hs₁ i j k
+
+@[simp]
+lemma inv_hom_s₁_apply {i j : F.I₀} (k : F.I₁ i j) :
+    e.hom.s₁ (e.inv.s₁ k) = F.congrIndexOneOfEq (by simp) (by simp) k := by
+  obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.inv_hom_id
+  simpa using hs₁ i j k
+
+@[reassoc (attr := simp)]
+lemma hom_inv_h₀ (i : E.I₀) : e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom (by simp) := by
+  obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.hom_inv_id
+  simpa using hh i
+
+@[reassoc (attr := simp)]
+lemma inv_hom_h₀ (i : F.I₀) : e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom (by simp) := by
+  obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.inv_hom_id
+  simpa using hh i
+
+@[reassoc (attr := simp)]
+lemma hom_inv_h₁ {i j : E.I₀} (k : E.I₁ i j) :
+    e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) =
+      (E.congrIndexOneOfEqIso (hom_inv_s₀_apply e i).symm (hom_inv_s₀_apply e j).symm k).inv ≫
+      eqToHom (by congr 1; simp) := by
+  obtain ⟨hs, _, _, hh⟩ := Hom.
... [truncated]
```
PAST COMMENT (from reviewer):
Could you try to show the triangle identity?

--- candidate 13 (sim=0.675, past_pr=#32578, file=Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean) ---
PAST HUNK:
```
@@ -148,6 +148,20 @@ lemma Hom.id_eq_id (X : WalkingMulticospan J) :
 lemma Hom.comp_eq_comp {X Y Z : WalkingMulticospan J}
     (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.comp f g = f ≫ g := rfl
 
+/-- Construct a natural isomorphism between functors out of a walking multicospan from its
+components. -/
+@[simps!]
+def functorExt {C : Type*} [Category C] {F G : WalkingMulticospan J ⥤ C}
+    (left : ∀ i, F.obj (.left i) ≅ G.obj (.left i))
+    (right : ∀ i, F.obj (.right i) ≅ G.obj (.right i))
+    (wl : ∀ i, F.map (WalkingMulticospan.Hom.fst i) ≫ (right i).hom =
+      (left _).hom ≫ G.map (WalkingMulticospan.Hom.fst i))
+    (wr : ∀ i, F.map (WalkingMulticospan.Hom.snd i) ≫ (right i).hom =
+      (left _).hom ≫ G.map (WalkingMulticospan.Hom.snd i)) :
```
PAST COMMENT (from reviewer):
We could add a default tactic `by cat_disch` here (and below)?

--- candidate 14 (sim=0.675, past_pr=#16783, file=Mathlib/CategoryTheory/Category/Quiv.lean) ---
PAST HUNK:
```
@@ -82,6 +82,38 @@ end Cat
 
 namespace Quiv
 
+def isoOfEquiv {V W : Type u } [Quiver.{v + 1, u} V] [Quiver.{v + 1, u} W]
```
PAST COMMENT (from reviewer):
I believe it would much more convenient to develop a suitable API (kind of similar to `eqToHom`) for quivers:
```lean
section

variable {V : Type*} [Quiver V]

def _root_.Quiver.homOfEq {X Y : V} (f : X ⟶ Y) {X' Y' : V}
    (hX : X = X') (hY : Y = Y') : X' ⟶ Y' := by
  subst hX hY
  exact f

@[simp]
lemma _root_.Quiver.homOfEq_trans
    {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y')
    {X'' Y'' : V} (hX' : X' = X'') (hY' : Y' = Y'') :
    Quiver.homOfEq (Quiver.homOfEq f hX hY) hX' hY' =
      Quiver.homOfEq f (hX.trans hX') (hY.trans hY') := by
  subst hX hY hX' hY'
  rfl

lemma _root_.Quiver.homOfEq_injective {X X' Y Y' : V} (hX : X = X') (hY : Y = Y')
    {f g : X ⟶ Y} (h : Quiver.homOfEq f hX hY = Quiver.homOfEq g hX hY) : f = g := by
... [truncated]

--- candidate 15 (sim=0.675, past_pr=#36613, file=Mathlib/CategoryTheory/Yoneda.lean) ---
PAST HUNK:
```
@@ -1080,43 +1125,42 @@ lemma isIso_iff_coyoneda_map_bijective {X Y : C} (f : X ⟶ Y) :
     IsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x)) := by
   refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_coyoneda_map_bijective f hf⟩
   intro T
-  rw [← isIso_iff_bijective]
+  rw [bijective_iff_isIso_ofHom]
   exact inferInstanceAs (IsIso ((coyoneda.map f.op).app _))
 
 lemma isIso_iff_isIso_coyoneda_map {X Y : C} (f : X ⟶ Y) :
     IsIso f ↔ ∀ c : C, IsIso ((coyoneda.map f.op).app c) := by
   rw [isIso_iff_coyoneda_map_bijective]
-  exact forall_congr' fun _ ↦ (isIso_iff_bijective _).symm
+  exact forall_congr' fun _ ↦ bijective_iff_isIso_ofHom _
 
 /-- Coyoneda's lemma as a bijection `(uliftCoyoneda.{w}.obj X ⟶ F) ≃ F.obj (op X)`
 for any presheaf of type `F : Cᵒᵖ ⥤ Type (max w v₁)` for some
 auxiliary universe `w`. -/
-@[simps! -isSimp]
+@[simps! -isSimp apply symm_apply_app]
 def uliftCoyonedaEquiv {X : Cᵒᵖ} {F : C ⥤ Type (max w v₁)} :
     (uliftCoyoneda.{w}.obj X ⟶ F) ≃ F.obj X.unop where
   toFun τ := τ.app X.unop (ULift.up (𝟙 _))
-  invFun x := { app Y y := F.map y.down x }
+  invFun x := { app Y := TypeCat.ofHom fun y ↦ F.map y.down x }
   left_inv τ := by
-    ext Y ⟨y⟩
-    simp [uliftYoneda, ← FunctorToTypes.naturality]
+    ext Y ⟨x⟩
+    simp [← comp_apply, ← τ.naturality]
   right_inv x := by simp
 
 attribute [simp] uliftCoyonedaEquiv_symm_apply_app
 
 set_option backward.isDefEq.respectTransparency false in
-lemma uliftCoyonedaEquiv_naturality {X Y : C} {F : C ⥤ Type max w v₁}
+lemma uliftCoyonedaEquiv_naturality {X Y : C} {F : C ⥤ Type (max w v₁)}
```
PAST COMMENT (from reviewer):
```suggestion
lemma uliftCoyonedaEquiv_naturality {X Y : C} {F : C ⥤ Type (max w v₁)}
```
Just a general comment: I think it would have been fine to leave unparenthesized the `max u v`, but I am too lazy to go and find them all and make suggestions for all of them. Ultimately it’s a matter of taste I guess.

--- candidate 16 (sim=0.673, past_pr=#28234, file=Mathlib/CategoryTheory/Groupoid.lean) ---
PAST HUNK:
```
@@ -95,7 +95,7 @@ variable (X Y)
 @[simps!]
 def Groupoid.isoEquivHom : (X ≅ Y) ≃ (X ⟶ Y) where
   toFun := Iso.hom
-  invFun f := ⟨f, Groupoid.inv f, (by simp), (by simp)⟩
+  invFun f := ⟨f, Groupoid.inv f, by simp, by simp⟩
```
PAST COMMENT (from reviewer):
Untested:
```suggestion
  invFun f := { hom := f, inv := Groupoid.inv f }
```

--- candidate 17 (sim=0.671, past_pr=#28395, file=Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean) ---
PAST HUNK:
```
@@ -266,6 +259,59 @@ lemma range_δ {n : ℕ} (i : Fin (n + 2)) :
   rw [Subcomplex.range_eq_ofSimplex]
   exact ofSimplex_yonedaEquiv_δ i
 
+/-- The standard simplex identifies to the nerve to the preordered type
+`ULift (Fin (n + 1))`. -/
+def isoNerve (n : ℕ) :
+    (Δ[n] : SSet.{u}) ≅ nerve (ULift.{u} (Fin (n + 1))) :=
+  NatIso.ofComponents (fun d ↦ Equiv.toIso (objEquiv.trans
+    { toFun f := (ULift.orderIso.symm.monotone.comp f.toOrderHom.monotone).functor
+      invFun f :=
+        SimplexCategory.Hom.mk
+          (ULift.orderIso.toOrderEmbedding.toOrderHom.comp f.toOrderHom)
+      left_inv _ := by aesop
+      right_inv _ := by rfl }))
```
PAST COMMENT (from reviewer):
```suggestion
      left_inv _ := by aesop }))
```
auto-param finds `right_inv`. 

--- candidate 18 (sim=0.669, past_pr=#25780, file=Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean) ---
PAST HUNK:
```
@@ -314,6 +315,15 @@ def nonDegenerateEquiv {n d : ℕ} :
 
 end stdSimplex
 
+/-- The n-simplex is isomorphic to the nerve of the ordinal category `Fin (n + 1)`. -/
+def simplexIsNerve (n : ℕ) : Δ[n] ≅ nerve (Fin (n + 1)) := NatIso.ofComponents <| fun n ↦
+    Equiv.toIso <| stdSimplex.objEquiv.trans SimplexCategory.homEquivFunctor
```
PAST COMMENT (from reviewer):
As I encountered similar definitions in my formalization of the homotopy theory of simplicial sets, I would suggest using the following two definitions which also uses your definition `homEquivFunctor`:
```lean
def CategoryTheory.nerve.representableBy
    {n : ℕ} (α : Type u) [Preorder α] (e : α ≃o Fin (n + 1)) :
    (nerve α).RepresentableBy ⦋n⦌ where
  homEquiv := SimplexCategory.homEquivFunctor.trans
    { toFun F := F ⋙ e.symm.monotone.functor
      invFun F := F ⋙ e.monotone.functor
      left_inv F := Functor.ext (fun x ↦ by simp)
      right_inv F := Functor.ext (fun x ↦ by simp) }
  homEquiv_comp _ _ := rfl

/-- If a simplicial set `X` is representable by `⦋m⦌` for some `m : ℕ`, then this is the
corresponding isomorphism `Δ[m] ≅ X`. -/
def SSet.stdSimplex.isoOfRepres
... [truncated]

--- candidate 19 (sim=0.669, past_pr=#34008, file=Mathlib/CategoryTheory/Iso.lean) ---
PAST HUNK:
```
@@ -178,272 +191,219 @@ theorem symm_self_id_assoc (α : X ≅ Y) (β : Y ≅ Z) : α.symm ≪≫ α ≪
 theorem self_symm_id_assoc (α : X ≅ Y) (β : X ≅ Z) : α ≪≫ α.symm ≪≫ β = β := by
   rw [← trans_assoc, self_symm_id, refl_trans]
 
+@[to_dual none]
 theorem inv_comp_eq (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : α.inv ≫ f = g ↔ f = α.hom ≫ g :=
   ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩
 
+@[to_dual none]
 theorem eq_inv_comp (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : g = α.inv ≫ f ↔ α.hom ≫ g = f :=
   (inv_comp_eq α.symm).symm
 
+@[to_dual none]
 theorem comp_inv_eq (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ α.inv = g ↔ f = g ≫ α.hom :=
   ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩
 
+@[to_dual none]
 theorem eq_comp_inv (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : g = f ≫ α.inv ↔ g ≫ α.hom = f :=
   (comp_inv_eq α.symm).symm
 
+@[to_dual none]
 theorem inv_eq_inv (f g : X ≅ Y) : f.inv = g.inv ↔ f.hom = g.hom :=
   have : ∀ {X Y : C} (f g : X ≅ Y), f.hom = g.hom → f.inv = g.inv := fun f g h => by rw [ext h]
   ⟨this f.symm g.symm, this f g⟩
 
+@[to_dual comp_inv_eq_id]
 theorem hom_comp_eq_id (α : X ≅ Y) {f : Y ⟶ X} : α.hom ≫ f = 𝟙 X ↔ f = α.inv := by
   rw [← eq_inv_comp, comp_id]
 
+@[to_dual inv_comp_eq_id]
 theorem comp_hom_eq_id (α : X ≅ Y) {f : Y ⟶ X} : f ≫ α.hom = 𝟙 Y ↔ f = α.inv := by
   rw [← eq_comp_inv, id_comp]
 
-theorem inv_comp_eq_id (α : X ≅ Y) {f : X ⟶ Y} : α.inv ≫ f = 𝟙 Y ↔ f = α.hom :=
-  hom_comp_eq_id α.symm
-
-theorem comp_inv_eq_id (α : X ≅ Y) {f : X ⟶ Y} : f ≫ α.inv = 𝟙 X ↔ f = α.hom :=
-  comp_hom_eq_id α.symm
-
+@[to_dual inv_eq_hom]
 theorem 
... [truncated]
```
PAST COMMENT (from reviewer):
is there a way to get `to_dual` to match both the signature and variable names? Here, 
`to_dual (reorder := X Y) inv_eq_of_inv_hom_id` seems to give the exact signature of the previous declaration, but the named parameters remain swapped?

(There are probably no places in the library where we call these by being explicit with explicit naming of `X` and `Y` rather than on `f` and `g` for this def, but this is technically a breaking change if some are calling it by naming parameters)

This also applies to a bunch of other declarations here, so I’ll just suggest the reorderings

--- candidate 20 (sim=0.669, past_pr=#34008, file=Mathlib/CategoryTheory/Iso.lean) ---
PAST HUNK:
```
@@ -178,272 +191,219 @@ theorem symm_self_id_assoc (α : X ≅ Y) (β : Y ≅ Z) : α.symm ≪≫ α ≪
 theorem self_symm_id_assoc (α : X ≅ Y) (β : X ≅ Z) : α ≪≫ α.symm ≪≫ β = β := by
   rw [← trans_assoc, self_symm_id, refl_trans]
 
+@[to_dual none]
 theorem inv_comp_eq (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : α.inv ≫ f = g ↔ f = α.hom ≫ g :=
   ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩
 
+@[to_dual none]
 theorem eq_inv_comp (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : g = α.inv ≫ f ↔ α.hom ≫ g = f :=
   (inv_comp_eq α.symm).symm
 
+@[to_dual none]
 theorem comp_inv_eq (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ α.inv = g ↔ f = g ≫ α.hom :=
   ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩
 
+@[to_dual none]
 theorem eq_comp_inv (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : g = f ≫ α.inv ↔ g ≫ α.hom = f :=
   (comp_inv_eq α.symm).symm
 
+@[to_dual none]
 theorem inv_eq_inv (f g : X ≅ Y) : f.inv = g.inv ↔ f.hom = g.hom :=
   have : ∀ {X Y : C} (f g : X ≅ Y), f.hom = g.hom → f.inv = g.inv := fun f g h => by rw [ext h]
   ⟨this f.symm g.symm, this f g⟩
 
+@[to_dual comp_inv_eq_id]
 theorem hom_comp_eq_id (α : X ≅ Y) {f : Y ⟶ X} : α.hom ≫ f = 𝟙 X ↔ f = α.inv := by
   rw [← eq_inv_comp, comp_id]
 
+@[to_dual inv_comp_eq_id]
 theorem comp_hom_eq_id (α : X ≅ Y) {f : Y ⟶ X} : f ≫ α.hom = 𝟙 Y ↔ f = α.inv := by
   rw [← eq_comp_inv, id_comp]
 
-theorem inv_comp_eq_id (α : X ≅ Y) {f : X ⟶ Y} : α.inv ≫ f = 𝟙 Y ↔ f = α.hom :=
-  hom_comp_eq_id α.symm
-
-theorem comp_inv_eq_id (α : X ≅ Y) {f : X ⟶ Y} : f ≫ α.inv = 𝟙 X ↔ f = α.hom :=
-  comp_hom_eq_id α.symm
-
+@[to_dual inv_eq_hom]
 theorem 
... [truncated]
```
PAST COMMENT (from reviewer):
```suggestion
@[aesop apply safe (rule_sets := [CategoryTheory]), to_dual (reorder := X Y) eq_inv_of_inv_hom_id]
```


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

[ASSISTANT]
----------------------------------------------------------------------------------------------------
{
  "summary": "No past reviewer feedback directly applies to this new hunk.",
  "confidence": "none",
  "strong_matches": [],
  "weak_observations": []
}