-- 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)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ ((((curry
                  (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)) ∘ₗ
                    (↑(LinearEquiv.symm
                            (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i)
                              ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i))) :
                        (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)) →ₗ[R]
                          ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)) ∘ₗ
                      LinearMap.lTensor (⨁ (i : ι), 𝒜 i)
                          ((↑(TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) :
                              (((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R]
                                (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)) ∘ₗ
                            LinearMap.rTensor (⨁ (i : ι), ℬ i)
                                (↑(gradedComm R ℬ 𝒜) :
                                  ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) ∘ₗ
                              (↑(LinearEquiv.symm
                                    (TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ))) :
                                DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
                                  DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)) ∘ₗ
                        (↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)) :
                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
                            DirectSum ι 𝒜 ⊗[R] (DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)))) :
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            (a₁ ⊗ₜ[R] (lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ ⊗ₜ[R] b₂) =
    HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      (HMul.hMul (β := ⨁ (i : ι), 𝒜 i) a₁ ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), ℬ i) ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i) b₂)
have dsimp : ((map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)) :
        ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R]
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
      (a : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)) →
        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    ((LinearEquiv.symm
          (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)) :
        (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i))) →
          ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i))
      (a₁ ⊗ₜ[R]
        (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i) :
            (a : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i) →
              (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i))
          ((gradedComm R ℬ 𝒜 : (a : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) → (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
              ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ ⊗ₜ[R]
                (lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂) ⊗ₜ[R]
            b₂))) =
  HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
    (HMul.hMul (β := ⨁ (i : ι), 𝒜 i) a₁ ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      HMul.hMul (α := ⨁ (i : ι), ℬ i) ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i) b₂)
Tactic: dsimp only [curry_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_tmul,
    map_tmul, LinearMap.id_coe, id_eq, assoc_symm_tmul, LinearMap.rTensor_tmul,
    LinearMap.lTensor_tmul]