-- 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 ι ℬ
⊢ 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))
have 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)
Tactic: ext i₁ a₁ j₁ b₁ i₂ a₂ j₂ b₂