diff --git a/Mathlib/CategoryTheory/Functor/Flat.lean b/Mathlib/CategoryTheory/Functor/Flat.lean
index 33280fbd6fd05b..b9a6af7b584ced 100644
--- a/Mathlib/CategoryTheory/Functor/Flat.lean
+++ b/Mathlib/CategoryTheory/Functor/Flat.lean
@@ -184,7 +184,7 @@ theorem fac (x : J) : lift F hc s ≫ (F.mapCone c).π.app x = s.π.app x := by
   simp [lift, ← Functor.map_comp]
 #align category_theory.preserves_finite_limits_of_flat.fac CategoryTheory.PreservesFiniteLimitsOfFlat.fac
 
-attribute [local simp] eqToHom_map
+-- attribute [local simp] eqToHom_map
 
 theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
     (f₁ f₂ : s.pt ⟶ F.obj c.pt) (h₁ : ∀ j : J, f₁ ≫ (F.mapCone c).π.app j = s.π.app j)
@@ -208,7 +208,7 @@ theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
     intro j
     injection c₀.π.naturality (BiconeHom.left j) with _ e₁
     injection c₀.π.naturality (BiconeHom.right j) with _ e₂
-    simpa using e₁.symm.trans e₂
+    convert e₁.symm.trans e₂ <;> simp
   have : c.extend g₁.right = c.extend g₂.right := by
     unfold Cone.extend
     congr 1