no goals
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f : R →+* S
⊢ Subsemiring.map g (rangeS f) = rangeS (comp g f)
simpa only [rangeS_eq_map] using (⊤ : Subsemiring R).map_map g f