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
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:
by

Goal state after:
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
⊢ IsUnit x ↔ ∀ (i : ι), IsUnit (x i)

Tactic:
by

Goal state after:
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
inst✝ : ∀ (i : ι), Subsingleton (M i)ˣ
⊢ ∀ (a : (i : ι) → M i), IsUnit a → a = 1

Tactic:
by

Goal state after:
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 : ι
⊢ ↑hx.unit⁻¹ i = ↑⋯.unit⁻¹

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : ι → Type u_5
inst✝ : (i : ι) → NonUnitalSemiring (κ i)
x : (i : ι) → κ i
⊢ IsQuasiregular x ↔ ∀ (i : ι), IsQuasiregular (x i)

Tactic:
by

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

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝¹ : NonUnitalSemiring A
inst✝ : NonUnitalSemiring B
a : A
b : B
⊢ IsQuasiregular (a, b) ↔ IsQuasiregular a ∧ IsQuasiregular b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Ring (κ i)
inst✝ : (i : ι) → Algebra R (κ i)
a : (i : ι) → κ i
⊢ (resolventSet R a)ᶜᶜ = (⋃ i, (resolventSet R (a i))ᶜ)ᶜ

Tactic:
Set.compl_iUnion,

Goal state after:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Ring (κ i)
inst✝ : (i : ι) → Algebra R (κ i)
a : (i : ι) → κ i
⊢ (resolventSet R a)ᶜᶜ = ⋂ i, (resolventSet R (a i))ᶜᶜ
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Ring (κ i)
inst✝ : (i : ι) → Algebra R (κ i)
a : (i : ι) → κ i
⊢ spectrum R a = ⋃ i, spectrum R (a i)

Tactic:
by

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

Goal state before:
pp: A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
a : A
b : B
⊢ spectrum R (a, b) = spectrum R a ∪ spectrum R b

Tactic:
by

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 ⊗ₜ[R'] fT t

Tactic:
by

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
⊢ (mapRingHom fR fS fT HS HT).comp includeLeftRingHom = includeLeftRingHom.comp fS

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
⊢ quasispectrum R a = ⋃ i, quasispectrum R (a i)

Tactic:
by

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:
by

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
⊢ (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) (1 ⊗ₜ[R] 1) = 1

Tactic:
by

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:
by

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

Goal state before:
pp: A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : NonUnitalRing B
inst✝¹ : Module R A
inst✝ : Module R B
a : A
b : B
⊢ quasispectrum R (a, b) = quasispectrum R a ∪ quasispectrum R b

Tactic:
by

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
⊢ (↑(map f g)).comp includeLeftRingHom = includeLeftRingHom.comp ↑f

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : αᵐᵒᵖ
hab : a ≤ b
c : αᵐᵒᵖ
⊢ unop a ≤ unop b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : αᵐᵒᵖ
hab : a ≤ b
c : αᵐᵒᵖ
⊢ unop a ≤ unop b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : αᵃᵒᵖ
hab : a ≤ b
c : αᵃᵒᵖ
⊢ unop a ≤ unop b

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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:
by

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:
by

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✝² x✝¹ x✝ : Unitization R A
⊢ (x✝² * (x✝¹ + x✝)).toProd.2 = (x✝² * x✝¹ + x✝² * x✝).toProd.2

Tactic:
by

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✝² x✝¹ x✝ : Unitization R A
⊢ ((x✝² + x✝¹) * x✝).toProd.2 = (x✝² * x✝ + x✝¹ * x✝).toProd.2

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x y z : Unitization R A
⊢ (x * y * z).toProd.2 = (x * (y * z)).toProd.2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalCommSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x✝¹ x✝ : Unitization R A
⊢ (x✝¹ * x✝).toProd.2 = (x✝ * x✝¹).toProd.2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Star R
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : R
⊢ (inl (star r)).toProd.2 = (star (inl r)).toProd.2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : AddMonoid R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ (↑(star a)).toProd.1 = (star ↑a).toProd.1

Tactic:
by

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:
by

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:
by

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✝³ : NonUnitalNonAssocSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
x y : Unitization R A
⊢ (star (x * y)).toProd.1 = (star y * star x).toProd.1

Tactic:
by

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✝³ : NonUnitalNonAssocSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
x y : Unitization R A
⊢ (star (x * y)).toProd.2 = (star y * star x).toProd.2

Tactic:
by

Goal state after:
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✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
x : Unitization R A
⊢ ((inlRingHom R A).comp (algebraMap S R)) s * x = x * ((inlRingHom R A).comp (algebraMap S R)) s

Tactic:
by

Goal state after:
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✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
x : Unitization R A
⊢ s • x = ((inlRingHom R A).comp (algebraMap S R)) s * x

Tactic:
by

Goal state after:
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
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) B
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)
⊢ φ = ψ

Tactic:
by

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:
by

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
C : Type u_5
inst✝³ : Semiring C
inst✝² : Algebra R C
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) C
inst✝ : AlgHomClass F R (Unitization R A) C
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
r : R
⊢ φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)

Tactic:
by

Goal state after:
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
⊢ (algebraMap R C) (toProd 1).1 + φ (toProd 1).2 = 1

Tactic:
by

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

Tactic:
by

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:
by

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:
by

Goal state after:
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
x y : Unitization R A
⊢ (algebraMap R C) (x * y).toProd.1 + φ (x * y).toProd.2 =
    ((algebraMap R C) x.toProd.1 + φ x.toProd.2) * ((algebraMap R C) y.toProd.1 + φ y.toProd.2)

Tactic:
by

Goal state after:
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
⊢ (algebraMap R C) (toProd 0).1 + φ (toProd 0).2 = 0

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
x y : Unitization R A
⊢ (algebraMap R C) (x + y).toProd.1 + φ (x + y).toProd.2 =
    (algebraMap R C) x.toProd.1 + φ x.toProd.2 + ((algebraMap R C) y.toProd.1 + φ y.toProd.2)

Tactic:
by

Goal state after:
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
r : R
⊢ (algebraMap R C) ((algebraMap R (Unitization R A)) r).toProd.1 + φ ((algebraMap R (Unitization R A)) r).toProd.2 =
    (algebraMap R C) r

Tactic:
by

Goal state after: