mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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
φ : Unitization R A →ₐ[R] C
⊢ ((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ).toAlgHom = φ

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
⊢ ⇑(NonUnitalAlgHom.toAlgHom 0) = fun x ↦ 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
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
φ : A →⋆ₙₐ[R] C
x : Unitization R A
⊢ (↑↑(lift φ.toNonUnitalAlgHom).toRingHom).toFun (star x) = star ((↑↑(lift φ.toNonUnitalAlgHom).toRingHom).toFun x)

Tactic:
by

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

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

Tactic:
by

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

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

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
inst✝¹⁶ : CommSemiring T
inst✝¹⁵ : Algebra R T
inst✝¹⁴ : Algebra T A
inst✝¹³ : IsScalarTower R T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : Algebra S T
inst✝¹⁰ : IsScalarTower S T A
inst✝⁹ : CommSemiring R'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R' T
inst✝⁶ : Algebra R' A
inst✝⁵ : Algebra R' B
inst✝⁴ : IsScalarTower R R' A
inst✝³ : SMulCommClass S R' A
inst✝² : SMulCommClass R' S A
inst✝¹ : IsScalarTower R' T A
inst✝ : IsScalarTower R R' B
⊢ (LinearMap.mul T (A ⊗[R'] B ⊗[S] (C ⊗[R] D))).compr₂ ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D) =
    (LinearMap.mul T (A ⊗[S] C ⊗[R'] (B ⊗[R] D)) ∘ₗ
          ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D)).compl₂
      ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D)

Tactic:
by

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

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

Tactic:
by

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

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

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

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective ⇑φ
x y : Unitization R A
h : (starMap φ) x = (starMap φ) y
⊢ φ x.toProd.2 = φ y.toProd.2

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
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)
⊢ Function.Bijective ⇑includeLeft

Tactic:
by

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

Goal state before:
pp: 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
h : Function.Bijective ⇑(algebraMap R A)
⊢ Function.Bijective ⇑includeRight

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
r : R
⊢ (algebraMap R A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

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✝⁵ : 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

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
x✝¹ x✝ : S
⊢ (LinearMap.mul' R S).toFun (s • x✝¹ ⊗ₜ[R] x✝) = (RingHom.id S) s • (LinearMap.mul' R S).toFun (x✝¹ ⊗ₜ[R] x✝)

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✝⁵ : 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✝ x y : S ⊗[R] S
hx : (LinearMap.mul' R S).toFun (s • x) = (RingHom.id S) s • (LinearMap.mul' R S).toFun x
hy : (LinearMap.mul' R S).toFun (s • y) = (RingHom.id S) s • (LinearMap.mul' R S).toFun y
⊢ (LinearMap.mul' R S).toFun (s • (x + y)) = (RingHom.id S) s • (LinearMap.mul' R S).toFun (x + y)

Tactic:
by

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

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

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✝⁵ : 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
a₁ a₂ b₁ b₂ : S
⊢ (let __spread.0 := LinearMap.mul' R S;
      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
      ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    (let __spread.0 := LinearMap.mul' R S;
        { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
        (a₁ ⊗ₜ[R] b₁) *
      (let __spread.0 := LinearMap.mul' R S;
        { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
        (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✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (let __spread.0 := LinearMap.mul' R S;
      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
      (1 ⊗ₜ[R] 1) =
    1

Tactic:
by

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

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

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

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
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:
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✝⁶ : 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
inst✝ : CompatibleSMul R S S S
x : S ⊗[R] S
⊢ (includeLeft.comp (lmul'' R)) 0 = (AlgHom.id S (S ⊗[R] S)) 0

Tactic:
by

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

Goal state after:
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:
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✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ IsSelfAdjoint ↑a ↔ IsSelfAdjoint a

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✝⁴ : StarAddMonoid R
inst✝³ : Star A
a : A
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : SMulWithZero R A
⊢ IsStarNormal ↑a ↔ IsStarNormal a

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
⊢ IsIdempotentElem ↑a ↔ IsIdempotentElem a

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✝³ : StarRing R
inst✝² : NonUnitalSemiring A
inst✝¹ : StarRing A
inst✝ : Module R A
p : A
⊢ IsStarProjection ↑p ↔ IsStarProjection p

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✝⁶ : 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
inst✝ : CompatibleSMul R S S S
x x✝¹ x✝ : S ⊗[R] S
hx : (includeLeft.comp (lmul'' R)) x✝¹ = (AlgHom.id S (S ⊗[R] S)) x✝¹
hy : (includeLeft.comp (lmul'' R)) x✝ = (AlgHom.id S (S ⊗[R] S)) x✝
⊢ (includeLeft.comp (lmul'' R)) (x✝¹ + x✝) = (AlgHom.id S (S ⊗[R] S)) (x✝¹ + x✝)

Tactic:
by

Goal state after:
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:
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
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:
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
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
a : A
⊢ (productMap f g) (a ⊗ₜ[R] 1) = f a

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
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
b : B
⊢ (productMap f g) (1 ⊗ₜ[R] b) = g b

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : PartialOrder A
inst✝² : Monoid A
inst✝¹ : Zero A
inst✝ : Subsingleton A
a : A
⊢ 0 ≤ a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsStrictlyPositive (star u * a * u) ↔ IsStrictlyPositive a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsUnit b
hb₂ : IsSelfAdjoint b
⊢ IsStrictlyPositive (b * a * b) ↔ IsStrictlyPositive a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
⊢ c • a * c⁻¹ • ↑⋯.unit⁻¹ = 1 ∧ c⁻¹ • ↑⋯.unit⁻¹ * c • a = 1

Tactic:
by

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (c • a)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : PartialOrder A
inst✝⁴ : ZeroLEOneClass A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
⊢ IsStrictlyPositive ((algebraMap 𝕜 A) c)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 ≤ x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
⊢ x ≠ 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r✝ : R
a✝ : A
r : R
a : A
⊢ (fun s ↦ star s * s) (r • a) = (fun s ↦ star s * s) r • (fun s ↦ star s * s) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ r • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

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
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).range = f.range ⊔ g.range

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (x y : A), (x + y) • baseChangeHom R A M N = x • baseChangeHom R A M N + y • baseChangeHom R A M N

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (m x : A), (m • x) • baseChangeHom R A M N = (RingHom.id A) m • x • baseChangeHom R A M N

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
a b : A
f g : End R M
⊢ (tensorProduct R A M M) ((a * b) ⊗ₜ[R] (f * g)) =
    (tensorProduct R A M M) (a ⊗ₜ[R] f) * (tensorProduct R A M M) (b ⊗ₜ[R] g)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ (tensorProduct R A M M) (1 ⊗ₜ[R] 1) = 1

Tactic:
by

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

Goal state after: