-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
i : ι
g : G i
m : M
rw :
  Eq (α :=
    Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
      LinearMap.rTensor M (f i j h))
    ((((LinearMap.compr₂ (mk R (G i) M)
                  (of R ι (fun (_i : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G _i) M)
                    (fun (_i _j : ι) (h : _i ≤ _j) ↦ LinearMap.rTensor M (f _i _j h)) i) :
                (a : G i) →
                  M →ₗ[R]
                    Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦
                      LinearMap.rTensor M (f i j h))
              g :
            M →ₗ[R]
              Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
          (a : M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        m :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
    (((of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
              (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) i :
            TensorProduct.{u_1, u_3, u_4} R (G i) M →ₗ[R]
              Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
          (a : G i ⊗[R] M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        (g ⊗ₜ[R] m) :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
⊢ Eq (α :=
    Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
      LinearMap.rTensor M (f i j h))
    ((toDirectLimit (G := G) f M :
          (a : Module.DirectLimit G f ⊗[R] M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        ((of R ι G f i : (a : G i) → Module.DirectLimit G f) g ⊗ₜ[R] m) :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
    (((of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
              (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) i :
            TensorProduct.{u_1, u_3, u_4} R (G i) M →ₗ[R]
              Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
          (a : G i ⊗[R] M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        (g ⊗ₜ[R] m) :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))

Tactic:
rw [toDirectLimit, lift.tmul, lift_of]

Premises used: Module.DirectLimit.lift_of, TensorProduct.toDirectLimit, TensorProduct.lift.tmul