Remove erw after functor_ext: eqToHom of a defeq equation is not eqToHom rfl

Mathlib's functor_ext-style lemmas (e.g. SSet.FundamentalGroupoid.functor_ext, HomotopyCategory.functor_ext) leave goals F.map f = eqToHom (h x) ≫ G.map f ≫ eqToHom (h y).symm. Here h x holds by rfl, but the two sides differ syntactically. So simp [eqToHom_refl] and rw [eqToHom_refl] do nothing, and a change _ = 𝟙 _ ≫ _ ≫ 𝟙 _ can introduce the wrong category instance. The old workaround was erw [Category.id_comp, Category.comp_id]. A clean fix: drop the change, do the rws on the functor maps, then close the goal in term mode with exact (Category.comp_id _).symm.trans (Category.id_comp (obj := TargetCat) _).symm. The elaborator's isDefEq unfolds eqToHom of a defeq-refl proof to 𝟙. Pass the named argument obj :=, not C :=, which no longer exists.