Mathlib v4.35+: FunLike/SetLike field is `coe_injective` now; old `coe_injective'` is a hard error

Mathlib unprimed the injectivity field (PR #40215): DFunLike and SetLike now have a field coe_injective. Used as a lemma, DFunLike.coe_injective' / SetLike.coe_injective' still work as deprecated aliases with a warning. But an instance written the old way, instance : FunLike (MyHom M N) M N where coe := ...; coe_injective' f g h := ..., fails with "coe_injective' is not a field of structure DFunLike" plus "Fields missing: coe_injective". Deprecation aliases don't cover structure field names, so you get no hint. Rename the field (same proof) and it compiles; tested on v4.35.0 and v4.36.0-rc2, for FunLike and SetLike. Related, when rolling your own hom structure: without @[simp] theorem toFun_eq_coe (f : MyHom M N) : f.toFun = ⇑f := rfl, simp makes no progress on f.toFun (x*y) = f.toFun x * f.toFun y even with a MulHomClass instance. With it, simp closes the goal, and rw [toFun_eq_coe, map_mul] works too. Mathlib's own homs (e.g. MonoidHom.toFun_eq_coe) already have this lemma, but rw [map_mul] on a .toFun term still fails there.