-- Mathlib.RingTheory.IsTensorProduct
/-- Variant of `IsTensorProduct.assoc` taking an `R`-bilinear map `f` and proofs that
`f` is `T` linear in the first and `S`-linear in the second argument.  -/
IsTensorProduct.assocOfMapSMul : {R : Type u_9} →
  {S : Type u_10} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {M₁ : Type u_11} →
            {M₂ : Type u_12} →
              {M₃ : Type u_13} →
                {M₁₂ : Type u_14} →
                  {M₂₃ : Type u_15} →
                    [inst_3 : AddCommMonoid M₁] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : AddCommMonoid M₃] →
                          [inst_6 : AddCommMonoid M₁₂] →
                            [inst_7 : AddCommMonoid M₂₃] →
                              [inst_8 : Module R M₁] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : Module S M₂] →
                                    [IsScalarTower R S M₂] →
                                      [inst_12 : Module R M₃] →
                                        [inst_13 : Module S M₃] →
                                          [IsScalarTower R S M₃] →
                                            [inst_15 : Module R M₁₂] →
                                              [inst_16 : Module S M₁₂] →
                                                [IsScalarTower R S M₁₂] →
                                                  [inst_18 : Module R M₂₃] →
                                                    [inst_19 : Module S M₂₃] →
                                                      [IsScalarTower R S M₂₃] →
                                                        {T : Type u_16} →
                                                          [inst_21 : CommSemiring T] →
                                                            [inst_22 : Algebra R T] →
                                                              [inst_23 : Module T M₁] →
                                                                [inst_24 : IsScalarTower R T M₁] →
                                                                  [inst_25 : Module T M₁₂] →
                                                                    [inst_26 : SMulCommClass S T M₁₂] →
                                                                      [IsScalarTower R T M₁₂] →
                                                                        (f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂) →
                                                                          IsTensorProduct f →
                                                                            (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) →
                                                                              IsTensorProduct g →
                                                                                (∀ (t : T) (x : M₁) (y : M₂),
                                                                                    (f (t • x)) y = t • (f x) y) →
                                                                                  (∀ (s : S) (x : M₁) (y : M₂),
                                                                                      (f x) (s • y) = s • (f x) y) →
                                                                                    TensorProduct S M₁₂ M₃ ≃ₗ[T]
                                                                                      TensorProduct R M₁ M₂₃