-- 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)
i j : ι
a : 𝒜 i
b : ℬ j
simp :
  (HSMul.hSMul (β :=
          TensorProduct.{u_1, u_4, u_3} R (ℬ j) (𝒜 i) →ₗ[R]
            ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
          (HPow.hPow (α := ℤˣ) (-1) (j * i))
          (lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (j, i) :
            TensorProduct.{u_1, u_4, u_3} R (ℬ (j, i).1) (𝒜 (j, i).2) →ₗ[R]
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ℬ j ⊗[R] 𝒜 i) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
      (b ⊗ₜ[R] a) =
    HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (j, i) :
              TensorProduct.{u_1, u_4, u_3} R (ℬ (j, i).1) (𝒜 (j, i).2) →ₗ[R]
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
            (a : ℬ j ⊗[R] 𝒜 i) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
          (b ⊗ₜ[R] a) :
        ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
⊢ (DirectSum.toModule R (ι × ι) (M := fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2))
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) fun (i : ι × ι) ↦
          have o :
            TensorProduct.{u_1, u_4, u_3} R (ℬ (i.2, i.1).1) (𝒜 (i.2, i.1).2) →ₗ[R]
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) :=
            lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (i.2, i.1);
          have s := HPow.hPow (α := ℤˣ) (-1) (i.1 * i.2);
          (s • o) ∘ₗ (↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2)) : 𝒜 i.1 ⊗[R] ℬ i.2 →ₗ[R] ℬ i.2 ⊗[R] 𝒜 i.1) :
        (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
      (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) (i, j) :
            TensorProduct.{u_1, u_3, u_4} R (𝒜 (i, j).1) (ℬ (i, j).2) →ₗ[R]
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
          (a : 𝒜 (i, j).1 ⊗[R] ℬ (i, j).2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
        (a ⊗ₜ[R] b)) =
    HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (j, i) :
              TensorProduct.{u_1, u_4, u_3} R (ℬ (j, i).1) (𝒜 (j, i).2) →ₗ[R]
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
            (a : ℬ (j, i).1 ⊗[R] 𝒜 (j, i).2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
          (b ⊗ₜ[R] a) :
        ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))

Tactic:
simp [mul_comm i j]

Premises used: mul_comm