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

Goal state before:
pp: case succ
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
ih : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
⊢ a ⊗ₜ[R] b ^ (k + 1) = (a ^ (k + 1)) ⊗ₜ[R] (b ^ (k + 1))

Tactic:
| succ k ih =>

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

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✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (x y : A),
    (↑((AlgebraTensorModule.mk R R A B).flip 1).toAddMonoidHom).toFun (x * y) =
      (↑((AlgebraTensorModule.mk R R A B).flip 1).toAddMonoidHom).toFun x *
        (↑((AlgebraTensorModule.mk R R A B).flip 1).toAddMonoidHom).toFun y

Tactic:
by simp

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

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✝⁷ : Algebra R A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Semiring C
inst✝³ : Algebra R C
inst✝² : CommSemiring S
inst✝¹ : Algebra S A
inst✝ : SMulCommClass R S A
⊢ ∀ (r : S), (↑↑includeLeftRingHom).toFun ((algebraMap S A) r) = (algebraMap S (A ⊗[R] B)) r

Tactic:
by simp

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

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✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : CommSemiring S
inst✝ : Algebra S A
⊢ ∀ (x y : B),
    (↑((AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun (x * y) =
      (↑((AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun x *
        (↑((AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun y

Tactic:
by simp

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

Goal state before:
pp: case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = ↑h'.subInvSMul⁻¹

Tactic:
h'.val_inv_subInvSMul

Goal state after:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = r • ↑h'.unit⁻¹
Module: Mathlib.RingTheory.TensorProduct.Basic

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✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
a : A
b : B
x : A ⊗[R] B
⊢ a • b • 0 = b • a • 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
q✝ : Q
h : q✝ ∈ I • ⊤
r : R
hr : r ∈ I
q : Q
x✝ : q ∈ ⊤
⊢ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) (⟨r, hr⟩ ⊗ₜ[R] q) = r • q

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) 0 ∈ I • ⊤

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
⊢ ∀ (w : A) (x : B) (y : A) (z : B),
    (mul' R (A ⊗[R] B)) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) =
      (map (mul' R A) (mul' R B) ∘ₗ ↑(tensorTensorTensorComm R A B A B)) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z))

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalNonAssocSemiring A
inst✝¹¹ : NonUnitalNonAssocSemiring B
inst✝¹⁰ : Module R A
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : SMulCommClass R B B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : IsScalarTower R B B
inst✝⁴ : StarRing R
inst✝³ : StarRing A
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x y : A ⊗[R] B
⊢ star (0 * y) = star y * star 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalNonAssocSemiring A
inst✝¹¹ : NonUnitalNonAssocSemiring B
inst✝¹⁰ : Module R A
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : SMulCommClass R B B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : IsScalarTower R B B
inst✝⁴ : StarRing R
inst✝³ : StarRing A
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x y : A ⊗[R] B
x✝¹ : A
x✝ : B
⊢ star (x✝¹ ⊗ₜ[R] x✝ * 0) = star 0 * star (x✝¹ ⊗ₜ[R] x✝)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalNonAssocSemiring A
inst✝¹¹ : NonUnitalNonAssocSemiring B
inst✝¹⁰ : Module R A
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : SMulCommClass R B B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : IsScalarTower R B B
inst✝⁴ : StarRing R
inst✝³ : StarRing A
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x y : A ⊗[R] B
x✝³ : A
x✝² : B
x✝¹ : A
x✝ : B
⊢ star (x✝³ ⊗ₜ[R] x✝² * x✝¹ ⊗ₜ[R] x✝) = star (x✝¹ ⊗ₜ[R] x✝) * star (x✝³ ⊗ₜ[R] x✝²)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalNonAssocSemiring A
inst✝¹¹ : NonUnitalNonAssocSemiring B
inst✝¹⁰ : Module R A
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : SMulCommClass R B B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : IsScalarTower R B B
inst✝⁴ : StarRing R
inst✝³ : StarRing A
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
⊢ ∀ (r s : A ⊗[R] B), star (r + s) = star r + star s

Tactic:
by simp

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

Goal state before:
pp: case e'_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ 1 = 1 + ↑0

Tactic:
simp only [inr_zero, add_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ { val := 1 + ↑(PreQuasiregular.equiv.symm ↑x), inv := 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹), val_inv := ⋯,
      inv_val := ⋯ } ∈
    unitsFstOne R A

Tactic:
by 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
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 S C
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
⊢ ∀ (x : A), ((lift f g hfg).comp includeLeft) x = f x

Tactic:
by 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
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 S C
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
⊢ ∀ (x : B), ((AlgHom.restrictScalars R (lift f g hfg)).comp includeRight) x = g x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x y : ↥(unitsFstOne R A)
⊢ PreQuasiregular.equiv.symm
      ↑{ val := PreQuasiregular.equiv (↑↑(x * y)).toProd.2, inv := PreQuasiregular.equiv (↑↑(x * y)⁻¹).toProd.2,
          val_inv := ⋯, inv_val := ⋯ } =
    PreQuasiregular.equiv.symm
      ↑({ val := PreQuasiregular.equiv (↑↑x).toProd.2, inv := PreQuasiregular.equiv (↑↑x⁻¹).toProd.2, val_inv := ⋯,
            inv_val := ⋯ } *
          { val := PreQuasiregular.equiv (↑↑y).toProd.2, inv := PreQuasiregular.equiv (↑↑y⁻¹).toProd.2, val_inv := ⋯,
            inv_val := ⋯ })

Tactic:
by 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
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
⊢ ∀ (x : B), ((lift f g hfg).comp includeRight) x = g x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ equiv.symm ↑u⁻¹ + equiv.symm ↑u + equiv.symm ↑u * equiv.symm ↑u⁻¹ = 0 ∧
    equiv.symm ↑u + equiv.symm ↑u⁻¹ + equiv.symm ↑u⁻¹ * equiv.symm ↑u = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ hx.unit ∈ Unitization.unitsFstOne R A

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ PreQuasiregular.equiv.symm ↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, ⋯⟩) = x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Nontrivial R
a : A
⊢ ¬IsUnit 0

Tactic:
by 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
⊢ ∀ (y : A ⊗[S] B),
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (0 * y) =
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) 0 * (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) y

Tactic:
by 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
⊢ (_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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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
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 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:
by 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:
by simp

Goal state after: