-- 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 z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (((((AlgebraTensorModule.curry
                        (((((AlgebraTensorModule.curry
                                          (((((AlgebraTensorModule.curry
                                                            ((LinearMap.llcomp R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                    (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                    (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                                                  (a :
                                                                      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                                                                    (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
                                                                      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                mA ∘ₗ
                                                              mA) ∘ₗ
                                                          lof R ι 𝒜 ixa :
                                                        𝒜 ixa →ₗ[R]
                                                          DirectSum ι ℬ →ₗ[R]
                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                                      (a : 𝒜 ixa) →
                                                        DirectSum ι ℬ →ₗ[R]
                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                    xa ∘ₗ
                                                  lof R ι ℬ ixb :
                                                ℬ ixb →ₗ[R]
                                                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                    DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                              (a : ℬ ixb) →
                                                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                    DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                            xb) ∘ₗ
                                        lof R ι 𝒜 iya :
                                      𝒜 iya →ₗ[R]
                                        DirectSum ι ℬ →ₗ[R]
                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                    (a : 𝒜 iya) →
                                      DirectSum ι ℬ →ₗ[R]
                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                  ya ∘ₗ
                                lof R ι ℬ iyb :
                              ℬ iyb →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                            (a : ℬ iyb) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                          yb) ∘ₗ
                      lof R ι 𝒜 iza :
                    𝒜 iza →ₗ[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                  (a : 𝒜 iza) → DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                za ∘ₗ
              lof R ι ℬ izb :
            ℬ izb →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
          (a : ℬ izb) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        zb :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (((((AlgebraTensorModule.curry
                        (((((AlgebraTensorModule.curry
                                          (((((AlgebraTensorModule.curry
                                                            (LinearMap.flip
                                                              ((((LinearMap.llcomp R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                          (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 ι ℬ →ₗ[R]
                                                                                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                                  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 ι ℬ →ₗ[R]
                                                                                  DirectSum ι 𝒜 ⊗[R]
                                                                                    DirectSum ι ℬ) →ₗ[R]
                                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                      (↑LinearMap.lflip :
                                                                        (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                              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 ι ℬ →ₗ[R]
                                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
                                                                      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                                                  (a :
                                                                      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 ι ℬ →ₗ[R]
                                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                ((LinearMap.llcomp R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                        (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                        (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                                                      (a :
                                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                                                                        (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
                                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                                    mA.flip ∘ₗ
                                                                  mA))) ∘ₗ
                                                          lof R ι 𝒜 ixa :
                                                        𝒜 ixa →ₗ[R]
                                                          DirectSum ι ℬ →ₗ[R]
                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                                      (a : 𝒜 ixa) →
                                                        DirectSum ι ℬ →ₗ[R]
                                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                                    xa ∘ₗ
                                                  lof R ι ℬ ixb :
                                                ℬ ixb →ₗ[R]
                                                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                    DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                              (a : ℬ ixb) →
                                                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                                    DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                            xb) ∘ₗ
                                        lof R ι 𝒜 iya :
                                      𝒜 iya →ₗ[R]
                                        DirectSum ι ℬ →ₗ[R]
                                          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                                    (a : 𝒜 iya) →
                                      DirectSum ι ℬ →ₗ[R]
                                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                  ya ∘ₗ
                                lof R ι ℬ iyb :
                              ℬ iyb →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                            (a : ℬ iyb) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                          yb) ∘ₗ
                      lof R ι 𝒜 iza :
                    𝒜 iza →ₗ[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                  (a : 𝒜 iza) → DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                za ∘ₗ
              lof R ι ℬ izb :
            ℬ izb →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
          (a : ℬ izb) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        zb :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
have a : Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
  ((((gradedMul R 𝒜 ℬ :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            ((((gradedMul R 𝒜 ℬ :
                      (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →
                        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                    ((lof R ι 𝒜 ixa : (a : 𝒜 ixa) → ⨁ (i : ι), 𝒜 i) xa ⊗ₜ[R]
                      (lof R ι ℬ ixb : (a : ℬ ixb) → ⨁ (i : ι), ℬ i) xb) :
                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
              ((lof R ι 𝒜 iya : (a : 𝒜 iya) → ⨁ (i : ι), 𝒜 i) ya ⊗ₜ[R]
                (lof R ι ℬ iyb : (a : ℬ iyb) → ⨁ (i : ι), ℬ i) yb)) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      ((lof R ι 𝒜 iza : (a : 𝒜 iza) → ⨁ (i : ι), 𝒜 i) za ⊗ₜ[R] (lof R ι ℬ izb : (a : ℬ izb) → ⨁ (i : ι), ℬ i) zb) :
    DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
  ((((gradedMul R 𝒜 ℬ :
              (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            ((lof R ι 𝒜 ixa : (a : 𝒜 ixa) → ⨁ (i : ι), 𝒜 i) xa ⊗ₜ[R]
              (lof R ι ℬ ixb : (a : ℬ ixb) → ⨁ (i : ι), ℬ i) xb) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      ((((gradedMul R 𝒜 ℬ :
                (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →
                  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
              ((lof R ι 𝒜 iya : (a : 𝒜 iya) → ⨁ (i : ι), 𝒜 i) ya ⊗ₜ[R]
                (lof R ι ℬ iyb : (a : ℬ iyb) → ⨁ (i : ι), ℬ i) yb) :
            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
          (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        ((lof R ι 𝒜 iza : (a : 𝒜 iza) → ⨁ (i : ι), 𝒜 i) za ⊗ₜ[R] (lof R ι ℬ izb : (a : ℬ izb) → ⨁ (i : ι), ℬ i) zb)) :
    DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
Tactic: dsimp [mA]