-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : M ⊗[R] N
P : { P : Submodule R M // P.FG }
t : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
ht :
  Eq (α :=
    Module.DirectLimit (R := R)
      (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
      fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
    (((Module.DirectLimit.of R { P : Submodule R M // P.FG }
              (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
              (fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) P :
            TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N →ₗ[R]
              Module.DirectLimit (R := R)
                (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
                fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) :
          (a : ↥(↑P : Submodule R M) ⊗[R] N) →
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        t :
      Module.DirectLimit (R := R)
        (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
        fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
    ((LinearEquiv.symm (FG.rTensor.directLimit R M N) :
          (a : M ⊗[R] N) →
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        u :
      Module.DirectLimit (R := R)
        (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
        fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
h :
  (FG.rTensor.directLimit R M N :
        (a :
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) →
          M ⊗[R] N)
      (((Module.DirectLimit.of R { P : Submodule R M // P.FG }
              (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
              (fun ⦃x x_1 : { P : Submodule R M // P.FG }⦄ (h : x ≤ x_1) ↦ rTensor N (inclusion h)) P :
            TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N →ₗ[R]
              Module.DirectLimit (R := R)
                (fun (P : { P : Submodule R M // P.FG }) ↦ TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
                fun ⦃x x_1 : { P : Submodule R M // P.FG }⦄ (h : x ≤ x_1) ↦ rTensor N (inclusion h)) :
          (a : ↥(↑P : Submodule R M) ⊗[R] N) →
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃x x_1 : { P : Submodule R M // P.FG }⦄ (h : x ≤ x_1) ↦ rTensor N (inclusion h))
        t) =
    u
h₁ :
  (FG.rTensor.directLimit R M N :
        (a :
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h)) →
          M ⊗[R] N)
      ((LinearEquiv.symm (FG.rTensor.directLimit R M N) :
          (a : M ⊗[R] N) →
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M) ⊗[R] N)
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        u) =
    u
h₂ h₃ : u = u
⊢ (rTensor N (↑P : Submodule R M).subtype : (a : ↥(↑P : Submodule R M) ⊗[R] N) → M ⊗[R] N) t = u

Tactic:
rw [← Submodule.FG.rTensor.directLimit_apply, ht, LinearEquiv.apply_symm_apply]

Premises used: Submodule.FG.rTensor.directLimit_apply, LinearEquiv.apply_symm_apply