-- Module: Mathlib.Algebra.Colimit.TensorProduct
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : { x : Submodule R P // x.FG }
x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M
eq :
  Eq (α :=
    Module.DirectLimit (R := R)
      (fun (x : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑x : Submodule R P)) M)
      fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
    ((directLimitLeft (G := fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P) M :
          (a :
              Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                  (Module.fgSystem R P) ⊗[R]
                M) →
            Module.DirectLimit (fun (x : { N : Submodule R P // N.FG }) ↦ ↥(↑x : Submodule R P) ⊗[R] M)
              fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
        ((LinearMap.rTensor M
              (↑(LinearEquiv.symm (Module.fgSystem.equiv R P)) :
                P →ₗ[R]
                  Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                    (Module.fgSystem R P)) :
            (a : P ⊗[R] M) →
              Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                  (Module.fgSystem R P) ⊗[R]
                M)
          ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x)) :
      Module.DirectLimit (R := R)
        (fun (x : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑x : Submodule R P)) M)
        fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
    ((directLimitLeft (G := fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P) M :
          (a :
              Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                  (Module.fgSystem R P) ⊗[R]
                M) →
            Module.DirectLimit (fun (x : { N : Submodule R P // N.FG }) ↦ ↥(↑x : Submodule R P) ⊗[R] M)
              fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
        ((LinearMap.rTensor M
              (↑(LinearEquiv.symm (Module.fgSystem.equiv R P)) :
                P →ₗ[R]
                  Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                    (Module.fgSystem R P)) :
            (a : P ⊗[R] M) →
              Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                  (Module.fgSystem R P) ⊗[R]
                M)
          ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y)) :
      Module.DirectLimit (R := R)
        (fun (x : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑x : Submodule R P)) M)
        fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
⊢ Eq (α :=
    Module.DirectLimit (R := R)
      (fun (x : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑x : Submodule R P)) M)
      fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
    (((Module.DirectLimit.of R { N : Submodule R P // N.FG }
              (fun (i : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑i : Submodule R P)) M)
              (fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
              N :
            TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M →ₗ[R]
              Module.DirectLimit (R := R)
                (fun (i : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑i : Submodule R P)) M)
                fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦
                LinearMap.rTensor M (Module.fgSystem R P i j h)) :
          (a : ↥(↑N : Submodule R P) ⊗[R] M) →
            Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P) ⊗[R] M)
              fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
        x :
      Module.DirectLimit (R := R)
        (fun (i : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑i : Submodule R P)) M)
        fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
    (((Module.DirectLimit.of R { N : Submodule R P // N.FG }
              (fun (i : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑i : Submodule R P)) M)
              (fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
              N :
            TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M →ₗ[R]
              Module.DirectLimit (R := R)
                (fun (i : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑i : Submodule R P)) M)
                fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦
                LinearMap.rTensor M (Module.fgSystem R P i j h)) :
          (a : ↥(↑N : Submodule R P) ⊗[R] M) →
            Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P) ⊗[R] M)
              fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))
        y :
      Module.DirectLimit (R := R)
        (fun (i : { N : Submodule R P // N.FG }) ↦ TensorProduct.{u_1, u_3, u_2} R (↥(↑i : Submodule R P)) M)
        fun (i j : { N : Submodule R P // N.FG }) (h : i ≤ j) ↦ LinearMap.rTensor M (Module.fgSystem R P i j h))

Tactic:
simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq

Premises used: Iff.mpr, LinearEquiv.eq_toLinearMap_symm_comp, TensorProduct.directLimitLeft_rTensor_of, Module.fgSystem.equiv_comp_of, LinearMap.rTensor_comp_apply