internlm/Lean-Github huggingface dataset:
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'
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'
Tactic:
let ⟨P'₁, hP₁_le, hP'₁, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq hP₁ _ _ this
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) 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'
this : (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let ⟨s, hs⟩ := 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
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = 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')
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let ⟨w, hw⟩ := hA
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
⊢ ∃ 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'
this : (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
let B := Algebra.adjoin R ((s ∪ w : Finset S) : Set S)
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
⊢ ∃ 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'
this : (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
have hBA : A ≤ B := by
  simp only [B, ← hw]
  apply Algebra.adjoin_mono
  simp only [Finset.coe_union, Set.subset_union_right]
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ ∃ 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'
this : (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Tactic:
use B, hBA, Subalgebra.fg_adjoin_finset _
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
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
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
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) t'
Tactic:
rw [← hu, ← hu']
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
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) ((LinearMap.rTensor N P.subtype) u) =
    (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) ((LinearMap.rTensor N P'.subtype) u')
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
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
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) ((LinearMap.rTensor N P.subtype) u) =
    (LinearMap.rTensor N (Subalgebra.inclusion hBA).toLinearMap) ((LinearMap.rTensor N P'.subtype) u')
Tactic:
simp only [← LinearMap.comp_apply, ← LinearMap.rTensor_comp]
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
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'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
⊢ (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'