awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : 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_4, u_2} R (F i) N
⊢ Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
    ((LinearMap.rTensor N (f ⋯) : (a : F i ⊗[R] N) → F i ⊗[R] N) ((LinearMap.id : (a : F i ⊗[R] N) → F i ⊗[R] N) t) :
      TensorProduct.{u, u_4, u_2} R (F i) N)
    ((LinearMap.id : (a : F i ⊗[R] N) → F i ⊗[R] N) t : TensorProduct.{u, u_4, u_2} R (F i) N)
have h₁ : Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) (LinearMap.rTensor N (f sorry))
  LinearMap.id
Tactic: apply DFunLike.congr_fun
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : 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_4, u_2} R (F i) N
⊢ Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N)
    (LinearMap.rTensor N (f ⋯)) LinearMap.id
have h₁ : ∀ (m : F i) (n : N),
  Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor N (f sorry)) :
                  F i →ₗ[R] N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
                (a : F i) → N →ₗ[R] F i ⊗[R] N)
              m :
            N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
          (a : N) → F i ⊗[R] N)
        n :
      TensorProduct.{u, u_4, u_2} R (F i) N)
    (((((AlgebraTensorModule.curry LinearMap.id : F i →ₗ[R] N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
                (a : F i) → N →ₗ[R] F i ⊗[R] N)
              m :
            N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
          (a : N) → F i ⊗[R] N)
        n :
      TensorProduct.{u, u_4, u_2} R (F i) N)
Tactic: ext m n
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : 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_4, u_2} R (F k) N
⊢ Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
    ((LinearMap.rTensor N (f h') : (a : F j ⊗[R] N) → F i ⊗[R] N)
        ((LinearMap.rTensor N (f h) : (a : F k ⊗[R] N) → F j ⊗[R] N) t) :
      TensorProduct.{u, u_4, u_2} R (F i) N)
    ((LinearMap.rTensor N (f ⋯) : (a : F k ⊗[R] N) → F i ⊗[R] N) t : TensorProduct.{u, u_4, u_2} R (F i) N)
have rw : Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
  ((LinearMap.rTensor N (f h' ∘ₗ f h) : (a : F k ⊗[R] N) → F i ⊗[R] N) t : TensorProduct.{u, u_4, u_2} R (F i) N)
  ((LinearMap.rTensor N (f sorry) : (a : F k ⊗[R] N) → F i ⊗[R] N) t : TensorProduct.{u, u_4, u_2} R (F i) N)
Tactic: rw [← comp_apply, ← rTensor_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : 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_4, u_2} R (F k) N
⊢ Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
    ((LinearMap.rTensor N (f h' ∘ₗ f h) : (a : F k ⊗[R] N) → F i ⊗[R] N) t : TensorProduct.{u, u_4, u_2} R (F i) N)
    ((LinearMap.rTensor N (f ⋯) : (a : F k ⊗[R] N) → F i ⊗[R] N) t : TensorProduct.{u, u_4, u_2} R (F i) N)
have h₁ : Eq (α := TensorProduct.{u, u_4, u_2} R (F k) N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N)
  (LinearMap.rTensor N (f h' ∘ₗ f h)) (LinearMap.rTensor N (f sorry))
Tactic: apply DFunLike.congr_fun
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : 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_4, u_2} R (F k) N
⊢ Eq (α := TensorProduct.{u, u_4, u_2} R (F k) N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N)
    (LinearMap.rTensor N (f h' ∘ₗ f h)) (LinearMap.rTensor N (f ⋯))
have h₁ : ∀ (p : F k) (n : N),
  Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor N (f h' ∘ₗ f h)) :
                  F k →ₗ[R] N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
                (a : F k) → N →ₗ[R] F i ⊗[R] N)
              p :
            N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
          (a : N) → F i ⊗[R] N)
        n :
      TensorProduct.{u, u_4, u_2} R (F i) N)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor N (f sorry)) :
                  F k →ₗ[R] N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
                (a : F k) → N →ₗ[R] F i ⊗[R] N)
              p :
            N →ₗ[R] TensorProduct.{u, u_4, u_2} R (F i) N) :
          (a : N) → F i ⊗[R] N)
        n :
      TensorProduct.{u, u_4, u_2} R (F i) N)
Tactic: ext p n
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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
⊢ 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)
have 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)
Tactic: ext p n
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ (LinearMap.lTensor M (f ⋯) : (a : M ⊗[R] F i) → M ⊗[R] F i) t = t
have rw : Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
  ((LinearMap.lTensor M (f sorry) : (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: rw [← id_apply (R := R) t]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ 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))
have 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 sorry))
  LinearMap.id
Tactic: apply DFunLike.congr_fun
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ 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
have h₁ : ∀ (m : M) (n : F i),
  Eq (α := TensorProduct.{u, u_1, u_4} R M (F i))
    (((((AlgebraTensorModule.curry (LinearMap.lTensor M (f sorry)) :
                  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: ext m n
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ 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))
have 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 sorry) : (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]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ 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))
have 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 sorry))
Tactic: apply DFunLike.congr_fun
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ 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 ⋯))
have 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 sorry)) :
                  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: ext p n
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ 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)
have suffices : 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)
Tactic: suffices (Submodule.FG.lTensor.directLimit R M N).toLinearMap.comp
      (Module.DirectLimit.of R {Q : Submodule R N // Q.FG} (fun Q ↦ M ⊗[R] Q.val)
        (fun _ _ hPQ ↦ lTensor M (inclusion hPQ)) Q)
      = lTensor M (Submodule.subtype Q.val) by
    exact DFunLike.congr_fun this u
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
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)
⊢ 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)
have a : ∀ (p : M) (n : ↥(↑Q : Submodule R N)),
  Eq (α := M ⊗[R] N)
    (((((AlgebraTensorModule.curry
                    ((↑(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) :
                  M →ₗ[R] ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N) :
                (a : M) → ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N)
              p :
            ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N) :
          (a : ↥(↑Q : Submodule R N)) → M ⊗[R] N)
        n :
      M ⊗[R] N)
    (((((AlgebraTensorModule.curry (lTensor M (↑Q : Submodule R N).subtype) :
                  M →ₗ[R] ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N) :
                (a : M) → ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N)
              p :
            ↥(↑Q : Submodule R N) →ₗ[R] M ⊗[R] N) :
          (a : ↥(↑Q : Submodule R N)) → M ⊗[R] N)
        n :
      M ⊗[R] N)
Tactic: ext p n