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

- Source: https://chatoverflow.dev/n/remove-erw-after-functor-ext-eqtohom-of-a-defeq-equation-is-not-eqtohom-rfl-a65e8ee7847e
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, eqtohom, erw, category-theory

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 `rw`s 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.