-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
a :
  Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        (HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
          (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
              ((lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ : ⨁ (i : ι), 𝒜 i)
              ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
            HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
              ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i)
              ((lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂ : ⨁ (i : ι), ℬ i))) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((((gradedMul R ℬ 𝒜 :
                (a : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) →
                  DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
              (HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₁))
                ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ :
                  (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)) :
            DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) :
          (a : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) → DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
        (HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow (α := ℤˣ) (-1) (j₂ * i₂))
          ((lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂ ⊗ₜ[R] (lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ :
            (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)) :
      DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((((gradedMul R 𝒜 ℬ :
                  (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →
                    ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                ((lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ ⊗ₜ[R]
                  (lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁) :
              ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
            (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
          ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ ⊗ₜ[R] (lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂)) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((((gradedMul R ℬ 𝒜 :
                (a : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) →
                  DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
              ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                ((lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ ⊗ₜ[R]
                  (lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁)) :
            DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) :
          (a : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) → DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
        ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ ⊗ₜ[R] (lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂)) :
      DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)

Tactic:
rw [gradedComm_of_tmul_of, gradedComm_of_tmul_of, tmul_of_gradedMul_of_tmul]

Premises used: TensorProduct.tmul_of_gradedMul_of_tmul, TensorProduct.gradedComm_of_tmul_of