chore(CategoryTheory): remove use of erw in ι_gluedIso_hom (#32523)

Author: euprunin

Mathlib/CategoryTheory/GlueData.lean

@@ -298,11 +298,8 @@ def gluedIso : F.obj D.glued ≅ (D.mapGlueData F).glued :=
 
 @[reassoc (attr := simp)]
 theorem ι_gluedIso_hom (i : D.J) : F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i := by
-  haveI : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance
   erw [ι_preservesColimitIso_hom_assoc]
-  rw [HasColimit.isoOfNatIso_ι_hom]
-  erw [Category.id_comp]
-  rfl
+  simp [GlueData.ι]
 
 @[reassoc (attr := simp)]
 theorem ι_gluedIso_inv (i : D.J) : (D.mapGlueData F).ι i ≫ (D.gluedIso F).inv = F.map (D.ι i) := by