no goals
M : Type u_3
N : Type u_1
P : Type u_2
σ : Type ?u.60762
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
g : N →ₙ* P
f : M →ₙ* N
⊢ map g (srange f) = srange (comp g f)
simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f