Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq (DividedPowers/ForMathlib/DirectLimit.lean)

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]
State after:
no goals

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
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'

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'
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'

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')
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'

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')
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'

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⟩)
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'

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⟩)
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'

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₁
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'

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'₁
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'

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]
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'

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
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'

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'₁
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'

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
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'

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)
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'

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]
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'

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 _
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'

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']
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')

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]
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'

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 ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'
Tactic:
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
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
⊢ (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'

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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
⊢ (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'
Tactic:
have k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype
  = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j := by ext; rfl
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
⊢ (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'

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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
⊢ (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'
Tactic:
have k' : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype
  = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j' := by ext; rfl
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
k' :
  (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
⊢ (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'

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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
k' :
  (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
⊢ (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (LinearMap.rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'
Tactic:
rw [k, k']
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
k' :
  (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
⊢ (LinearMap.rTensor N (Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j)) u =
    (LinearMap.rTensor N (Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j')) u'

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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
k' :
  (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
⊢ (LinearMap.rTensor N (Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j)) u =
    (LinearMap.rTensor N (Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j')) u'
Tactic:
simp only [LinearMap.rTensor_comp, LinearMap.comp_apply]
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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
k' :
  (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
⊢ (LinearMap.rTensor N (Submodule.inclusion hP'₁_le))
      ((LinearMap.rTensor N (Submodule.inclusion hP₁_le)) ((LinearMap.rTensor N j) u)) =
    (LinearMap.rTensor N (Submodule.inclusion hP'₁_le))
      ((LinearMap.rTensor N (Submodule.inclusion hP₁_le)) ((LinearMap.rTensor N j') u'))

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
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
k' :
  (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
⊢ (LinearMap.rTensor N (Submodule.inclusion hP'₁_le))
      ((LinearMap.rTensor N (Submodule.inclusion hP₁_le)) ((LinearMap.rTensor N j) u)) =
    (LinearMap.rTensor N (Submodule.inclusion hP'₁_le))
      ((LinearMap.rTensor N (Submodule.inclusion hP₁_le)) ((LinearMap.rTensor N j') u'))
Tactic:
rw [← hu₁, ← hu'₁, h]
State after:
no goals

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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ (Subalgebra.toSubmodule A).subtype p ∈ P₁
Tactic:
simp only [Submodule.coeSubtype, Submodule.map_sup, P₁]
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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P ⊔ Submodule.map (Subalgebra.toSubmodule A).subtype P'

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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P ⊔ Submodule.map (Subalgebra.toSubmodule A).subtype P'
Tactic:
apply Submodule.mem_sup_left
State after:
case 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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P

State before:
case 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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P
Tactic:
use p
State after:
case h
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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ p ∈ ↑P ∧ (Subalgebra.toSubmodule A).subtype p = ↑p

State before:
case h
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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ p ∈ ↑P ∧ (Subalgebra.toSubmodule A).subtype p = ↑p
Tactic:
simp only [SetLike.mem_coe]
State after:
case h
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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ p ∈ P ∧ (Subalgebra.toSubmodule A).subtype p = ↑p

State before:
case h
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
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ p ∈ P ∧ (Subalgebra.toSubmodule A).subtype p = ↑p
Tactic:
exact ⟨hp, rfl⟩
State after:
no goals

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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ (Subalgebra.toSubmodule A).subtype p ∈ P₁
Tactic:
simp only [Submodule.coeSubtype, Submodule.map_sup, P₁]
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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P ⊔ Submodule.map (Subalgebra.toSubmodule A).subtype P'

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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P ⊔ Submodule.map (Subalgebra.toSubmodule A).subtype P'
Tactic:
apply Submodule.mem_sup_right
State after:
case 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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P'

State before:
case 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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ ↑p ∈ Submodule.map (Subalgebra.toSubmodule A).subtype P'
Tactic:
use p
State after:
case h
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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ p ∈ ↑P' ∧ (Subalgebra.toSubmodule A).subtype p = ↑p

State before:
case h
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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ p ∈ ↑P' ∧ (Subalgebra.toSubmodule A).subtype p = ↑p
Tactic:
simp only [SetLike.mem_coe]
State after:
case h
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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ p ∈ P' ∧ (Subalgebra.toSubmodule A).subtype p = ↑p

State before:
case h
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 ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ p ∈ P' ∧ (Subalgebra.toSubmodule A).subtype p = ↑p
Tactic:
exact ⟨hp, rfl⟩
State after:
no goals

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'
⊢ (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
Tactic:
rw [hu₁, hu'₁]
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'
⊢ (LinearMap.rTensor N P₁.subtype) ((LinearMap.rTensor N j) u) =
    (LinearMap.rTensor N P₁.subtype) ((LinearMap.rTensor N j') u')

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'
⊢ (LinearMap.rTensor N P₁.subtype) ((LinearMap.rTensor N j) u) =
    (LinearMap.rTensor N P₁.subtype) ((LinearMap.rTensor N j') u')
Tactic:
simp only [← LinearMap.comp_apply, ← LinearMap.rTensor_comp]
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'
⊢ (LinearMap.rTensor N (P₁.subtype ∘ₗ j)) u = (LinearMap.rTensor N (P₁.subtype ∘ₗ j')) u'

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'
⊢ (LinearMap.rTensor N (P₁.subtype ∘ₗ j)) u = (LinearMap.rTensor N (P₁.subtype ∘ₗ j')) u'
Tactic:
have hj₁ : P₁.subtype ∘ₗ j = (Subalgebra.val A).toLinearMap ∘ₗ P.subtype := by ext; rfl
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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
⊢ (LinearMap.rTensor N (P₁.subtype ∘ₗ j)) u = (LinearMap.rTensor N (P₁.subtype ∘ₗ j')) u'

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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
⊢ (LinearMap.rTensor N (P₁.subtype ∘ₗ j)) u = (LinearMap.rTensor N (P₁.subtype ∘ₗ j')) u'
Tactic:
have hj'₁ : P₁.subtype ∘ₗ j' = (Subalgebra.val A).toLinearMap ∘ₗ P'.subtype := by ext; rfl
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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (LinearMap.rTensor N (P₁.subtype ∘ₗ j)) u = (LinearMap.rTensor N (P₁.subtype ∘ₗ j')) u'

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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (LinearMap.rTensor N (P₁.subtype ∘ₗ j)) u = (LinearMap.rTensor N (P₁.subtype ∘ₗ j')) u'
Tactic:
rw [hj₁, hj'₁]
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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (LinearMap.rTensor N (A.val.toLinearMap ∘ₗ P.subtype)) u = (LinearMap.rTensor N (A.val.toLinearMap ∘ₗ P'.subtype)) u'

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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (LinearMap.rTensor N (A.val.toLinearMap ∘ₗ P.subtype)) u = (LinearMap.rTensor N (A.val.toLinearMap ∘ₗ P'.subtype)) u'
Tactic:
simp only [LinearMap.rTensor_comp, LinearMap.comp_apply]
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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (LinearMap.rTensor N A.val.toLinearMap) ((LinearMap.rTensor N P.subtype) u) =
    (LinearMap.rTensor N A.val.toLinearMap) ((LinearMap.rTensor N P'.subtype) u')

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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (LinearMap.rTensor N A.val.toLinearMap) ((LinearMap.rTensor N P.subtype) u) =
    (LinearMap.rTensor N A.val.toLinearMap) ((LinearMap.rTensor N P'.subtype) u')
Tactic:
rw [hu, hu', h]
State after:
no goals

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'
⊢ P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
Tactic:
ext
State after:
case h
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'
x✝ : ↥P
⊢ (P₁.subtype ∘ₗ j) x✝ = (A.val.toLinearMap ∘ₗ P.subtype) x✝

State before:
case h
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'
x✝ : ↥P
⊢ (P₁.subtype ∘ₗ j) x✝ = (A.val.toLinearMap ∘ₗ P.subtype) x✝
Tactic:
rfl
State after:
no goals

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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
⊢ P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
Tactic:
ext
State after:
case h
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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
x✝ : ↥P'
⊢ (P₁.subtype ∘ₗ j') x✝ = (A.val.toLinearMap ∘ₗ P'.subtype) x✝

State before:
case h
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'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
x✝ : ↥P'
⊢ (P₁.subtype ∘ₗ j') x✝ = (A.val.toLinearMap ∘ₗ P'.subtype) x✝
Tactic:
rfl
State after:
no goals

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)
⊢ A ≤ B
Tactic:
simp only [B, ← hw]
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)
⊢ Algebra.adjoin R ↑w ≤ Algebra.adjoin R ↑(s ∪ w)

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)
⊢ Algebra.adjoin R ↑w ≤ Algebra.adjoin R ↑(s ∪ w)
Tactic:
apply Algebra.adjoin_mono
State after:
case H
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)
⊢ ↑w ⊆ ↑(s ∪ w)

State before:
case H
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)
⊢ ↑w ⊆ ↑(s ∪ w)
Tactic:
simp only [Finset.coe_union, Set.subset_union_right]
State after:
no goals

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
⊢ P'₁ ≤ Subalgebra.toSubmodule B
Tactic:
simp only [← hs, Finset.coe_union, Submodule.span_le, Subalgebra.coe_toSubmodule, B]
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
⊢ ↑s ⊆ ↑(Algebra.adjoin R (↑s ∪ ↑w))

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
⊢ ↑s ⊆ ↑(Algebra.adjoin R (↑s ∪ ↑w))
Tactic:
exact subset_trans (Set.subset_union_left _ _) Algebra.subset_adjoin
State after:
no goals

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
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✝)

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
State after:
no goals

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
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
⊢ (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
Tactic:
ext
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
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✝)

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
State after:
no goals