awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_5 : DecidableEq { P : Submodule R M // P.FG }
P : { P : Submodule R M // P.FG }
u : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
suffices :
  Eq (α := TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N →ₗ[R] M ⊗[R] N)
    ((↑(directLimit R M 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)) →ₗ[R]
          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 }) (hPQ : x ≤ x_1) ↦ rTensor N (inclusion hPQ)) P)
    (rTensor N (↑P : Submodule R M).subtype)
⊢ Eq (α := M ⊗[R] N)
    ((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))
          u) :
      M ⊗[R] N)
    ((rTensor N (↑P : Submodule R M).subtype : (a : ↥(↑P : Submodule R M) ⊗[R] N) → M ⊗[R] N) u : M ⊗[R] N)

Tactic:
suffices (Submodule.FG.rTensor.directLimit R M N).toLinearMap.comp
      (Module.DirectLimit.of R {P : Submodule R M // P.FG} (fun P ↦ P.val ⊗[R] N)
        (fun _ _ hPQ ↦ rTensor N (Submodule.inclusion hPQ)) P)
      = rTensor N (Submodule.subtype P.val) by
    exact DFunLike.congr_fun this u
-- 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
inst_5 : DecidableEq { P : Submodule R M // P.FG }
P : { P : Submodule R M // P.FG }
u : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
a :
  ∀ (p : ↥(↑P : Submodule R M)) (n : N),
    Eq (α := M ⊗[R] N)
      (((((AlgebraTensorModule.curry
                      ((↑(directLimit R M 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)) →ₗ[R]
                            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 }) (hPQ : x ≤ x_1) ↦ rTensor N (inclusion hPQ)) P) :
                    ↥(↑P : Submodule R M) →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                  (a : ↥(↑P : Submodule R M)) → N →ₗ[R] M ⊗[R] N)
                p :
              N →ₗ[R] M ⊗[R] N) :
            (a : N) → M ⊗[R] N)
          n :
        M ⊗[R] N)
      (((((AlgebraTensorModule.curry (rTensor N (↑P : Submodule R M).subtype) :
                    ↥(↑P : Submodule R M) →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                  (a : ↥(↑P : Submodule R M)) → N →ₗ[R] M ⊗[R] N)
                p :
              N →ₗ[R] M ⊗[R] N) :
            (a : N) → M ⊗[R] N)
          n :
        M ⊗[R] N)
⊢ Eq (α := TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N →ₗ[R] M ⊗[R] N)
    ((↑(directLimit R M 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)) →ₗ[R]
          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 }) (hPQ : x ≤ x_1) ↦ rTensor N (inclusion hPQ)) P)
    (rTensor N (↑P : Submodule R M).subtype)

Tactic:
ext p n
-- 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
inst_5 : DecidableEq { P : Submodule R M // P.FG }
P : { P : Submodule R M // P.FG }
u : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
p : ↥(↑P : Submodule R M)
n : N
⊢ Eq (α := M ⊗[R] N)
    (((((AlgebraTensorModule.curry
                    ((↑(directLimit R M 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)) →ₗ[R]
                          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 }) (hPQ : x ≤ x_1) ↦ rTensor N (inclusion hPQ)) P) :
                  ↥(↑P : Submodule R M) →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : ↥(↑P : Submodule R M)) → N →ₗ[R] M ⊗[R] N)
              p :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)
    (((((AlgebraTensorModule.curry (rTensor N (↑P : Submodule R M).subtype) :
                  ↥(↑P : Submodule R M) →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : ↥(↑P : Submodule R M)) → N →ₗ[R] M ⊗[R] N)
              p :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        n :
      M ⊗[R] N)

Tactic:
simp [Submodule.FG.rTensor.directLimit, Submodule.FG.directLimit]

Premises used: Submodule.FG.directLimit, Submodule.FG.rTensor.directLimit
-- 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
inst_5 : DecidableEq { P : Submodule R M // P.FG }
P : Submodule R M
hP : P.FG
u : TensorProduct.{u, u_1, u_2} R (↥P) N
⊢ Eq (α := M ⊗[R] N)
    ((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))
                (Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) P hP) :
              TensorProduct.{u, u_1, u_2} R
                  (↥(↑(Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) P hP) : 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, hP⟩ : 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))
          u) :
      M ⊗[R] N)
    ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) u : M ⊗[R] N)

Tactic:
apply Submodule.FG.rTensor.directLimit_apply

Premises used: Submodule.FG.rTensor.directLimit_apply
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i : ι
t : TensorProduct.{u, u_1, u_4} R M (F i)
rw :
  Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f ⋯) : (a : M ⊗[R] F i) → M ⊗[R] F i) ((LinearMap.id : (a : M ⊗[R] F i) → M ⊗[R] F i) t) :
      TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.id : (a : M ⊗[R] F i) → M ⊗[R] F i) t : TensorProduct.{u, u_1, u_4} R M (F i))
⊢ (LinearMap.lTensor M (f ⋯) : (a : M ⊗[R] F i) → M ⊗[R] F i) t = t

Tactic:
rw [← id_apply (R := R) t]

Premises used: LinearMap.id_apply
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i : ι
t : TensorProduct.{u, u_1, u_4} R M (F i)
h₁ :
  Eq (α := TensorProduct.{u, u_1, u_4} R M (F i) →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i))
    (LinearMap.lTensor M (f ⋯)) LinearMap.id
⊢ Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f ⋯) : (a : M ⊗[R] F i) → M ⊗[R] F i) ((LinearMap.id : (a : M ⊗[R] F i) → M ⊗[R] F i) t) :
      TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.id : (a : M ⊗[R] F i) → M ⊗[R] F i) t : TensorProduct.{u, u_1, u_4} R M (F i))

Tactic:
apply DFunLike.congr_fun

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i : ι
t : TensorProduct.{u, u_1, u_4} R M (F i)
h₁ :
  ∀ (m : M) (n : F i),
    Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
      (((((AlgebraTensorModule.curry (LinearMap.lTensor M (f ⋯)) :
                    M →ₗ[R] F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                  (a : M) → F i →ₗ[R] M ⊗[R] F i)
                m :
              F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
            (a : F i) → M ⊗[R] F i)
          n :
        TensorProduct.{u, u_1, u_4} R M (F i))
      (((((AlgebraTensorModule.curry LinearMap.id : M →ₗ[R] F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                  (a : M) → F i →ₗ[R] M ⊗[R] F i)
                m :
              F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
            (a : F i) → M ⊗[R] F i)
          n :
        TensorProduct.{u, u_1, u_4} R M (F i))
⊢ Eq (α := TensorProduct.{u, u_1, u_4} R M (F i) →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i))
    (LinearMap.lTensor M (f ⋯)) LinearMap.id

Tactic:
ext m n
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i : ι
t : TensorProduct.{u, u_1, u_4} R M (F i)
m : M
n : F i
⊢ Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    (((((AlgebraTensorModule.curry (LinearMap.lTensor M (f ⋯)) :
                  M →ₗ[R] F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                (a : M) → F i →ₗ[R] M ⊗[R] F i)
              m :
            F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
          (a : F i) → M ⊗[R] F i)
        n :
      TensorProduct.{u, u_1, u_4} R M (F i))
    (((((AlgebraTensorModule.curry LinearMap.id : M →ₗ[R] F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                (a : M) → F i →ₗ[R] M ⊗[R] F i)
              m :
            F i →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
          (a : F i) → M ⊗[R] F i)
        n :
      TensorProduct.{u, u_1, u_4} R M (F i))

Tactic:
simp [D.map_self]

Premises used: DirectedSystem.map_self
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : TensorProduct.{u, u_1, u_4} R M (F k)
rw :
  Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f h' ∘ₗ f h) : (a : M ⊗[R] F k) → M ⊗[R] F i) t : TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f ⋯) : (a : M ⊗[R] F k) → M ⊗[R] F i) t : TensorProduct.{u, u_1, u_4} R M (F i))
⊢ Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f h') : (a : M ⊗[R] F j) → M ⊗[R] F i)
        ((LinearMap.lTensor M (f h) : (a : M ⊗[R] F k) → M ⊗[R] F j) t) :
      TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f ⋯) : (a : M ⊗[R] F k) → M ⊗[R] F i) t : TensorProduct.{u, u_1, u_4} R M (F i))

Tactic:
rw [← comp_apply, ← lTensor_comp]

Premises used: LinearMap.comp_apply, LinearMap.lTensor_comp
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : TensorProduct.{u, u_1, u_4} R M (F k)
h₁ :
  Eq (α := TensorProduct.{u, u_1, u_4} R M (F k) →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i))
    (LinearMap.lTensor M (f h' ∘ₗ f h)) (LinearMap.lTensor M (f ⋯))
⊢ Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f h' ∘ₗ f h) : (a : M ⊗[R] F k) → M ⊗[R] F i) t : TensorProduct.{u, u_1, u_4} R M (F i))
    ((LinearMap.lTensor M (f ⋯) : (a : M ⊗[R] F k) → M ⊗[R] F i) t : TensorProduct.{u, u_1, u_4} R M (F i))

Tactic:
apply DFunLike.congr_fun

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : TensorProduct.{u, u_1, u_4} R M (F k)
h₁ :
  ∀ (p : M) (n : F k),
    Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
      (((((AlgebraTensorModule.curry (LinearMap.lTensor M (f h' ∘ₗ f h)) :
                    M →ₗ[R] F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                  (a : M) → F k →ₗ[R] M ⊗[R] F i)
                p :
              F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
            (a : F k) → M ⊗[R] F i)
          n :
        TensorProduct.{u, u_1, u_4} R M (F i))
      (((((AlgebraTensorModule.curry (LinearMap.lTensor M (f ⋯)) :
                    M →ₗ[R] F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                  (a : M) → F k →ₗ[R] M ⊗[R] F i)
                p :
              F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
            (a : F k) → M ⊗[R] F i)
          n :
        TensorProduct.{u, u_1, u_4} R M (F i))
⊢ Eq (α := TensorProduct.{u, u_1, u_4} R M (F k) →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i))
    (LinearMap.lTensor M (f h' ∘ₗ f h)) (LinearMap.lTensor M (f ⋯))

Tactic:
ext p n
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : TensorProduct.{u, u_1, u_4} R M (F k)
p : M
n : F k
⊢ Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    (((((AlgebraTensorModule.curry (LinearMap.lTensor M (f h' ∘ₗ f h)) :
                  M →ₗ[R] F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                (a : M) → F k →ₗ[R] M ⊗[R] F i)
              p :
            F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
          (a : F k) → M ⊗[R] F i)
        n :
      TensorProduct.{u, u_1, u_4} R M (F i))
    (((((AlgebraTensorModule.curry (LinearMap.lTensor M (f ⋯)) :
                  M →ₗ[R] F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
                (a : M) → F k →ₗ[R] M ⊗[R] F i)
              p :
            F k →ₗ[R] TensorProduct.{u, u_1, u_4} R M (F i)) :
          (a : F k) → M ⊗[R] F i)
        n :
      TensorProduct.{u, u_1, u_4} R M (F i))

Tactic:
simp [D.map_map]

Premises used: DirectedSystem.map_map
-- 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
⊢ DirectedSystem (fun (Q : { Q : Submodule R N // Q.FG }) ↦ TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N))
    fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦
    (⇑(lTensor M (inclusion hPQ)) : (a : M ⊗[R] ↥(↑x : Submodule R N)) → M ⊗[R] ↥(↑x_1 : Submodule R N))

Tactic:
Submodule.FG.directedSystem.lTensor R M

Premises used: DirectedSystem.lTensor, Submodule.FG.directedSystem
-- 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
inst_5 : DecidableEq { P : Submodule R N // P.FG }
Q : { Q : Submodule R N // Q.FG }
u : TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N)
this :
  Eq (α := TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N)
    ((↑(directLimit R M N) :
        (Module.DirectLimit (fun (Q : { Q : Submodule R N // Q.FG }) ↦ M ⊗[R] ↥(↑Q : Submodule R N))
            fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) →ₗ[R]
          M ⊗[R] N) ∘ₗ
      Module.DirectLimit.of R { Q : Submodule R N // Q.FG }
        (fun (Q : { Q : Submodule R N // Q.FG }) ↦ TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N))
        (fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) Q)
    (lTensor M (↑Q : Submodule R N).subtype)
⊢ Eq (α := M ⊗[R] N)
    ((directLimit R M N :
          (a :
              Module.DirectLimit (fun (Q : { Q : Submodule R N // Q.FG }) ↦ M ⊗[R] ↥(↑Q : Submodule R N))
                fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) →
            M ⊗[R] N)
        (((Module.DirectLimit.of R { Q : Submodule R N // Q.FG }
                (fun (Q : { Q : Submodule R N // Q.FG }) ↦ TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N))
                (fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) Q :
              TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N) →ₗ[R]
                Module.DirectLimit (R := R)
                  (fun (Q : { Q : Submodule R N // Q.FG }) ↦ TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N))
                  fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) :
            (a : M ⊗[R] ↥(↑Q : Submodule R N)) →
              Module.DirectLimit (fun (Q : { Q : Submodule R N // Q.FG }) ↦ M ⊗[R] ↥(↑Q : Submodule R N))
                fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ))
          u) :
      M ⊗[R] N)
    ((lTensor M (↑Q : Submodule R N).subtype : (a : M ⊗[R] ↥(↑Q : Submodule R N)) → M ⊗[R] N) u : M ⊗[R] N)

Tactic:
DFunLike.congr_fun this u

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn
-- 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
inst_5 : DecidableEq { P : Submodule R N // P.FG }
Q : { Q : Submodule R N // Q.FG }
u : TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N)
this :
  Eq (α := TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N)
    ((↑(directLimit R M N) :
        (Module.DirectLimit (fun (Q : { Q : Submodule R N // Q.FG }) ↦ M ⊗[R] ↥(↑Q : Submodule R N))
            fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) →ₗ[R]
          M ⊗[R] N) ∘ₗ
      Module.DirectLimit.of R { Q : Submodule R N // Q.FG }
        (fun (Q : { Q : Submodule R N // Q.FG }) ↦ TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N))
        (fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) Q)
    (lTensor M (↑Q : Submodule R N).subtype)
⊢ Eq (α := M ⊗[R] N)
    ((directLimit R M N :
          (a :
              Module.DirectLimit (fun (Q : { Q : Submodule R N // Q.FG }) ↦ M ⊗[R] ↥(↑Q : Submodule R N))
                fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) →
            M ⊗[R] N)
        (((Module.DirectLimit.of R { Q : Submodule R N // Q.FG }
                (fun (Q : { Q : Submodule R N // Q.FG }) ↦ TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N))
                (fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) Q :
              TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N) →ₗ[R]
                Module.DirectLimit (R := R)
                  (fun (Q : { Q : Submodule R N // Q.FG }) ↦ TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N))
                  fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ)) :
            (a : M ⊗[R] ↥(↑Q : Submodule R N)) →
              Module.DirectLimit (fun (Q : { Q : Submodule R N // Q.FG }) ↦ M ⊗[R] ↥(↑Q : Submodule R N))
                fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) ↦ lTensor M (inclusion hPQ))
          u) :
      M ⊗[R] N)
    ((lTensor M (↑Q : Submodule R N).subtype : (a : M ⊗[R] ↥(↑Q : Submodule R N)) → M ⊗[R] N) u : M ⊗[R] N)

Tactic:
exact DFunLike.congr_fun this u

Premises used: DFunLike.congr_fun