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
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
⊢ (LinearMap.mul T (A ⊗[S] C ⊗[R] D)).compr₂ ↑(AlgebraTensorModule.assoc R S T A C D) =
    (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)

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Algebra.Group.Pi.Units

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ MulEquiv.piUnits hx.unit i = ⋯.unit

Tactic:
ext

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i) = ↑⋯.unit
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
⊢ (mapRingHom fR fS fT HS HT).comp includeLeftRingHom = includeLeftRingHom.comp fS

Tactic:
ext

Goal state after:
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✝
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
⊢ (mapRingHom fR fS fT HS HT).comp ↑includeRight = (↑includeRight).comp fT

Tactic:
ext

Goal state after:
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✝
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
⊢ (↑(map f g)).comp includeLeftRingHom = includeLeftRingHom.comp ↑f

Tactic:
ext

Goal state after:
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✝
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
⊢ (↑(TensorProduct.comm R C D)).comp (map f g) = (map g f).comp ↑(TensorProduct.comm R A B)

Tactic:
ext

Goal state after:
case ha
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
x✝ : A
⊢ (((↑(TensorProduct.comm R C D)).comp (map f g)).comp includeLeft) x✝ =
    (((map g f).comp ↑(TensorProduct.comm R A B)).comp includeLeft) x✝

case hb
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
x✝ : B
⊢ ((AlgHom.restrictScalars R ((↑(TensorProduct.comm R C D)).comp (map f g))).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((map g f).comp ↑(TensorProduct.comm R A B))).comp includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ↑↑(leftComm R A B C) = ↑(_root_.TensorProduct.leftComm R A B C)

Tactic:
ext

Goal state after:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
x✝² : A
x✝¹ : B
x✝ : C
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry ↑↑(leftComm R A B C)) x✝²)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry ↑(_root_.TensorProduct.leftComm R A B C)) x✝²)) x✝¹) x✝
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ.toAlgHom = φ

Tactic:
ext

Goal state after:
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x✝ : A
⊢ ((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ.toAlgHom) x✝ = φ x✝
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
⊢ ((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ).toAlgHom = φ

Tactic:
ext

Goal state after:
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
x✝ : A
⊢ ((↑((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ).toAlgHom).comp (inrNonUnitalAlgHom R A)) x✝ =
    ((↑φ).comp (inrNonUnitalAlgHom R A)) x✝
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
⊢ ⇑(NonUnitalAlgHom.toAlgHom 0) = fun x ↦ x.toProd.1

Tactic:
ext

Goal state after:
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
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
⊢ (fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
      ((fun φ ↦
          let __AlgHom := lift φ.toNonUnitalAlgHom;
          { toAlgHom := __AlgHom, map_star' := ⋯ })
        x✝) =
    x✝

Tactic:
ext

Goal state after:
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✝
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
⊢ (fun φ ↦
        let __AlgHom := lift φ.toNonUnitalAlgHom;
        { toAlgHom := __AlgHom, map_star' := ⋯ })
      ((fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A)) x✝) =
    x✝

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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)
⊢ includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)

Tactic:
ext

Goal state after:
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✝
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
hφ : Function.Injective ⇑φ
x y : Unitization R A
h : (starMap φ) x = (starMap φ) y
⊢ x = y

Tactic:
ext

Goal state after:
case fst
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
hφ : Function.Injective ⇑φ
x y : Unitization R A
h : (starMap φ) x = (starMap φ) y
⊢ x.toProd.1 = y.toProd.1

case snd
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
hφ : Function.Injective ⇑φ
x y : Unitization R A
h : (starMap φ) x = (starMap φ) y
⊢ x.toProd.2 = y.toProd.2
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ lmul'' R = (↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul S R S S S)

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : S
⊢ ((AlgHom.restrictScalars R (lmul'' R)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul S R S S S))).comp includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ (lmul' R).comp (map f g) = lift f g ⋯

Tactic:
ext

Goal state after:
case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
x✝ : A
⊢ (((lmul' R).comp (map f g)).comp includeLeft) x✝ = ((lift f g ⋯).comp includeLeft) x✝

case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
x✝ : B
⊢ ((AlgHom.restrictScalars R ((lmul' R).comp (map f g))).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R (lift f g ⋯)).comp includeRight) x✝
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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✝⁶ : NonUnitalSemiring C
inst✝⁵ : StarRing C
inst✝⁴ : Module R C
inst✝³ : SMulCommClass R C C
inst✝² : IsScalarTower R C C
inst✝¹ : StarModule R B
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
⊢ starMap (ψ.comp φ) = (starMap ψ).comp (starMap φ)

Tactic:
ext

Goal state after:
case fst
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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✝⁶ : NonUnitalSemiring C
inst✝⁵ : StarRing C
inst✝⁴ : Module R C
inst✝³ : SMulCommClass R C C
inst✝² : IsScalarTower R C C
inst✝¹ : StarModule R B
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
x✝ : A
⊢ (((↑(starMap (ψ.comp φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.1 =
    (((↑((starMap ψ).comp (starMap φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.1

case snd
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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✝⁶ : NonUnitalSemiring C
inst✝⁵ : StarRing C
inst✝⁴ : Module R C
inst✝³ : SMulCommClass R C C
inst✝² : IsScalarTower R C C
inst✝¹ : StarModule R B
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
x✝ : A
⊢ (((↑(starMap (ψ.comp φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.2 =
    (((↑((starMap ψ).comp (starMap φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.2
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
⊢ starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)

Tactic:
ext

Goal state after:
case fst
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.1 =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.1

case snd
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.2 =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.2
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
⊢ ↑(lmulEquiv R S) = ↑(lidOfCompatibleSMul R S S)

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
x✝ : S
⊢ ((AlgHom.restrictScalars R ↑(lmulEquiv R S)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ↑(lidOfCompatibleSMul R S S)).comp includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ productMap f g = (lmul' R).comp (map f g)

Tactic:
ext

Goal state after:
case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
x✝ : A
⊢ ((productMap f g).comp includeLeft) x✝ = (((lmul' R).comp (map f g)).comp includeLeft) x✝

case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
x✝ : B
⊢ ((AlgHom.restrictScalars R (productMap f g)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((lmul' R).comp (map f g))).comp includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ lmul' (ULift.{u₁, u_4} R) =
    (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm

Tactic:
ext

Goal state after:
case ha
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((lmul' (ULift.{u₁, u_4} R)).comp includeLeft) x✝).down =
    ((((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm).comp
          includeLeft)
        x✝).down

case hb
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((AlgHom.restrictScalars (ULift.{u₁, u_4} R) (lmul' (ULift.{u₁, u_4} R))).comp includeRight) x✝).down =
    (((AlgHom.restrictScalars (ULift.{u₁, u_4} R)
              ((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp
                ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm)).comp
          includeRight)
        x✝).down