-- 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 : Submodule R P
hN : N.FG
x y : TensorProduct.{u_1, u_3, u_2} R (↥N) M
eq :
  Eq (α := P ⊗[R] M) ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
lift :
  ∀ (N : { x : Submodule R P // x.FG }) (hN : (↑N : Submodule R P).FG)
    {x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M}
    (eq :
      Eq (α := P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x :
          P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y :
          P ⊗[R] 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)
lift₁ :
  ∀ (N : { x : Submodule R P // x.FG }) {x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M}
    (eq :
      Eq (α := P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x :
          P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y :
          P ⊗[R] 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)
lift₂ :
  ∀ (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)
lift₃ :
  ∀ (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))),
    ∃ (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)
lift₄ :
  ∀ (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))
        (((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))),
    ∃ (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)
lift₅ :
  ∀ (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))
        (((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)))
    (N' : { N : Submodule R P // N.FG }) (le : N ≤ N')
    (eq :
      Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥(↑N' : Submodule R P)) M)
        ((LinearMap.rTensor M (Module.fgSystem R P N N' le) :
              (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥(↑N' : Submodule R P) ⊗[R] M)
            x :
          TensorProduct.{u_1, u_3, u_2} R (↥(↑N' : Submodule R P)) M)
        ((LinearMap.rTensor M (Module.fgSystem R P N N' le) :
              (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥(↑N' : Submodule R P) ⊗[R] M)
            y :
          TensorProduct.{u_1, u_3, u_2} R (↥(↑N' : Submodule 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)
⊢ ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : N ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)

Tactic:
classical
  lift N to {N : Submodule R P // N.FG} using hN
  apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
  apply_fun directLimitLeft _ _ at eq
  simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
  have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
  exact ⟨_, N'.2, le, eq⟩

Premises used: TensorProduct.directLimitLeft, Submodule, LinearEquiv.symm, Module.fgSystem.equiv, TensorProduct.directLimitLeft_rTensor_of, Submodule.FG, LinearEquiv.toLinearMap, LinearMap.rTensor_comp_apply, LinearMap.rTensor