-- 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 ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (((((AlgebraTensorModule.curry
                        (((((AlgebraTensorModule.curry
                                          (LinearMap.compr₂ (gradedMul R 𝒜 ℬ)
                                            (↑(gradedComm R 𝒜 ℬ) :
                                              ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R]
                                                (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)) ∘ₗ
                                        lof R ι 𝒜 i₁ :
                                      𝒜 i₁ →ₗ[R]
                                        DirectSum ι ℬ →ₗ[R]
                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
                                    (a : 𝒜 i₁) →
                                      DirectSum ι ℬ →ₗ[R]
                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                                  a₁ ∘ₗ
                                lof R ι ℬ j₁ :
                              ℬ j₁ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
                            (a : ℬ j₁) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                          b₁) ∘ₗ
                      lof R ι 𝒜 i₂ :
                    𝒜 i₂ →ₗ[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
                  (a : 𝒜 i₂) → DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                a₂ ∘ₗ
              lof R ι ℬ j₂ :
            ℬ j₂ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
          (a : ℬ j₂) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        b₂ :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (((((AlgebraTensorModule.curry
                        (((((AlgebraTensorModule.curry
                                          (LinearMap.compl₂
                                            (gradedMul R ℬ 𝒜 ∘ₗ
                                              (↑(gradedComm R 𝒜 ℬ) :
                                                ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R]
                                                  (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i))
                                            (↑(gradedComm R 𝒜 ℬ) :
                                              ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R]
                                                (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)) ∘ₗ
                                        lof R ι 𝒜 i₁ :
                                      𝒜 i₁ →ₗ[R]
                                        DirectSum ι ℬ →ₗ[R]
                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
                                    (a : 𝒜 i₁) →
                                      DirectSum ι ℬ →ₗ[R]
                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                                  a₁ ∘ₗ
                                lof R ι ℬ j₁ :
                              ℬ j₁ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
                            (a : ℬ j₁) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                          b₁) ∘ₗ
                      lof R ι 𝒜 i₂ :
                    𝒜 i₂ →ₗ[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
                  (a : 𝒜 i₂) → DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                a₂ ∘ₗ
              lof R ι ℬ j₂ :
            ℬ j₂ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
          (a : ℬ j₂) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        b₂ :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
have a : 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: dsimp