internlm/Lean-Github huggingface dataset:
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Tactic:
rw [← Submodule.subtype_comp_inclusion P _ this,
  LinearMap.rTensor_comp] at ht
Proof state after:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
ht :
  t ∈
    LinearMap.range
      (LinearMap.rTensor N (Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ
        LinearMap.rTensor N (Submodule.inclusion this))
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
ht :
  t ∈
    LinearMap.range
      (LinearMap.rTensor N (Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ
        LinearMap.rTensor N (Submodule.inclusion this))
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Tactic:
exact LinearMap.range_comp_le_range _ _ ht
Proof state after:
no goals
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
Tactic:
simp only [← hs, Submodule.span_le, Subalgebra.coe_toSubmodule]
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ↑s ⊆ ↑(Algebra.adjoin R ↑s)
Theorem: TensorProduct.Algebra.exists_of_fg
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ↑s ⊆ ↑(Algebra.adjoin R ↑s)
Tactic:
exact Algebra.subset_adjoin
Proof state after:
no goals
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
classical
let ⟨P, hP, ⟨u, hu⟩⟩ := TensorProduct.exists_of_fg t
let ⟨P', hP', ⟨u', hu'⟩⟩ := TensorProduct.exists_of_fg t'
let P₁ := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
have hP₁ : Submodule.FG P₁ := Submodule.FG.map _ (Submodule.FG.sup hP hP')
let j : P →ₗ[R] P₁ := LinearMap.restrict (Subalgebra.toSubmodule A).subtype
    (fun p hp ↦ by
      simp only [Submodule.coeSubtype, Submodule.map_sup, P₁]
      apply Submodule.mem_sup_left
      use p; simp only [SetLike.mem_coe]; exact ⟨hp, rfl⟩)
let j' : P' →ₗ[R] P₁ := LinearMap.restrict (Subalgebra.toSubmodule A).subtype
    (fun p hp ↦ by
      simp only [Submodule.coeSubtype, Submodule.map_sup, P₁]
      apply Submodule.mem_sup_right
      use p; simp only [SetLike.mem_coe]; exact ⟨hp, rfl⟩)
set u₁ := LinearMap.rTensor N j u with hu₁
set u'₁ := LinearMap.rTensor N j' u' with hu'₁
have : LinearMap.rTensor N P₁.subtype u₁ = LinearMap.rTensor N P₁.subtype u'₁ := by
  rw [hu₁, hu'₁]
  simp only [← LinearMap.comp_apply, ← LinearMap.rTensor_comp]
  have hj₁ : P₁.subtype ∘ₗ j = (Subalgebra.val A).toLinearMap ∘ₗ P.subtype := by ext; rfl
  have hj'₁ : P₁.subtype ∘ₗ j' = (Subalgebra.val A).toLinearMap ∘ₗ P'.subtype := by ext; rfl
  rw [hj₁, hj'₁]
  simp only [LinearMap.rTensor_comp, LinearMap.comp_apply]
  rw [hu, hu', h]
let ⟨P'₁, hP₁_le, hP'₁, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq hP₁ _ _ this
let ⟨s, hs⟩ := hP'₁
let ⟨w, hw⟩ := hA
let B := Algebra.adjoin R ((s ∪ w : Finset S) : Set S)
have hBA : A ≤ B := by
  simp only [B, ← hw]
  apply Algebra.adjoin_mono
  simp only [Finset.coe_union, Set.subset_union_right]
use B, hBA, Subalgebra.fg_adjoin_finset _
rw [← hu, ← hu']
simp only [← LinearMap.comp_apply, ← LinearMap.rTensor_comp]
have hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B := by
  simp only [← hs, Finset.coe_union, Submodule.span_le, Subalgebra.coe_toSubmodule, B]
  exact subset_trans (Set.subset_union_left _ _) Algebra.subset_adjoin
have k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype
  = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j := by ext; rfl
have k' : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype
  = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j' := by ext; rfl
rw [k, k']
simp only [LinearMap.rTensor_comp, LinearMap.comp_apply]
rw [← hu₁, ← hu'₁, h]
Proof state after:
no goals
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let ⟨P, hP, ⟨u, hu⟩⟩ := TensorProduct.exists_of_fg t
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let ⟨P', hP', ⟨u', hu'⟩⟩ := TensorProduct.exists_of_fg t'
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let P₁ := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
have hP₁ : Submodule.FG P₁ := Submodule.FG.map _ (Submodule.FG.sup hP hP')
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let j : P →ₗ[R] P₁ := LinearMap.restrict (Subalgebra.toSubmodule A).subtype
    (fun p hp ↦ by
      simp only [Submodule.coeSubtype, Submodule.map_sup, P₁]
      apply Submodule.mem_sup_left
      use p; simp only [SetLike.mem_coe]; exact ⟨hp, rfl⟩)
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let j' : P' →ₗ[R] P₁ := LinearMap.restrict (Subalgebra.toSubmodule A).subtype
    (fun p hp ↦ by
      simp only [Submodule.coeSubtype, Submodule.map_sup, P₁]
      apply Submodule.mem_sup_right
      use p; simp only [SetLike.mem_coe]; exact ⟨hp, rfl⟩)
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
set u₁ := LinearMap.rTensor N j u with hu₁
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j) u
hu₁ : u₁ = (LinearMap.rTensor N j) u
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j) u
hu₁ : u₁ = (LinearMap.rTensor N j) u
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
set u'₁ := LinearMap.rTensor N j' u' with hu'₁
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j) u
hu₁ : u₁ = (LinearMap.rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j') u'
hu'₁ : u'₁ = (LinearMap.rTensor N j') u'
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j) u
hu₁ : u₁ = (LinearMap.rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j') u'
hu'₁ : u'₁ = (LinearMap.rTensor N j') u'
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
have : LinearMap.rTensor N P₁.subtype u₁ = LinearMap.rTensor N P₁.subtype u'₁ := by
  rw [hu₁, hu'₁]
  simp only [← LinearMap.comp_apply, ← LinearMap.rTensor_comp]
  have hj₁ : P₁.subtype ∘ₗ j = (Subalgebra.val A).toLinearMap ∘ₗ P.subtype := by ext; rfl
  have hj'₁ : P₁.subtype ∘ₗ j' = (Subalgebra.val A).toLinearMap ∘ₗ P'.subtype := by ext; rfl
  rw [hj₁, hj'₁]
  simp only [LinearMap.rTensor_comp, LinearMap.comp_apply]
  rw [hu, hu', h]
Proof state after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j) u
hu₁ : u₁ = (LinearMap.rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j') u'
hu'₁ : u'₁ = (LinearMap.rTensor N j') u'
this : (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'