awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x_1 x_2 : ι
h : x_1 ≤ x_2
x : TensorProduct.{u_1, u_3, u_4} R (G x_1) M
⊢ ∀ (x y : TensorProduct.{u_1, u_3, u_4} R (G x_1) M),
    Eq (α := Module.DirectLimit G f ⊗[R] M)
        (((fun (x : ι) ↦
                  (LinearMap.rTensor M (of R ι G f x) :
                    TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                x_2 :
              (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
            ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) x) :
          Module.DirectLimit G f ⊗[R] M)
        (((fun (x : ι) ↦
                  (LinearMap.rTensor M (of R ι G f x) :
                    TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                x_1 :
              (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
            x :
          Module.DirectLimit G f ⊗[R] M) →
      Eq (α := Module.DirectLimit G f ⊗[R] M)
          (((fun (x : ι) ↦
                    (LinearMap.rTensor M (of R ι G f x) :
                      TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                  x_2 :
                (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
              ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) y) :
            Module.DirectLimit G f ⊗[R] M)
          (((fun (x : ι) ↦
                    (LinearMap.rTensor M (of R ι G f x) :
                      TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                  x_1 :
                (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
              y :
            Module.DirectLimit G f ⊗[R] M) →
        Eq (α := Module.DirectLimit G f ⊗[R] M)
          (((fun (x : ι) ↦
                    (LinearMap.rTensor M (of R ι G f x) :
                      TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                  x_2 :
                (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
              ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) (x + y)) :
            Module.DirectLimit G f ⊗[R] M)
          (((fun (x : ι) ↦
                    (LinearMap.rTensor M (of R ι G f x) :
                      TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                  x_1 :
                (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
              (x + y) :
            Module.DirectLimit G f ⊗[R] M)

Tactic:
aesop
-- 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
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M)
    ((fromDirectLimit (G := G) f M :
          (a :
              Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) →
            Module.DirectLimit G f ⊗[R] M)
        (((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 G f ⊗[R] M)
    ((of R ι G f i : (a : G i) → Module.DirectLimit G f) g ⊗ₜ[R] m : Module.DirectLimit G f ⊗[R] M)

Tactic:
lift_of (G := (G · ⊗[R] M)) _ _ (g ⊗ₜ m)

Premises used: Module.DirectLimit.lift_of, Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- 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
⊢ 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))

Tactic:
rfl
-- 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
h :
  ∀ (i : ι) (x : G i) (x_1 : 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))
      ((((LinearMap.compr₂ₛₗ (mk R (G i) M)
                    ((toDirectLimit (G := G) f M ∘ₗ fromDirectLimit (G := G) f M) ∘ₗ
                      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) :
                  (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))
                x :
              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))
          x_1 :
        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₂ₛₗ (σ₃₄ := RingHom.id R) (mk R (G i) M)
                    (LinearMap.id ∘ₗ
                      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) :
                  (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))
                x :
              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))
          x_1 :
        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)) →ₗ[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))
    (toDirectLimit (G := G) f M ∘ₗ fromDirectLimit (G := G) f M) LinearMap.id

Tactic:
ext
-- 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 : G i
x_1 : 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))
    ((((LinearMap.compr₂ₛₗ (mk R (G i) M)
                  ((toDirectLimit (G := G) f M ∘ₗ fromDirectLimit (G := G) f M) ∘ₗ
                    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) :
                (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))
              x :
            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))
        x_1 :
      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₂ₛₗ (σ₃₄ := RingHom.id R) (mk R (G i) M)
                  (LinearMap.id ∘ₗ
                    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) :
                (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))
              x :
            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))
        x_1 :
      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:
simp
-- 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
H :
  ∀ (i : ι) (x : G i) (x_1 : M),
    Eq (α := Module.DirectLimit G f ⊗[R] M)
      ((((LinearMap.compr₂ₛₗ (mk R (Module.DirectLimit G f) M)
                      (fromDirectLimit (G := G) f M ∘ₗ toDirectLimit (G := G) f M) ∘ₗ
                    of R ι G f i :
                  (a : G i) → M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
                x :
              M →ₗ[R] Module.DirectLimit G f ⊗[R] M) :
            (a : M) → Module.DirectLimit G f ⊗[R] M)
          x_1 :
        Module.DirectLimit G f ⊗[R] M)
      ((((LinearMap.compr₂ₛₗ (mk R (Module.DirectLimit G f) M) LinearMap.id ∘ₗ of R ι G f i :
                  (a : G i) → M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
                x :
              M →ₗ[R] Module.DirectLimit G f ⊗[R] M) :
            (a : M) → Module.DirectLimit G f ⊗[R] M)
          x_1 :
        Module.DirectLimit G f ⊗[R] M)
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
    (fromDirectLimit (G := G) f M ∘ₗ toDirectLimit (G := G) f M) LinearMap.id

Tactic:
ext
-- 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 : G i
x_1 : M
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M)
    ((((LinearMap.compr₂ₛₗ (mk R (Module.DirectLimit G f) M)
                    (fromDirectLimit (G := G) f M ∘ₗ toDirectLimit (G := G) f M) ∘ₗ
                  of R ι G f i :
                (a : G i) → M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
              x :
            M →ₗ[R] Module.DirectLimit G f ⊗[R] M) :
          (a : M) → Module.DirectLimit G f ⊗[R] M)
        x_1 :
      Module.DirectLimit G f ⊗[R] M)
    ((((LinearMap.compr₂ₛₗ (mk R (Module.DirectLimit G f) M) LinearMap.id ∘ₗ of R ι G f i :
                (a : G i) → M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
              x :
            M →ₗ[R] Module.DirectLimit G f ⊗[R] M) :
          (a : M) → Module.DirectLimit G f ⊗[R] M)
        x_1 :
      Module.DirectLimit G f ⊗[R] M)

Tactic:
simp
-- 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
⊢ 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))
        ((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 (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))
        (g ⊗ₜ[R] m) :
      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:
toDirectLimit_tmul_of f g m

Premises used: TensorProduct.toDirectLimit_tmul_of
-- 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
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M)
    ((LinearEquiv.symm (directLimitLeft (G := G) f M) :
          (a :
              Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) →
            Module.DirectLimit G f ⊗[R] M)
        (((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 G f ⊗[R] M)
    ((of R ι G f i : (a : G i) → Module.DirectLimit G f) g ⊗ₜ[R] m : Module.DirectLimit G f ⊗[R] M)

Tactic:
fromDirectLimit_of_tmul f g m

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, Quotient.map₂, TensorProduct.fromDirectLimit_of_tmul, List.foldr, Finset.sum, Trunc.lift
-- 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
⊢ 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) 0))
    (((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))
      0)

Tactic:
simp
-- 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 : G i) (y : 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 ⊗ₜ[R] 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 ⊗ₜ[R] 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
-- 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 j : ι
h : i ≤ j
⊢ ∀ (x : G i),
    Eq (α := M →ₗ[R] TensorProduct.{u_1, u_4, u_3} R M (G j))
      ((LinearMap.compr₂ₛₗ (mk R (G i) M)
              ((↑((fun (x : ι) ↦
                        (TensorProduct.comm R (G x) M :
                          TensorProduct.{u_1, u_3, u_4} R (G x) M ≃ₗ[R] TensorProduct.{u_1, u_4, u_3} R M (G x)))
                      j) :
                  G j ⊗[R] M →ₗ[R] M ⊗[R] G j) ∘ₗ
                LinearMap.rTensor M (f i j h)) :
            (a : G i) → M →ₗ[R] M ⊗[R] G j)
          x :
        M →ₗ[R] TensorProduct.{u_1, u_4, u_3} R M (G j))
      ((LinearMap.compr₂ₛₗ (mk R (G i) M)
              (LinearMap.lTensor M (f i j h) ∘ₗ
                (↑((fun (x : ι) ↦
                        (TensorProduct.comm R (G x) M :
                          TensorProduct.{u_1, u_3, u_4} R (G x) M ≃ₗ[R] TensorProduct.{u_1, u_4, u_3} R M (G x)))
                      i) :
                  G i ⊗[R] M →ₗ[R] M ⊗[R] G i)) :
            (a : G i) → M →ₗ[R] M ⊗[R] G j)
          x :
        M →ₗ[R] TensorProduct.{u_1, u_4, u_3} R M (G j))

Tactic:
aesop