∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {P₂ : Type u_17} {P₃ : Type u_18} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid P₂]
  [inst_6 : AddCommMonoid P₃] [inst_7 : Module R M] [inst_8 : Module R N] [inst_9 : Module R₂ P₂]
  [inst_10 : Module R₃ P₃] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} [inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (h : P₂ →ₛₗ[σ₂₃] P₃), TensorProduct.lift (f'.compr₂ₛₗ h) = h ∘ₛₗ TensorProduct.lift f'