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 N // P.FG }
Q : { Q : Submodule R N // Q.FG }
u : TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N)
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)
⊢ 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:
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
-- 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)
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)
⊢ 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:
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 N // P.FG }
Q : { Q : Submodule R N // Q.FG }
u : TensorProduct.{u, u_1, u_2} R M ↥(↑Q : Submodule R N)
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:
simp [Submodule.FG.lTensor.directLimit, Submodule.FG.directLimit]

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

Tactic:
Submodule.FG.lTensor.directLimit_apply R M N ⟨Q, hQ⟩ u

Premises used: Set.Mem, Subtype.mk, Submodule.FG.lTensor.directLimit_apply
-- 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
u : M ⊗[R] N
let :
  ∀ (P : { P : Submodule R M // P.FG }) (t : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N)
    (ht :
      Eq (α :=
        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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        (((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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ 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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ 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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
            t :
          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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        ((LinearEquiv.symm (FG.rTensor.directLimit R M N) :
              (a : M ⊗[R] 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))
            u :
          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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))),
    ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u
⊢ ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u

Tactic:
let ⟨P, t, ht⟩ := Module.DirectLimit.exists_of ((Submodule.FG.rTensor.directLimit R M N).symm 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
u : M ⊗[R] N
P : { P : Submodule R M // P.FG }
t : TensorProduct.{u, u_1, u_2} R (↥(↑P : Submodule R M)) N
ht :
  Eq (α :=
    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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
    (((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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ 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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ 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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
        t :
      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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
    ((LinearEquiv.symm (FG.rTensor.directLimit R M N) :
          (a : M ⊗[R] 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))
        u :
      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 ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) ↦ rTensor N (inclusion h))
h : (rTensor N (↑P : Submodule R M).subtype : (a : ↥(↑P : Submodule R M) ⊗[R] N) → M ⊗[R] N) t = u
⊢ ∃ (P : Submodule R M), P.FG ∧ Membership.mem (γ := Submodule R (M ⊗[R] N)) (range (rTensor N P.subtype)) u

Tactic:
use P.val, P.property, t

Premises used: Subtype.val, Subtype.property
-- 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
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
h : Eq (α := M ⊗[R] N) ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N) (0 : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N) ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
    ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)

Tactic:
rw [← (rTensor N P.subtype).map_zero] at h

Premises used: LinearMap.map_zero, Submodule.subtype, LinearMap.rTensor
-- 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
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
h :
  Eq (α := M ⊗[R] N) ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
    ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)
⊢ ∃ (Q : Submodule R M) (hPQ : P ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        (0 : TensorProduct.{u, u_1, u_2} R (↥Q) N)

Tactic:
simpa only [map_zero] using TensorProduct.eq_of_fg_of_subtype_eq hP h

Premises used: map_zero, TensorProduct.eq_of_fg_of_subtype_eq
-- 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
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
P' : Submodule R M
hP' : P'.FG
t' : TensorProduct.{u, u_1, u_2} R (↥P') N
h :
  Eq (α := M ⊗[R] N) ((rTensor N P.subtype : (a : ↥P ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
    ((rTensor N P'.subtype : (a : ↥P' ⊗[R] N) → M ⊗[R] N) t' : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      M ⊗[R] N)

Tactic:
simp only [← subtype_comp_inclusion _ _ (le_sup_left : _ ≤ P ⊔ P'),
    ← subtype_comp_inclusion _ _ (le_sup_right : _ ≤ P ⊔ P'),
    rTensor_comp, coe_comp, Function.comp_apply] at h

Premises used: Submodule.subtype_comp_inclusion, le_sup_left, le_sup_right, LinearMap.coe_comp, LinearMap.rTensor_comp, Function.comp_apply
-- 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
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
P' : Submodule R M
hP' : P'.FG
t' : TensorProduct.{u, u_1, u_2} R (↥P') N
h :
  Eq (α := M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      M ⊗[R] N)
let :
  ∀ (Q : Submodule R M) (hQ_le : P ⊔ P' ≤ Q) (hQ : Q.FG)
    (h :
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
            ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
          TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
            ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
          TensorProduct.{u, u_1, u_2} R (↥Q) N)),
    ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧
        Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
          ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
          ((rTensor N (inclusion hP'Q) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)
⊢ ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hP'Q) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)

Tactic:
let ⟨Q, hQ_le, hQ, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq (hP.sup hP') h
-- 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
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
P' : Submodule R M
hP' : P'.FG
t' : TensorProduct.{u, u_1, u_2} R (↥P') N
h_1 :
  Eq (α := M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      M ⊗[R] N)
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      TensorProduct.{u, u_1, u_2} R (↥Q) N)
right :
  Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)
⊢ ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
    Q.FG ∧
      Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hPQ) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
        ((rTensor N (inclusion hP'Q) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)

Tactic:
use Q, le_trans le_sup_left hQ_le, le_trans le_sup_right hQ_le, hQ

Premises used: le_sup_left, le_sup_right, le_trans
-- 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
P : Submodule R M
hP : P.FG
t : TensorProduct.{u, u_1, u_2} R (↥P) N
P' : Submodule R M
hP' : P'.FG
t' : TensorProduct.{u, u_1, u_2} R (↥P') N
h_1 :
  Eq (α := M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      M ⊗[R] N)
    ((rTensor N (P ⊔ P').subtype : (a : ↥(P ⊔ P') ⊗[R] N) → M ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      M ⊗[R] N)
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t) :
      TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion hQ_le) : (a : ↥(P ⊔ P') ⊗[R] N) → ↥Q ⊗[R] N)
        ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥(P ⊔ P') ⊗[R] N) t') :
      TensorProduct.{u, u_1, u_2} R (↥Q) N)
⊢ Eq (α := TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion ⋯) : (a : ↥P ⊗[R] N) → ↥Q ⊗[R] N) t : TensorProduct.{u, u_1, u_2} R (↥Q) N)
    ((rTensor N (inclusion ⋯) : (a : ↥P' ⊗[R] N) → ↥Q ⊗[R] N) t' : TensorProduct.{u, u_1, u_2} R (↥Q) N)

Tactic:
simpa [← comp_apply, ← rTensor_comp] using h

Premises used: LinearMap.comp_apply, LinearMap.rTensor_comp
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : S ⊗[R] N
obtain :
  ∀ (P : Submodule R S) (hu : Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N P.subtype)) u)
    (s : Finset S) (hs : span R (↑s : Set S) = P),
    ∃ (A : Subalgebra R S), A.FG ∧ Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N A.val.toLinearMap)) u
⊢ ∃ (A : Subalgebra R S), A.FG ∧ Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N A.val.toLinearMap)) u

Tactic:
obtain ⟨P, ⟨s, hs⟩, hu⟩ := TensorProduct.exists_of_fg u

Premises used: TensorProduct.exists_of_fg
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid N
inst_4 : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N P.subtype)) u
s : Finset S
hs : span R (↑s : Set S) = P
right :
  Membership.mem (γ := Submodule R (S ⊗[R] N))
    (range (M := TensorProduct.{u_1, u_2, u_4} R (↥(Algebra.adjoin R (↑s : Set S))) N)
      (rTensor N (AlgHom.toLinearMap (Subalgebra.val (Algebra.adjoin R (↑s : Set S))))))
    u
⊢ ∃ (A : Subalgebra R S), A.FG ∧ Membership.mem (γ := Submodule R (S ⊗[R] N)) (range (rTensor N A.val.toLinearMap)) u

Tactic:
use Algebra.adjoin R s, Subalgebra.fg_adjoin_finset _

Premises used: Algebra.adjoin, Subalgebra.fg_adjoin_finset