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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let A'' := A ⊔ A'
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let hA_le := (le_sup_left : A ≤ A'')
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let hA'_le := (le_sup_right : A' ≤ A'')
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
have hj : (Subalgebra.val A'').comp (Subalgebra.inclusion hA_le)
  = Subalgebra.val A := by ext; rfl
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
have hj' : (Subalgebra.val A'').comp (Subalgebra.inclusion hA'_le)
  = Subalgebra.val A' := by ext; rfl
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
rw [← hj, ← hj'] at h
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
h :
  (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA_le)).toLinearMap) t =
    (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA'_le)).toLinearMap) t'
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
h :
  (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA_le)).toLinearMap) t =
    (LinearMap.rTensor N (A''.val.comp (Subalgebra.inclusion hA'_le)).toLinearMap) t'
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
simp only [AlgHom.comp_toLinearMap, LinearMap.rTensor_comp, LinearMap.comp_apply] at h
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
let ⟨B, hB_le, hB, h⟩ := TensorProduct.Algebra.eq_of_fg_of_subtype_eq
  (Subalgebra.FG.sup hA hA') _ _ h
State after:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

State before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
          (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
Tactic:
use B, le_trans hA_le hB_le, le_trans hA'_le hB_le, hB
State after:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'

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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'
Tactic:
simp only [← LinearMap.rTensor_comp, ← LinearMap.comp_apply] at h
State after:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA_le).toLinearMap)) t =
    (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA'_le).toLinearMap)) t'
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA_le).toLinearMap)) t =
    (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA'_le).toLinearMap)) t'
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'
Tactic:
exact 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
⊢ A''.val.comp (Subalgebra.inclusion hA_le) = A.val
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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
x✝ : ↥A
⊢ (A''.val.comp (Subalgebra.inclusion hA_le)) x✝ = A.val 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
x✝ : ↥A
⊢ (A''.val.comp (Subalgebra.inclusion hA_le)) x✝ = A.val 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
⊢ A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
x✝ : ↥A'
⊢ (A''.val.comp (Subalgebra.inclusion hA'_le)) x✝ = A'.val 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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
x✝ : ↥A'
⊢ (A''.val.comp (Subalgebra.inclusion hA'_le)) x✝ = A'.val x✝
Tactic:
rfl
State after:
no goals