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

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.