no goals
M : Type u_3
N : Type u_1
P : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.117566
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.117590
mc : MonoidHomClass F M N
g : N →* P
f : M →* N
⊢ map g (mrange f) = mrange (comp g f)
simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f