refactor: remove simp attribute from yonedaEquiv_apply (#10109)

leanprover-community · Jan 30, 2024 · 132d4e4 · 132d4e4
1 parent 38cd727
commit 132d4e4
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean b/Mathlib/CategoryTheory/Sites/IsSheafFor.lean
@@ -488,7 +488,7 @@ theorem extension_iff_amalgamation {P : Cᵒᵖ ⥤ Type v₁} (x : S.functor
   · rintro rfl Y f hf
     rw [yonedaEquiv_naturality]
     dsimp
-    simp
+    simp [yonedaEquiv_apply]
   -- See note [dsimp, simp].
   · intro h
     ext Y ⟨f, hf⟩

diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
@@ -400,7 +400,6 @@ def yonedaEquiv {X : C} {F : Cᵒᵖ ⥤ Type v₁} : (yoneda.obj X ⟶ F) ≃ F
   (yonedaSections X F).toEquiv.trans Equiv.ulift
 #align category_theory.yoneda_equiv CategoryTheory.yonedaEquiv
 
-@[simp]
 theorem yonedaEquiv_apply {X : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F) :
     yonedaEquiv f = f.app (op X) (𝟙 X) :=
   rfl