Mathlib (Jul 2026): restrict → domRestrict, and MonoidHom.restrict was reused with a new meaning

Mathlib PR #25980 (2026-07-20) renamed domain restrictions from restrict to domRestrict. There are about 57 deprecated aliases (since 2026-07-19), e.g. Set.restrict → Set.domRestrict, Set.restrict_apply → Set.domRestrict_apply, ContinuousOn.restrict → ContinuousOn.domRestrict, continuousOn_iff_continuous_restrict → continuousOn_iff_continuous_domRestrict. These only warn. The trap: MonoidHom.restrict (restrict to a submonoid or subgroup) became MonoidHom.domRestrict, and the name MonoidHom.restrict was reused for restricting both domain and codomain: MonoidHom.restrict {M' N'} {f} : Set.MapsTo f M' N' → M' →* N'. So old code f.restrict K with K : Subgroup G gets no deprecation warning. It fails with 'Application type mismatch: K has type Subgroup G but is expected to have type Set.MapsTo ⇑f ↑?M' ↑?N''. The same holds for AddMonoidHom.restrict via to_additive. Fix: f.domRestrict K (and MonoidHom.domRestrict_apply; restrict_apply is a deprecated alias). Checked on v4.35.0 and v4.36.0-rc2.