-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
rw :
  ((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
            (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
        (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((gradedCommAux R 𝒜 ℬ : (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 : ι), ℬ 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)
rw₁ :
  ((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
            (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
        (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      (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))) =
    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)
rw₂ :
  ((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
            (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
        (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      (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))) =
    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)
rw₃ :
  ((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
            (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
        (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      (HSMul.hSMul (α := R) (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
        (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
        (((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))) =
    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)
rw₄ :
  HSMul.hSMul (α := R) (β := (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
              (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
                (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
            (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 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₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) =
    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)
rw₅ :
  HSMul.hSMul (α := R) (β := (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      ((lof R ι ℬ j : (a : ℬ j) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) =
    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)
rw₆ :
  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) =
    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)
⊢ ((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
            (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
        (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
        (((TensorProduct.directSum R R 𝒜 ℬ :
              ((⨁ (i₁ : ι), 𝒜 i₁) ⊗[R] ⨁ (i₂ : ι), ℬ i₂) ≃ₗ[R]
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
            (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
          ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j : (a : ℬ j) → ⨁ (i : ι), ℬ i) b))) =
    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)
have rw₇ : 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) =
  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)
Tactic: rw [TensorProduct.directSum_lof_tmul_lof, gradedCommAux_lof_tmul, Units.smul_def,
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 specialized `map_smul` to `LinearEquiv.map_smul` to avoid timeouts.
    ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, TensorProduct.directSum_symm_lof_tmul,
    Int.cast_smul_eq_zsmul, ← Units.smul_def]