-- 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 : ι
x : TensorProduct.{u_1, u_3, u_4} R (G i) M
⊢ ∀ (x y : TensorProduct.{u_1, u_3, u_4} R (G i) M),
    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))
        ((directLimitLeft (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))
            ((LinearMap.rTensor M (of R ι G f i) : (a : G i ⊗[R] M) → Module.DirectLimit G f ⊗[R] M) x) :
          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 (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 :
                TensorProduct.{u_1, u_3, u_4} R (G i) M →ₗ[R]
                  Module.DirectLimit (R := 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)) :
              (a : G i ⊗[R] M) →
                Module.DirectLimit (fun (i : ι) ↦ G i ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
            x :
          Module.DirectLimit (R := 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)) →
      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))
          ((directLimitLeft (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))
              ((LinearMap.rTensor M (of R ι G f i) : (a : G i ⊗[R] M) → Module.DirectLimit G f ⊗[R] M) y) :
            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 (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 :
                  TensorProduct.{u_1, u_3, u_4} R (G i) M →ₗ[R]
                    Module.DirectLimit (R := 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)) :
                (a : G i ⊗[R] M) →
                  Module.DirectLimit (fun (i : ι) ↦ G i ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦
                    LinearMap.rTensor M (f i j h))
              y :
            Module.DirectLimit (R := 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)) →
        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))
          ((directLimitLeft (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))
              ((LinearMap.rTensor M (of R ι G f i) : (a : G i ⊗[R] M) → Module.DirectLimit G f ⊗[R] M) (x + y)) :
            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 (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 :
                  TensorProduct.{u_1, u_3, u_4} R (G i) M →ₗ[R]
                    Module.DirectLimit (R := 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)) :
                (a : G i ⊗[R] M) →
                  Module.DirectLimit (fun (i : ι) ↦ G i ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦
                    LinearMap.rTensor M (f i j h))
              (x + y) :
            Module.DirectLimit (R := 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))

Tactic:
simp +contextual