awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
x : A
⊢ Eq.{u_7 + 1} (α := B)
    (((fun (f : S ⊗[R] A →ₐ[S] B) ↦ (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
            ((fun (f : A →ₐ[R] B) ↦
                (ofLinearMap
                    (LinearMap.liftBaseChange S
                      (↑f :
                        [inst : FunLike (A →ₐ[R] B) A B] →
                          [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                    ⋯ ⋯ :
                  S ⊗[R] A →ₐ[S] B))
              f) :
          (a : A) → B)
        x :
      B)
    ((f : (a : A) → B) x : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : S ⊗[R] A →ₐ[S] B
H :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := B)
      ((comp (B := S ⊗[R] A)
              (restrictScalars R (S := S)
                ((fun (f : A →ₐ[R] B) ↦
                    (ofLinearMap
                        (LinearMap.liftBaseChange S
                          (↑f :
                            [inst : FunLike (A →ₐ[R] B) A B] →
                              [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                        ⋯ ⋯ :
                      S ⊗[R] A →ₐ[S] B))
                  ((fun (f : S ⊗[R] A →ₐ[S] B) ↦
                      (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
                    f)))
              Algebra.TensorProduct.includeRight :
            (a : A) → B)
          x :
        B)
      ((comp (restrictScalars R f) Algebra.TensorProduct.includeRight : (a : A) → B) x : B)
⊢ Eq (α := A →ₐ[R] B)
    (comp (B := S ⊗[R] A)
      (restrictScalars R (S := S)
        ((fun (f : A →ₐ[R] B) ↦
            (ofLinearMap
                (LinearMap.liftBaseChange S
                  (↑f :
                    [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                ⋯ ⋯ :
              S ⊗[R] A →ₐ[S] B))
          ((fun (f : S ⊗[R] A →ₐ[S] B) ↦ (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
            f)))
      Algebra.TensorProduct.includeRight)
    (comp (restrictScalars R f) Algebra.TensorProduct.includeRight)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : S ⊗[R] A →ₐ[S] B
x : A
⊢ Eq.{u_7 + 1} (α := B)
    ((comp (B := S ⊗[R] A)
            (restrictScalars R (S := S)
              ((fun (f : A →ₐ[R] B) ↦
                  (ofLinearMap
                      (LinearMap.liftBaseChange S
                        (↑f :
                          [inst : FunLike (A →ₐ[R] B) A B] →
                            [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                      ⋯ ⋯ :
                    S ⊗[R] A →ₐ[S] B))
                ((fun (f : S ⊗[R] A →ₐ[S] B) ↦
                    (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
                  f)))
            Algebra.TensorProduct.includeRight :
          (a : A) → B)
        x :
      B)
    ((comp (restrictScalars R f) Algebra.TensorProduct.includeRight : (a : A) → B) x : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra S B
inst_6 : Algebra R S
inst_7 : Algebra R B
inst_8 : IsScalarTower R S B
f : A →ₐ[R] B
s : S
a : A
⊢ (((liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) f : S ⊗[R] A →ₐ[S] B) : (a : S ⊗[R] A) → B) (s ⊗ₜ[R] a) =
    HSMul.hSMul (β := B) s ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra S B
inst_6 : Algebra R S
inst_7 : Algebra R B
inst_8 : IsScalarTower R S B
f : S ⊗[R] A →ₐ[S] B
a : A
⊢ Eq.{u_7 + 1} (α := B)
    ((((Equiv.symm (liftEquiv R S A B) : (a : S ⊗[R] A →ₐ[S] B) → A →ₐ[R] B) f : A →ₐ[R] B) : (a : A) → B) a : B)
    ((f : (a : S ⊗[R] A) → B) (1 ⊗ₜ[R] a) : B)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra S B
inst_6 : Algebra R S
inst_7 : Algebra R B
inst_8 : IsScalarTower R S B
f g : S ⊗[R] A →ₐ[S] B
h :
  Eq (α := A →ₐ[R] B) (comp (restrictScalars R f) Algebra.TensorProduct.includeRight)
    (comp (restrictScalars R g) Algebra.TensorProduct.includeRight)
⊢ f = g

Tactic:
liftEquiv .. |>.symm.injective h

Premises used: Equiv.injective, Equiv.symm, AlgHom.liftEquiv
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u
inst : Semiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq { P : Submodule R M // P.FG }
x : M
⊢ (Module.DirectLimit.lift R { P : Submodule R M // P.FG }
          (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M))
          (fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ inclusion h)
          (fun (P : { P : Submodule R M // P.FG }) ↦ (↑P : Submodule R M).subtype) ⋯ :
        (a :
            Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M))
              fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ inclusion h) →
          M)
      (((Module.DirectLimit.of R { P : Submodule R M // P.FG }
                (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M))
                (fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ inclusion h)
                (Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) (R ∙ x) ⋯) :
              ↥(↑(Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) (R ∙ x) ⋯) : Submodule R M) →ₗ[R]
                Module.DirectLimit.{u, u_1, u_1} (R := R)
                  (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M))
                  fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ inclusion h) :
            (a : ↥(↑⟨R ∙ x, ⋯⟩ : Submodule R M)) →
              Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M))
                fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ inclusion h)
          (Subtype.mk (p := fun (x_1 : M) ↦
            Membership.mem (γ := Submodule R M)
              (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) (R ∙ x) ⋯) : Submodule R M) x_1)
            x ⋯) :
        Module.DirectLimit.{u, u_1, u_1} (R := R) (fun (P : { P : Submodule R M // P.FG }) ↦ ↥(↑P : Submodule R M))
          fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ inclusion h) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
rw :
  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)
⊢ (LinearMap.rTensor N (f ⋯) : (a : F i ⊗[R] N) → F i ⊗[R] N) t = t

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

Premises used: LinearMap.id_apply
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
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 ⋯)) LinearMap.id
⊢ 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)

Tactic:
apply DFunLike.congr_fun

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
h₁ :
  ∀ (m : F i) (n : N),
    Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
      (((((AlgebraTensorModule.curry (LinearMap.rTensor N (f ⋯)) :
                    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)
⊢ 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

Tactic:
ext m n
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
m : F i
n : N
⊢ Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor N (f ⋯)) :
                  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:
simp [D.map_self]

Premises used: DirectedSystem.map_self
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
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 ⋯) : (a : F k ⊗[R] N) → F i ⊗[R] N) 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 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)

Tactic:
rw [← comp_apply, ← rTensor_comp]

Premises used: LinearMap.comp_apply, LinearMap.rTensor_comp
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
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 ⋯))
⊢ 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)

Tactic:
apply DFunLike.congr_fun

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
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 ⋯)) :
                    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)
⊢ 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 ⋯))

Tactic:
ext p n
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
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
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 ⋯)) :
                  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:
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 (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 : ↥(↑x : Submodule R M) ⊗[R] N) → ↥(↑x_1 : Submodule R M) ⊗[R] N)

Tactic:
Submodule.FG.directedSystem.rTensor R N

Premises used: DirectedSystem.rTensor, 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 M // P.FG }
P : { P : Submodule R M // P.FG }
u : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
this :
  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:
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 M // P.FG }
P : { P : Submodule R M // P.FG }
u : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
this :
  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:
exact DFunLike.congr_fun this u

Premises used: DFunLike.congr_fun