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'₁
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
⊢ (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
Tactic:
ext
Proof state after:
case h.a
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
x✝ : ↥P
⊢ ↑(((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype) x✝) =
    ↑((Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j) x✝)
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
case h.a
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
x✝ : ↥P
⊢ ↑(((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype) x✝) =
    ↑((Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j) x✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
case h.a
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
x✝ : ↥P'
⊢ ↑(((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype) x✝) =
    ↑((Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j') x✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: Subalgebra.FG.sup
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
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A A' : Subalgebra R S
hA : A.FG
hA' : A'.FG
s : Set S
hs : s.Finite ∧ Algebra.adjoin R s = A
s' : Set S
hs' : s'.Finite ∧ Algebra.adjoin R s' = A'
⊢ Algebra.adjoin R (s ∪ s') = A ⊔ A'
Tactic:
rw [Algebra.adjoin_union, hs.2, hs'.2]
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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let A'' := A ⊔ A'
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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let hA_le := (le_sup_left : A ≤ A'')
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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let hA'_le := (le_sup_right : A' ≤ A'')
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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
have hj : (Subalgebra.val A'').comp (Subalgebra.inclusion hA_le)
  = Subalgebra.val A := by ext; 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
have hj' : (Subalgebra.val A'').comp (Subalgebra.inclusion hA'_le)
  = Subalgebra.val A' := by ext; 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
rw [← hj, ← hj'] at 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
h :
  (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA_le)).toLinearMap) t =
    (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA'_le)).toLinearMap) t'
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
h :
  (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA_le)).toLinearMap) t =
    (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA'_le)).toLinearMap) t'
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
simp only [AlgHom.comp_toLinearMap, LinearMap.rTensor_comp, LinearMap.comp_apply] at 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let ⟨B, hB_le, hB, h⟩ := TensorProduct.Algebra.eq_of_fg_of_subtype_eq
  (Subalgebra.FG.sup hA hA') _ _ 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
use B, le_trans hA_le hB_le, le_trans hA'_le hB_le, hB
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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'