-- 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 ι ℬ
a :
  ∀ (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)
⊢ Eq (α :=
    DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (LinearMap.compr₂ (gradedMul R 𝒜 ℬ)
      (↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i))
    (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))

Tactic:
ext i₁ a₁ j₁ b₁ i₂ a₂ j₂ b₂