-- Mathlib.RingTheory.IsTensorProduct
/-- This is the canonical isomorphism `(M₁ ⊗[R] M₂) ⊗[S] M₃ ≃ₗ[T] M₁ ⊗[R] (M₂ ⊗[S] M₃)`.
We state this for a general `M₁₂ = M₁ ⊗[R] M₂` and `M₂₃ = M₂ ⊗[R] M₃`.
For the version where `R` and `S` are flipped, see `TensorProduct.AlgebraTensorModule.assoc`.
 -/
IsTensorProduct.assoc : {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₂] →
                                    [inst_11 : 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₁₂] →
                                                [inst_17 : 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₁₂] →
                                                                      [inst_27 : IsScalarTower R T M₁₂] →
                                                                        (f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂) →
                                                                          IsTensorProduct
                                                                              (LinearMap.restrictScalars₁₂ R R f) →
                                                                            (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) →
                                                                              IsTensorProduct g →
                                                                                TensorProduct S M₁₂ M₃ ≃ₗ[T]
                                                                                  TensorProduct R M₁ M₂₃