∀ {R : Type u_1} [inst : CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {M : Type u_18}
  {N : Type u_19} {P : Type u_20} {Q : Type u_21} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
  (g : P →ₛₗ[σ₃₄] Q), Function.Injective ⇑f → Function.Injective ⇑g → Function.Injective ⇑(f.compr₂ₛₗ g)