-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module S M₂
inst_12 : IsScalarTower R S M₂
c : S
x : (M₁ × M₂) ⊗[R] M₃
⊢ ∀ (x y : (M₁ × M₂) ⊗[R] M₃),
    (LinearEquiv.toAddEquiv
              ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                  (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
                (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                  (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
            (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
          (c • x) =
        HSMul.hSMul (β := M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) c
          ((LinearEquiv.toAddEquiv
                  ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                      (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
                    (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                      (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
                (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
              x :
            M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) →
      (LinearEquiv.toAddEquiv
                ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                    (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
                  (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                    (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
              (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
            (c • y) =
          HSMul.hSMul (β := M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) c
            ((LinearEquiv.toAddEquiv
                    ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                        (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
                      (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                        (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
                  (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
                y :
              M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) →
        (LinearEquiv.toAddEquiv
                ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                    (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
                  (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                    (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
              (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
            (c • (x + y)) =
          HSMul.hSMul (β := M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) c
            ((LinearEquiv.toAddEquiv
                    ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                        (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
                      (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                        (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
                  (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
                (x + y) :
              M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)

Tactic:
simp_all