chore(CategoryTheory/Sites/MayerVietorisSquare): remove an erw (#38679)

- simplifies the Yoneda/sheafification naturality check to a single `simp [Adjunction.homEquiv, yonedaEquiv_naturality]`

Extracted from #38415

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

@@ -59,8 +59,7 @@ namespace CategoryTheory
 
 open Limits Opposite
 
-variable {C : Type u} [Category.{v} C]
-  {J : GrothendieckTopology C}
+variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
 
 set_option backward.isDefEq.respectTransparency false in
 lemma Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff
@@ -75,10 +74,7 @@ lemma Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff
     (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv) ?_ ?_ ?_ ?_
   all_goals
     ext x
-    dsimp
-    rw [yonedaEquiv_naturality]
-    erw [Adjunction.homEquiv_naturality_left]
-    rfl
+    simp [Adjunction.homEquiv, yonedaEquiv_naturality]
 
 namespace GrothendieckTopology