awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp : (↑s : Set S) ⊆ (↑(Algebra.adjoin R (↑s : Set S)) : Set S)
⊢ P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))

Tactic:
simp only [← hs, span_le, Subalgebra.coe_toSubmodule]

Premises used: Subalgebra.coe_toSubmodule, Submodule.span_le
-- 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
⊢ (↑s : Set S) ⊆ (↑(Algebra.adjoin R (↑s : Set S)) : Set S)

Tactic:
Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- 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
⊢ (↑s : Set S) ⊆ (↑(Algebra.adjoin R (↑s : Set S)) : Set S)

Tactic:
exact Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- 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
⊢ P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))

Tactic:
have : P ≤ (Algebra.adjoin R (s : Set S)).toSubmodule := by
    simp only [← hs, span_le, Subalgebra.coe_toSubmodule]
    exact Algebra.subset_adjoin
-- 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
this : P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))
⊢ Membership.mem (γ := Submodule R (S ⊗[R] N))
    (range
      (rTensor N
          (Submodule.subtype
            ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S)))) ∘ₗ
        rTensor N (inclusion this)))
    u

Tactic:
rw [← subtype_comp_inclusion P _ this, rTensor_comp] at hu

Premises used: Submodule.subtype_comp_inclusion, 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
P : Submodule R S
s : Finset S
hs : span R (↑s : Set S) = P
this : P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))
hu :
  Membership.mem (γ := Submodule R (S ⊗[R] N))
    (range
      (rTensor N
          (Submodule.subtype
            ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S)))) ∘ₗ
        rTensor N (inclusion this)))
    u
⊢ 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

Tactic:
range_comp_le_range _ _ hu

Premises used: Set.Mem, LinearMap.range_comp_le_range
-- 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
s : Finset S
hs : span R (↑s : Set S) = P
this : P ≤ (Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S))
hu :
  Membership.mem (γ := Submodule R (S ⊗[R] N))
    (range
      (rTensor N
          (Submodule.subtype
            ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S)))) ∘ₗ
        rTensor N (inclusion this)))
    u
⊢ 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

Tactic:
exact range_comp_le_range _ _ hu

Premises used: LinearMap.range_comp_le_range
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
H :
  ∀ (x : ↥A),
    Eq (α := S) (((A ⊔ A').val.comp (Subalgebra.inclusion ⋯) : (a : ↥A) → S) x : S) ((A.val : (a : ↥A) → S) x : S)
⊢ (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val

Tactic:
ext
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
x : ↥A
⊢ Eq (α := S) (((A ⊔ A').val.comp (Subalgebra.inclusion ⋯) : (a : ↥A) → S) x : S) ((A.val : (a : ↥A) → S) x : S)

Tactic:
rfl
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
⊢ (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val

Tactic:
have hj : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_left) = A.val := by ext; rfl
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
H :
  ∀ (x : ↥A'),
    Eq (α := S) (((A ⊔ A').val.comp (Subalgebra.inclusion ⋯) : (a : ↥A') → S) x : S) ((A'.val : (a : ↥A') → S) x : S)
⊢ (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val

Tactic:
ext
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
x : ↥A'
⊢ Eq (α := S) (((A ⊔ A').val.comp (Subalgebra.inclusion ⋯) : (a : ↥A') → S) x : S) ((A'.val : (a : ↥A') → S) x : S)

Tactic:
rfl
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
⊢ (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val

Tactic:
have hj' : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_right) = A'.val := by ext; rfl
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
h :
  Eq (α := S ⊗[R] N) ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) t : S ⊗[R] N)
    ((rTensor N A'.val.toLinearMap : (a : ↥A' ⊗[R] N) → S ⊗[R] N) t' : S ⊗[R] N)
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
      S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
      S ⊗[R] N)

Tactic:
simp only [← hj, ← hj', AlgHom.comp_toLinearMap, rTensor_comp, comp_apply] at h

Premises used: AlgHom.comp_toLinearMap, 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
h :
  Eq (α := S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
      S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
      S ⊗[R] N)
let :
  ∀ (B : Subalgebra R S) (hB_le : A ⊔ A' ≤ B) (hB : B.FG)
    (h :
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hB_le).toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → ↥B ⊗[R] N)
            ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hB_le).toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → ↥B ⊗[R] N)
            ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)),
    ∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
          ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
            TensorProduct.{u_1, u_2, u_4} R (↥B) N)
          ((rTensor N (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
            TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ ∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B),
    B.FG ∧
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)

Tactic:
let ⟨B, hB_le, hB, h⟩ := TensorProduct.Algebra.eq_of_fg_of_subtype_eq
    (Subalgebra.FG.sup hA hA') h
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
h_1 :
  Eq (α := S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
      S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
      S ⊗[R] N)
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion hB_le).toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → ↥B ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion hB_le).toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → ↥B ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
right :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ ∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B),
    B.FG ∧
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)

Tactic:
use B, le_trans le_sup_left hB_le, le_trans le_sup_right hB_le, hB

Premises used: le_sup_left, le_sup_right, le_trans
-- 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
A : Subalgebra R S
hA : A.FG
t : TensorProduct.{u_1, u_2, u_4} R (↥A) N
A' : Subalgebra R S
hA' : A'.FG
t' : TensorProduct.{u_1, u_2, u_4} R (↥A') N
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
h_1 :
  Eq (α := S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
      S ⊗[R] N)
    ((rTensor N (A ⊔ A').val.toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → S ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
      S ⊗[R] N)
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion hB_le).toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → ↥B ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t) :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion hB_le).toLinearMap : (a : ↥(A ⊔ A') ⊗[R] N) → ↥B ⊗[R] N)
        ((rTensor N (AlgHom.toLinearMap (Subalgebra.inclusion ⋯)) : (a : ↥A' ⊗[R] N) → ↥(A ⊔ A') ⊗[R] N) t') :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) t :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)
    ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A' ⊗[R] N) → ↥B ⊗[R] N) t' :
      TensorProduct.{u_1, u_2, u_4} R (↥B) N)

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

Premises used: LinearMap.comp_apply, LinearMap.rTensor_comp
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
obtain :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
⊢ ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t

Tactic:
obtain ⟨A, hA, ht_memA⟩ := TensorProduct.Algebra.exists_of_fg t

Premises used: TensorProduct.Algebra.exists_of_fg
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
obtain :
  ∀ (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M)
    (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
⊢ ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t

Tactic:
obtain ⟨u, hu⟩ := _root_.id ht_memA

Premises used: id
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
u : TensorProduct.{u_1, u_2, u_3} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
⊢ ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) 0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S) (hAB : A ≤ B),
      B.FG ∧
        Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
          ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
              ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
            TensorProduct.{u_1, u_2, u_4} R (↥B) N)
          ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) 0 :
            TensorProduct.{u_1, u_2, u_4} R (↥B) N)

Tactic:
have := TensorProduct.Algebra.eq_of_fg_of_subtype_eq hA (t := f.baseChange _ u) (t' := 0)
-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
A : Subalgebra R S
hA : A.FG
ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
u : TensorProduct.{u_1, u_2, u_3} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
this :
  ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) 0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S) (hAB : A ≤ B),
      B.FG ∧
        Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
          ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
              ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
            TensorProduct.{u_1, u_2, u_4} R (↥B) N)
          ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) 0 :
            TensorProduct.{u_1, u_2, u_4} R (↥B) N)
⊢ ∀
    (h :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N)),
    ∃ (B : Subalgebra R S),
      B.FG ∧
        ∃ (x : A ≤ B),
          Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              TensorProduct.{u_1, u_2, u_4} R (↥B) N)
            (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)

Tactic:
simp only [map_zero, exists_and_left] at this

Premises used: map_zero, exists_and_left