no goals
M : Type u_1
N : Type u_2
P : Type ?u.123584
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.123605
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.123629
mc : MonoidHomClass F M N
f : M →* N
⊢ mrange (restrict f S) = map f S
simp [SetLike.ext_iff]