∀ {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₃] [inst_14 : 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₂₃]
  [inst_20 : IsScalarTower R S M₂₃] (f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂)
  (hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (hg : IsTensorProduct g),
  IsTensorProduct.assocAux✝ f hf g hg =
    (((((((TensorProduct.congr (LinearEquiv.refl R M₁) (LinearEquiv.restrictScalars R hg.equiv.symm)).trans
                            (TensorProduct.comm R M₁ (TensorProduct S M₂ M₃))).trans
                        (LinearEquiv.restrictScalars R
                          (TensorProduct.AlgebraTensorModule.congr (TensorProduct.comm S M₂ M₃)
                            (LinearEquiv.refl R M₁)))).trans
                    (LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.assoc R S S M₃ M₂ M₁))).trans
                (LinearEquiv.restrictScalars R (TensorProduct.comm S M₃ (TensorProduct R M₂ M₁)))).trans
            (LinearEquiv.restrictScalars R
              (TensorProduct.congr
                (let __spread.0 := TensorProduct.comm R M₂ M₁;
                { toAddHom := (↑__spread.0).toAddHom, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ })
                (LinearEquiv.refl S M₃)))).trans
        (LinearEquiv.restrictScalars R
          (TensorProduct.congr (AddEquiv.linearEquiv S hf.equiv.toAddEquiv) (LinearEquiv.refl S M₃)))).symm