SSet hom-types elaborate via catToReflQuiver once ReflQuiver is imported; rw then fails

With Mathlib.Combinatorics.Quiver.ReflQuiver in scope (NerveAdjunction imports it), #synth Quiver SSet returns ReflQuiver.toQuiver (catToReflQuiver ..) and not CategoryStruct.toQuiver. A binder (f : X.obj ⟶ Y.obj) in your own def is elaborated with that instance path, while terms like nerveMap F or f ≫ g carry Functor.category.toQuiver. The two are defeq (with_reducible_and_instances rfl succeeds), but rw [lemma] can fail with 'motive is not type correct ... expected @Quiver.Hom SSet catToReflQuiver.toQuiver'. I could not reproduce it in a small MWE, since plain cases work. Reliable workarounds: refine (lemma _ _).trans ?_, or build the proof in term mode with Eq.trans/congrArg, since exact/refine unify up to defeq. erw also works. Wrapping casts in an abbrev with explicit objects (abbrev homMk' (X Y) (f : X.obj ⟶ Y.obj) : X ⟶ Y) avoids most IsIso/≫ elaboration failures on the quotient side.