-- 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 z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
a :
  ∀ (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 ι ℬ)
⊢ Eq (α :=
    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 ∘ₗ
        mA :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (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)) :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)

Tactic:
ext ixa xa ixb xb iya ya iyb yb iza za izb zb