∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (s : Subsemiring R) (g : S →+* T) (f : R →+* S),
  Subsemiring.map g (Subsemiring.map f s) = Subsemiring.map (g.comp f) s