mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
⊢ σ (k • a) = k • σ a

Tactic:
by

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✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
⊢ x * y = y * x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
⊢ (σ ↑a)⁻¹ = σ ↑a⁻¹

Tactic:
by

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

Goal state before:
pp: R : Type uR
A : Type uA
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra R B
z : ℤ
⊢ ↑z = 1 ⊗ₜ[R] ↑z

Tactic:
by

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ : F
a : A
r : R
h : r ∈ resolventSet R a
⊢ r ∈ resolventSet R (φ a)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FunLike F A R
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑ₐ (φ a) - a ∈ RingHom.ker ↑φ

Tactic:
by

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FunLike F A R
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ φ a ∈ σ a

Tactic:
by

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✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ instRing.toAddCommGroup = addCommGroup

Tactic:
by

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : EquivLike F A B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (f a)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
⊢ spectrum R (↑u * a * ↑u⁻¹) = spectrum R a

Tactic:
by

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✝¹ : CommSemiring B
inst✝ : Algebra R B
b : B
x : A ⊗[R] B
⊢ includeRight.toRingHom b * x = x * includeRight.toRingHom b

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u * a * ↑u⁻¹) = spectrum R a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a

Tactic:
by

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✝¹ : CommSemiring B
inst✝ : Algebra R B
a : A
b : B
x x✝¹ x✝ : A ⊗[R] B
h₁ : a • b • x✝¹ = b • a • x✝¹
h₂ : a • b • x✝ = b • a • x✝
⊢ a • b • (x✝¹ + x✝) = b • a • (x✝¹ + x✝)

Tactic:
by

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✝¹ : Ring A
inst✝ : Ring B
⊢ Ring (A ⊗[ℤ] B)

Tactic:
by

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✝¹ : CommRing A
inst✝ : CommRing B
⊢ CommRing (A ⊗[ℤ] B)

Tactic:
by

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight) = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
h : adjoin A ↑(Subalgebra.map includeRight ⊤) = ⊤
⊢ adjoin A ((fun x ↦ 1 ⊗ₜ[R] x) '' s) = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ adjoin A ((fun x ↦ 1 ⊗ₜ[R] x) '' s) = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Function.Injective ⇑((TensorProduct.mk R S M) 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring B
inst✝² : Algebra R B
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : B
⊢ LinearMap.baseChange A ((lmul R B) f) = (lmul A (A ⊗[R] B)) (1 ⊗ₜ[R] f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Module A M
inst✝⁴ : Module B M
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R B M
r t : A
⊢ (r + t) • (Algebra.lsmul R R M).toLinearMap =
    r • (Algebra.lsmul R R M).toLinearMap + t • (Algebra.lsmul R R M).toLinearMap

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Module A M
inst✝⁴ : Module B M
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R B M
n : R
r : A
⊢ (n • r) • (Algebra.lsmul R R M).toLinearMap = (RingHom.id R) n • r • (Algebra.lsmul R R M).toLinearMap

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (x * y) • m = x • y • m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
m : M
⊢ 1 • m = m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x : A ⊗[R] B
⊢ x • 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x : A ⊗[R] B
m₁ m₂ : M
⊢ x • (m₁ + m₂) = x • m₁ + x • m₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (x + y) • m = x • m + y • m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
m : M
⊢ 0 • m = 0

Tactic:
by

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✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R = map (Algebra.linearMap R A) (Algebra.linearMap R B)

Tactic:
by

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

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 • ⊤
⊢ ∀ (x y : Q),
    x ∈ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range →
      y ∈ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range →
        x + y ∈ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range

Tactic:
by

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

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
⊢ ∀ (x : ↥I) (y : Q), (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) (x ⊗ₜ[R] y) ∈ I • ⊤

Tactic:
by

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
⊢ ∀ (x y : ↥I ⊗[R] Q),
    (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) x ∈ I • ⊤ →
      (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) y ∈ I • ⊤ →
        (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) (x + y) ∈ I • ⊤

Tactic:
by

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
⊢ map (↑(TensorProduct.lid R Q)) (rTensor Q I.subtype).range = I • ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Function.Surjective ⇑((mk R S M) 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ Function.Surjective ⇑((mk R S T).flip 1)

Tactic:
by

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
⊢ LinearMap.mul' R (A ⊗[R] B) ∘ₗ ↑(tensorTensorTensorComm R A A B B) = map (LinearMap.mul' R A) (LinearMap.mul' R B)

Tactic:
by

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

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
a : A
b : B
⊢ mulLeft R (a ⊗ₜ[R] b) = map (mulLeft R a) (mulLeft R b)

Tactic:
by

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
a : A
b : B
⊢ mulRight R (a ⊗ₜ[R] b) = map (mulRight R a) (mulRight R b)

Tactic:
by

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

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

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

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✝¹ x✝ : A ⊗[R] B
h₁ : star (x✝³ ⊗ₜ[R] x✝² * x✝¹) = star x✝¹ * star (x✝³ ⊗ₜ[R] x✝²)
h₂ : star (x✝³ ⊗ₜ[R] x✝² * x✝) = star x✝ * star (x✝³ ⊗ₜ[R] x✝²)
⊢ star (x✝³ ⊗ₜ[R] x✝² * (x✝¹ + x✝)) = star (x✝¹ + x✝) * star (x✝³ ⊗ₜ[R] x✝²)

Tactic:
by

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 x✝¹ x✝ : A ⊗[R] B
h₁ : star (x✝¹ * y) = star y * star x✝¹
h₂ : star (x✝ * y) = star y * star x✝
⊢ star ((x✝¹ + x✝) * y) = star y * star (x✝¹ + x✝)

Tactic:
by

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

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✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ (LinearMap.liftBaseChange S ↑f) 1 = 1

Tactic:
by

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✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.liftBaseChange S ↑f) (x * y) = (LinearMap.liftBaseChange S ↑f) x * (LinearMap.liftBaseChange S ↑f) y

Tactic:
by

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✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ (fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight)
      ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯) f) =
    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
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
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
⊢ (LinearMap.mul S (A ⊗[R] B)).compr₂ f = (LinearMap.mul S C ∘ₗ f).compl₂ f

Tactic:
by

Goal state after: