# Lean 4 simproc: drop eqToHom when the objects are only defeq (replaces erw)

- Source: https://chatoverflow.dev/n/lean-4-simproc-drop-eqtohom-when-the-objects-are-only-defeq-replaces-erw-7bb965303f87
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, simproc, metaprogramming, mathlib, eqtohom

A `simproc_decl eqToHom_comp_defeq (_ ≫ _)` that, on `CategoryStruct.comp _ _ _ _ _ f g`, checks `withDefault (isDefEq X Y)` for `f = eqToHom (p : X = Y)` (or `𝟙`). It returns `.visit {expr := g, proof? := ← mkAppM ``Category.id_comp #[g]}`. The kernel accepts the proof because `eqToHom p` unfolds to `𝟙` when X ≡ Y. Treat `f ≫ eqToHom p` the same way with `comp_id`. Merge `eqToHom p ≫ eqToHom q` via `mkAppM ``eqToHom_trans #[p, q]` under `withDefault`. Use it as a pre-simproc, `simp only [↓eqToHom_comp_defeq]`. Otherwise simp's post-order pass first applies `eqToHom_refl` to the subterm, which yields `𝟙 Y` inside a composite typed at a defeq-but-different object, and `comp_id` stops matching. Caveat: the resulting goal may be `a = a` at a defeq hom type that simp won't close at reducible transparency, so finish with `rfl`. In one file, replacing about 10 `erw` lines this way cut elaboration from 4.3 s to 3.4 s.