diff --git a/Mathlib/Algebra/Category/Ring/Adjunctions.lean b/Mathlib/Algebra/Category/Ring/Adjunctions.lean
index 57adf439204b1..508b75ef50497 100644
--- a/Mathlib/Algebra/Category/Ring/Adjunctions.lean
+++ b/Mathlib/Algebra/Category/Ring/Adjunctions.lean
@@ -45,7 +45,7 @@ theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = MvPolynomial α 
 #align CommRing.free_obj_coe CommRingCat.free_obj_coe
 
 -- Porting note: `simpNF` should not trigger on `rfl` lemmas.
--- see https://github.com/leanprover-community/mathlib4/issues/5081
+-- see https://github.com/leanprover/std4/issues/86
 @[simp, nolint simpNF]
 theorem free_map_coe {α β : Type u} {f : α → β} : ⇑(free.map f) = ⇑(rename f) :=
   rfl
diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean
index 1f8a7da72425d..384bb446ca68f 100644
--- a/Mathlib/Algebra/Category/Ring/Basic.lean
+++ b/Mathlib/Algebra/Category/Ring/Basic.lean
@@ -135,7 +135,7 @@ set_option linter.uppercaseLean3 false in
 #align SemiRing.of_hom SemiRingCat.ofHom
 
 -- Porting note: `simpNF` should not trigger on `rfl` lemmas.
--- see https://github.com/leanprover-community/mathlib4/issues/5081
+-- see https://github.com/leanprover/std4/issues/86
 @[simp, nolint simpNF]
 theorem ofHom_apply {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) :
     ofHom f x = f x :=
diff --git a/Mathlib/Topology/Category/UniformSpace.lean b/Mathlib/Topology/Category/UniformSpace.lean
index 12ddaea984c9d..004ed91641418 100644
--- a/Mathlib/Topology/Category/UniformSpace.lean
+++ b/Mathlib/Topology/Category/UniformSpace.lean
@@ -66,14 +66,14 @@ instance (X Y : UniformSpaceCat) : CoeFun (X ⟶ Y) fun _ => X → Y :=
   ⟨(forget UniformSpaceCat).map⟩
 
 -- Porting note: `simpNF` should not trigger on `rfl` lemmas.
--- see https://github.com/leanprover-community/mathlib4/issues/5081
+-- see https://github.com/leanprover/std4/issues/86
 @[simp, nolint simpNF]
 theorem coe_comp {X Y Z : UniformSpaceCat} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : X → Z) = g ∘ f :=
   rfl
 #align UniformSpace.coe_comp UniformSpaceCat.coe_comp
 
 -- Porting note: `simpNF` should not trigger on `rfl` lemmas.
--- see https://github.com/leanprover-community/mathlib4/issues/5081
+-- see https://github.com/leanprover/std4/issues/86
 @[simp, nolint simpNF]
 theorem coe_id (X : UniformSpaceCat) : (𝟙 X : X → X) = id :=
   rfl