-- 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 𝒜 ℬ
⊢ 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 ι ℬ)
have 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 ι ℬ)
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