mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R✝ : Type uR
R' : Type u_1
S✝ : Type uS
T✝ : Type u_2
A✝ : Type uA
B✝ : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝³⁴ : CommSemiring R✝
inst✝³³ : CommSemiring S✝
inst✝³² : Algebra R✝ S✝
inst✝³¹ : Semiring A✝
inst✝³⁰ : Algebra R✝ A✝
inst✝²⁹ : Algebra S✝ A✝
inst✝²⁸ : IsScalarTower R✝ S✝ A✝
inst✝²⁷ : Semiring B✝
inst✝²⁶ : Algebra R✝ B✝
inst✝²⁵ : Semiring C
inst✝²⁴ : Algebra R✝ C
inst✝²³ : Algebra S✝ C
inst✝²² : IsScalarTower R✝ S✝ C
inst✝²¹ : Semiring D
inst✝²⁰ : Algebra R✝ D
inst✝¹⁹ : Semiring E
inst✝¹⁸ : Algebra R✝ E
inst✝¹⁷ : Algebra S✝ E
inst✝¹⁶ : IsScalarTower R✝ S✝ E
inst✝¹⁵ : Semiring F
inst✝¹⁴ : Algebra R✝ F
R : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra S A
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra T A
inst✝³ : SMulCommClass R T A
inst✝² : SMulCommClass S T A
inst✝¹ : SMulCommClass R S A
inst✝ : CompatibleSMul R S A B
x : A ⊗[S] B
x✝¹ : A
x✝ : B
y : A ⊗[S] B
⊢ (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ ⊗ₜ[S] x✝ * 0) =
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ ⊗ₜ[S] x✝) *
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ {0} = {r | ¬IsUnit r}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R✝ : Type uR
R' : Type u_1
S✝ : Type uS
T✝ : Type u_2
A✝ : Type uA
B✝ : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝³⁴ : CommSemiring R✝
inst✝³³ : CommSemiring S✝
inst✝³² : Algebra R✝ S✝
inst✝³¹ : Semiring A✝
inst✝³⁰ : Algebra R✝ A✝
inst✝²⁹ : Algebra S✝ A✝
inst✝²⁸ : IsScalarTower R✝ S✝ A✝
inst✝²⁷ : Semiring B✝
inst✝²⁶ : Algebra R✝ B✝
inst✝²⁵ : Semiring C
inst✝²⁴ : Algebra R✝ C
inst✝²³ : Algebra S✝ C
inst✝²² : IsScalarTower R✝ S✝ C
inst✝²¹ : Semiring D
inst✝²⁰ : Algebra R✝ D
inst✝¹⁹ : Semiring E
inst✝¹⁸ : Algebra R✝ E
inst✝¹⁷ : Algebra S✝ E
inst✝¹⁶ : IsScalarTower R✝ S✝ E
inst✝¹⁵ : Semiring F
inst✝¹⁴ : Algebra R✝ F
R : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra S A
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra T A
inst✝³ : SMulCommClass R T A
inst✝² : SMulCommClass S T A
inst✝¹ : SMulCommClass R S A
inst✝ : CompatibleSMul R S A B
x : A ⊗[S] B
x✝¹ : A
x✝ : B
y : A ⊗[S] B
⊢ ∀ (x : A) (y : B),
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ ⊗ₜ[S] x✝ * x ⊗ₜ[S] y) =
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ ⊗ₜ[S] x✝) *
        (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x ⊗ₜ[S] y)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring S
inst✝²⁴ : Algebra R S
inst✝²³ : Semiring A
inst✝²² : Algebra R A
inst✝²¹ : Algebra S A
inst✝²⁰ : IsScalarTower R S A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : Semiring C
inst✝¹⁶ : Algebra R C
inst✝¹⁵ : Algebra S C
inst✝¹⁴ : IsScalarTower R S C
inst✝¹³ : Semiring D
inst✝¹² : Algebra R D
inst✝¹¹ : Semiring E
inst✝¹⁰ : Algebra R E
inst✝⁹ : Algebra S E
inst✝⁸ : IsScalarTower R S E
inst✝⁷ : Semiring F
inst✝⁶ : Algebra R F
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : Algebra T A
inst✝¹ : IsScalarTower R T A
inst✝ : IsScalarTower S T A
x✝⁵ : A
x✝⁴ : C
x✝³ : D
x✝² : A
x✝¹ : C
x✝ : D
⊢ (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              ((((AlgebraTensorModule.curry
                      (AlgebraTensorModule.curry
                        ((LinearMap.mul T (A ⊗[S] C ⊗[R] D)).compr₂ ↑(AlgebraTensorModule.assoc R S T A C D))))
                    x✝⁵)
                  x✝⁴)
                x✝³)))
          x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              ((((AlgebraTensorModule.curry
                      (AlgebraTensorModule.curry
                        ((LinearMap.mul T (A ⊗[S] (C ⊗[R] D)) ∘ₗ ↑(AlgebraTensorModule.assoc R S T A C D)).compl₂
                          ↑(AlgebraTensorModule.assoc R S T A C D))))
                    x✝⁵)
                  x✝⁴)
                x✝³)))
          x✝²)
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T✝ : Type u_2
A✝ : Type uA
B✝ : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝³² : CommSemiring R
inst✝³¹ : CommSemiring S
inst✝³⁰ : Algebra R S
inst✝²⁹ : Semiring A✝
inst✝²⁸ : Algebra R A✝
inst✝²⁷ : Algebra S A✝
inst✝²⁶ : IsScalarTower R S A✝
inst✝²⁵ : Semiring B✝
inst✝²⁴ : Algebra R B✝
inst✝²³ : Semiring C
inst✝²² : Algebra R C
inst✝²¹ : Algebra S C
inst✝²⁰ : IsScalarTower R S C
inst✝¹⁹ : Semiring D
inst✝¹⁸ : Algebra R D
inst✝¹⁷ : Semiring E
inst✝¹⁶ : Algebra R E
inst✝¹⁵ : Algebra S E
inst✝¹⁴ : IsScalarTower R S E
inst✝¹³ : Semiring F
inst✝¹² : Algebra R F
T : Type u_3
A : Type u_4
B : Type u_5
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring A
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra T A
inst✝⁴ : IsScalarTower R T A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Algebra S T
inst✝ : IsScalarTower S T A
x✝³ x✝² : A
x✝¹ x✝ : B
⊢ ↑(AlgebraTensorModule.cancelBaseChange R S T A B).symm ((x✝³ * x✝²) ⊗ₜ[R] (x✝¹ * x✝)) =
    ↑(AlgebraTensorModule.cancelBaseChange R S T A B).symm (x✝³ ⊗ₜ[R] x✝¹) *
      ↑(AlgebraTensorModule.cancelBaseChange R S T A B).symm (x✝² ⊗ₜ[R] x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
s : S
t : T
⊢ (mapRingHom fR fS fT HS HT) (s ⊗ₜ[R] t) = (fS s * 1) ⊗ₜ[R'] (1 * fT t)

Tactic:
dsimp [mapRingHom, lift_tmul, algebraMap]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
s : S
t : T
⊢ (fS s * 1) ⊗ₜ[R'] (1 * fT t) = fS s ⊗ₜ[R'] fT t

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
x✝ : S
⊢ ((mapRingHom fR fS fT HS HT).comp includeLeftRingHom) x✝ = (includeLeftRingHom.comp fS) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
x✝ : T
⊢ ((mapRingHom fR fS fT HS HT).comp ↑includeRight) x✝ = ((↑includeRight).comp fT) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Semiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra S A
inst✝¹⁴ : IsScalarTower R S A
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R C
inst✝⁹ : Algebra S C
inst✝⁸ : IsScalarTower R S C
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Semiring E
inst✝⁴ : Algebra R E
inst✝³ : Algebra S E
inst✝² : IsScalarTower R S E
inst✝¹ : Semiring F
inst✝ : Algebra R F
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) (a₁ ⊗ₜ[R] b₁) *
        (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) (a₂ ⊗ₜ[R] b₂)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ ∀ (x : A), ((map f g).comp includeLeft) x = (includeLeft.comp f) x

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
x✝ : A
⊢ ((↑(map f g)).comp includeLeftRingHom) x✝ = (includeLeftRingHom.comp ↑f) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ ∀ (x : B), ((AlgHom.restrictScalars R (map f g)).comp includeRight) x = (includeRight.comp g) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : SMulZeroClass R A
r₁ r₂ : R
⊢ (inl (r₁ * r₂)).toProd.2 = (inl r₁ * inl r₂).toProd.2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : MulZeroClass R
inst✝² : AddZeroClass A
inst✝¹ : Mul A
inst✝ : SMulWithZero R A
a₁ a₂ : A
⊢ (↑(a₁ * a₂)).toProd.2 = (↑a₁ * ↑a₂).toProd.2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : MulZeroClass R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : SMulZeroClass R A
r : R
a : A
⊢ (inl r * ↑a).toProd.2 = (↑(r • a)).toProd.2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : MulZeroClass R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : SMulZeroClass R A
r : R
a : A
⊢ (↑a * inl r).toProd.2 = (↑(r • a)).toProd.2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
x : Unitization R A
⊢ (1 * x).toProd.2 = x.toProd.2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
x : Unitization R A
⊢ (x * 1).toProd.2 = x.toProd.2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
x✝ : Unitization R A
⊢ (0 * x✝).toProd.2 = (toProd 0).2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
x✝ : Unitization R A
⊢ (x✝ * 0).toProd.2 = (toProd 0).2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
x✝¹ : R
x✝ : Unitization R A
⊢ (star (x✝¹ • x✝)).toProd.1 = (star x✝¹ • star x✝).toProd.1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
x✝¹ : R
x✝ : Unitization R A
⊢ (star (x✝¹ • x✝)).toProd.2 = (star x✝¹ • star x✝).toProd.2

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
⊢ (map f g).range = (includeLeft.comp f).range ⊔ (includeRight.comp g).range

Tactic:
apply le_antisymm
  · rw [← map_top, ← adjoin_tmul_eq_top, ← adjoin_image, adjoin_le_iff]
    rintro _ ⟨_, ⟨a, b, rfl⟩, rfl⟩
    rw [map_tmul, ← mul_one (f a), ← one_mul (g b), ← tmul_mul_tmul]
    exact mul_mem_sup (AlgHom.mem_range_self _ a) (AlgHom.mem_range_self _ b)
  · rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]
    exact sup_le (AlgHom.range_comp_le_range _ _) (AlgHom.range_comp_le_range _ _)

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Semiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra S A
inst✝¹⁴ : IsScalarTower R S A
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R C
inst✝⁹ : Algebra S C
inst✝⁸ : IsScalarTower R S C
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Semiring E
inst✝⁴ : Algebra R E
inst✝³ : Algebra S E
inst✝² : IsScalarTower R S E
inst✝¹ : Semiring F
inst✝ : Algebra R F
f : A ≃ₐ[S] C
g : B ≃ₐ[R] D
b : C
d : D
⊢ ((map ↑f ↑g).comp (map ↑f.symm ↑g.symm)) (b ⊗ₜ[R] d) = (AlgHom.id S (C ⊗[R] D)) (b ⊗ₜ[R] d)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Semiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra S A
inst✝¹⁴ : IsScalarTower R S A
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R C
inst✝⁹ : Algebra S C
inst✝⁸ : IsScalarTower R S C
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Semiring E
inst✝⁴ : Algebra R E
inst✝³ : Algebra S E
inst✝² : IsScalarTower R S E
inst✝¹ : Semiring F
inst✝ : Algebra R F
f : A ≃ₐ[S] C
g : B ≃ₐ[R] D
a : A
c : B
⊢ ((map ↑f.symm ↑g.symm).comp (map ↑f ↑g)) (a ⊗ₜ[R] c) = (AlgHom.id S (A ⊗[R] B)) (a ⊗ₜ[R] c)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x✝ : Unitization R A
⊢ (NonUnitalAlgHom.toAlgHom 0) x✝ = x✝.toProd.1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
x✝¹ : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
        ((fun φ ↦
            let __AlgHom := lift φ.toNonUnitalAlgHom;
            { toAlgHom := __AlgHom, map_star' := ⋯ })
          x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝³⁷ : CommSemiring R
inst✝³⁶ : CommSemiring S
inst✝³⁵ : Algebra R S
inst✝³⁴ : Semiring A
inst✝³³ : Algebra R A
inst✝³² : Algebra S A
inst✝³¹ : IsScalarTower R S A
inst✝³⁰ : Semiring B
inst✝²⁹ : Algebra R B
inst✝²⁸ : Semiring C
inst✝²⁷ : Algebra R C
inst✝²⁶ : Algebra S C
inst✝²⁵ : IsScalarTower R S C
inst✝²⁴ : Semiring D
inst✝²³ : Algebra R D
inst✝²² : Semiring E
inst✝²¹ : Algebra R E
inst✝²⁰ : Algebra S E
inst✝¹⁹ : IsScalarTower R S E
inst✝¹⁸ : Semiring F
inst✝¹⁷ : Algebra R F
inst✝¹⁶ : CommSemiring T
inst✝¹⁵ : Algebra R T
inst✝¹⁴ : Algebra T A
inst✝¹³ : IsScalarTower R T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : Algebra S T
inst✝¹⁰ : IsScalarTower S T A
inst✝⁹ : CommSemiring R'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R' T
inst✝⁶ : Algebra R' A
inst✝⁵ : Algebra R' B
inst✝⁴ : IsScalarTower R R' A
inst✝³ : SMulCommClass S R' A
inst✝² : SMulCommClass R' S A
inst✝¹ : IsScalarTower R' T A
inst✝ : IsScalarTower R R' B
x✝⁷ : A
x✝⁶ : B
x✝⁵ : C
x✝⁴ : D
x✝³ : A
x✝² : B
x✝¹ : C
x✝ : D
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                        (((AlgebraTensorModule.curry
                              (AlgebraTensorModule.curry
                                ((LinearMap.mul T (A ⊗[R'] B ⊗[S] (C ⊗[R] D))).compr₂
                                  ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D))))
                            x✝⁷)
                          x✝⁶))
                      x✝⁵)
                    x✝⁴)))
              x✝³)
            x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                        (((AlgebraTensorModule.curry
                              (AlgebraTensorModule.curry
                                ((LinearMap.mul T (A ⊗[S] C ⊗[R'] (B ⊗[R] D)) ∘ₗ
                                      ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D)).compl₂
                                  ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D))))
                            x✝⁷)
                          x✝⁶))
                      x✝⁵)
                    x✝⁴)))
              x✝³)
            x✝²))
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
x✝¹ : Unitization R A →⋆ₐ[R] C
x✝ : A
⊢ ((↑((fun φ ↦
                let __AlgHom := lift φ.toNonUnitalAlgHom;
                { toAlgHom := __AlgHom, map_star' := ⋯ })
              ((fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A)) x✝¹))).comp
        (inrNonUnitalStarAlgHom R A))
      x✝ =
    ((↑x✝¹).comp (inrNonUnitalStarAlgHom R A)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
a : A
⊢ (starMap φ) ↑a = ↑(φ a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
r : R
⊢ (starMap φ) (inl r) = (algebraMap R (Unitization R B)) r

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
x✝ : A
⊢ ((includeLeft.comp ↑(TensorProduct.rid R S A)).comp includeLeft) x✝ =
    ((map (AlgHom.id S A) (ofId R B)).comp includeLeft) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
s : S
x : S ⊗[R] S
⊢ (LinearMap.mul' R S).toFun (s • 0) = (RingHom.id S) s • (LinearMap.mul' R S).toFun 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (let __spread.0 := LinearMap.mul' R S;
      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
      (1 ⊗ₜ[R] 1) =
    1

Tactic:
simp

Goal state after: