theorem isLocalHom_of_comp_surj {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) (h : Function.Surjective ⇑f) [IsLocalHom (g.comp f)] : IsLocalHom g