{R : Type u_14} →
  {R₂ : Type u_15} →
    {R₃ : Type u_16} →
      {R₄ : Type u_17} →
        {R₅ : Type u_18} →
          {M : Type u_19} →
            {N : Type u_20} →
              {P : Type u_21} →
                {Q : Type u_22} →
                  [inst : Semiring R] →
                    [inst_1 : Semiring R₂] →
                      [inst_2 : Semiring R₃] →
                        [inst_3 : Semiring R₄] →
                          [inst_4 : Semiring R₅] →
                            {σ₂₃ : R₂ →+* R₃} →
                              {σ₄₂ : R₄ →+* R₂} →
                                {σ₄₃ : R₄ →+* R₃} →
                                  [inst_5 : AddCommMonoid M] →
                                    [inst_6 : AddCommMonoid N] →
                                      [inst_7 : AddCommMonoid P] →
                                        [inst_8 : AddCommMonoid Q] →
                                          [inst_9 : Module R M] →
                                            [inst_10 : Module R₂ N] →
                                              [inst_11 : Module R₃ P] →
                                                [inst_12 : Module R₄ Q] →
                                                  [inst_13 : Module R₅ P] →
                                                    [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] →
                                                      [inst_15 : SMulCommClass R₃ R₅ P] →
                                                        {σ₁₅ : R →+* R₅} →
                                                          (M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) →
                                                            (Q →ₛₗ[σ₄₂] N) → M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P