-- Lean 4 proof step from Mathlib.Algebra.Colimit.TensorProduct (hypothesis)
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 (α :=
    TensorProduct.{u_1, u_3, u_2} R
      (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
    ((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) :
      TensorProduct.{u_1, u_3, u_2} R
        (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
    ((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) :
      TensorProduct.{u_1, u_3, u_2} R
        (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
⊢ ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : (↑N : Submodule R P) ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
have 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))
Tactic: apply_fun directLimitLeft _ _ at eq
Cleared hypotheses: eq