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

Tactic:
suffices LinearMap.llcomp R _ _ _ mA ∘ₗ mA =
      (LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <|
        LinearMap.llcomp R _ _ _ mA.flip ∘ₗ mA).flip by
    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z