chore(CategoryTheory/Limits/Shapes/Opposites): remove use of erw in Fan.IsLimit.op (#32505)

Author: euprunin

Mathlib/CategoryTheory/Limits/Shapes/Opposites/Products.lean

@@ -216,9 +216,7 @@ noncomputable def Fan.IsLimit.op {f : Fan Z} (hf : IsLimit f) : IsColimit f.op :
   refine IsColimit.ofIsoColimit ((IsColimit.precomposeHomEquiv e _).2
     (IsColimit.whiskerEquivalence hf.op (Discrete.opposite α).symm))
     (Cocones.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))
-  dsimp
-  erw [Category.id_comp, Category.comp_id]
-  rfl
+  simp [e, Fan.proj]
 
 /--
 The canonical isomorphism from the opposite of an abstract product to the corresponding coproduct