∀ (R : Type u_3) (S : Type u_4) (A : Type u_1) (B : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (a₁ a₂ : A) (b₁ b₂ : B),
  MulOpposite.unop
      (↑(TensorProduct.AlgebraTensorModule.congr (MulOpposite.opLinearEquiv S) (MulOpposite.opLinearEquiv R) ≪≫ₗ
            MulOpposite.opLinearEquiv S)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂))) =
    MulOpposite.unop
      (↑(TensorProduct.AlgebraTensorModule.congr (MulOpposite.opLinearEquiv S) (MulOpposite.opLinearEquiv R) ≪≫ₗ
              MulOpposite.opLinearEquiv S)
          (a₁ ⊗ₜ[R] b₁) *
        ↑(TensorProduct.AlgebraTensorModule.congr (MulOpposite.opLinearEquiv S) (MulOpposite.opLinearEquiv R) ≪≫ₗ
              MulOpposite.opLinearEquiv S)
          (a₂ ⊗ₜ[R] b₂))