mathlib-initiative/mathlib-tactics huggingface dataset:
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.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f) =
    (LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)

Tactic:
;

Goal state after:
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.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f) =
    (LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)
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
x✝¹ x✝ : A
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry ((LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f))) 1) x✝¹))
        1)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                ((LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)))
              1)
            x✝¹))
        1)
      x✝

Tactic:
;

Goal state after:
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
x✝¹ x✝ : A
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry ((LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f))) 1) x✝¹))
        1)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                ((LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)))
              1)
            x✝¹))
        1)
      x✝
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✝ : A
⊢ ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight)
        ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯) f))
      x✝ =
    f x✝

Tactic:
;

Goal state after:
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✝ : A
⊢ ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight)
        ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯) f))
      x✝ =
    f x✝
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 : S ⊗[R] A →ₐ[S] B
x✝ : A
⊢ ((restrictScalars R
            ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯)
              ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight) f))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((restrictScalars R f).comp Algebra.TensorProduct.includeRight) x✝

Tactic:
;

Goal state after:
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 : S ⊗[R] A →ₐ[S] B
x✝ : A
⊢ ((restrictScalars R
            ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯)
              ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight) f))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((restrictScalars R f).comp Algebra.TensorProduct.includeRight) x✝
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
x y z : PreQuasiregular R
⊢ z.val + (y.val + x.val + x.val * y.val) + (y.val * z.val + x.val * z.val + x.val * (y.val * z.val)) =
    z.val + y.val + y.val * z.val + x.val + (x.val * z.val + x.val * y.val + x.val * (y.val * z.val))

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalSemiring R
x y z : PreQuasiregular R
⊢ z.val + (y.val + x.val + x.val * y.val) + (y.val * z.val + x.val * z.val + x.val * (y.val * z.val)) =
    z.val + y.val + y.val * z.val + x.val + (x.val * z.val + x.val * y.val + x.val * (y.val * z.val))
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 S C✝
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Algebra R C✝
inst✝⁴ : IsScalarTower R S C✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝¹ : B →ₐ[R] C
x✝ : B
⊢ ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) ((fun f ↦ lift (ofId S C) f ⋯) x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C✝ : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Semiring A
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra S A
inst✝¹² : IsScalarTower R S A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Algebra R B
inst✝⁹ : Semiring C✝
inst✝⁸ : Algebra S C✝
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Algebra R C✝
inst✝⁴ : IsScalarTower R S C✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝¹ : B →ₐ[R] C
x✝ : B
⊢ ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) ((fun f ↦ lift (ofId S C) f ⋯) x✝¹)) x✝ = x✝¹ x✝
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 S C✝
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Algebra R C✝
inst✝⁴ : IsScalarTower R S C✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝¹ : S ⊗[R] B →ₐ[S] C
x✝ : B
⊢ ((AlgHom.restrictScalars R
            ((fun f ↦ lift (ofId S C) f ⋯) ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) x✝¹))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R x✝¹).comp includeRight) x✝

Tactic:
;

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C✝ : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Semiring A
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra S A
inst✝¹² : IsScalarTower R S A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Algebra R B
inst✝⁹ : Semiring C✝
inst✝⁸ : Algebra S C✝
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Algebra R C✝
inst✝⁴ : IsScalarTower R S C✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝¹ : S ⊗[R] B →ₐ[S] C
x✝ : B
⊢ ((AlgHom.restrictScalars R
            ((fun f ↦ lift (ofId S C) f ⋯) ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) x✝¹))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R x✝¹).comp includeRight) x✝
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
⊢ ∀ (a₁ a₂ : R) (b₁ b₂ : A), a₁ • a₂ • (b₁ * b₂) = a₂ • a₁ • (b₁ * b₂)

Tactic:
← mul_smul,

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Semiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra S A
inst✝¹⁴ : IsScalarTower R S A
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R C
inst✝⁹ : Algebra S C
inst✝⁸ : IsScalarTower R S C
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Semiring E
inst✝⁴ : Algebra R E
inst✝³ : Algebra S E
inst✝² : IsScalarTower R S E
inst✝¹ : Semiring F
inst✝ : Algebra R F
⊢ ∀ (a₁ a₂ : R) (b₁ b₂ : A), (a₁ * a₂) • (b₁ * b₂) = (a₂ * a₁) • (b₁ * b₂)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : S
⊢ ((AlgebraTensorModule.curry (↑R (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ (TensorProduct.rid R R S).toLinearMap)) x✝) 1 =
    ((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R B))) x✝) 1

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : S
⊢ ((AlgebraTensorModule.curry (↑R (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ (TensorProduct.rid R R S).toLinearMap)) x✝) 1 =
    ((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R B))) x✝) 1
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
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
x✝ : A
⊢ ((↑(TensorProduct.rid R S A)).comp includeLeftRingHom) x✝ = (RingHom.id A) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
A : Type uA
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
x✝ : A
⊢ ((↑(TensorProduct.rid R S A)).comp includeLeftRingHom) x✝ = (RingHom.id A) x✝
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Field S
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : Module S A
inst✝ : Algebra R S
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : quasispectrum S a ⊆ Set.range ⇑(algebraMap R S)
r : R
hs : (algebraMap R S) r ∈ quasispectrum S a
⊢ (algebraMap R S) (f ((algebraMap R S) r)) = (algebraMap R S) r

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Field S
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : Module S A
inst✝ : Algebra R S
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : quasispectrum S a ⊆ Set.range ⇑(algebraMap R S)
r : R
hs : (algebraMap R S) r ∈ quasispectrum S a
⊢ (algebraMap R S) (f ((algebraMap R S) r)) = (algebraMap R S) r
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
a✝ : B ⊗[R] A
⊢ (TensorProduct.comm R A B).symm a✝ = (TensorProduct.comm R B A) a✝

Tactic:
;

Goal state after:
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✝ : B ⊗[R] A
⊢ (TensorProduct.comm R A B).symm a✝ = (TensorProduct.comm R B A) a✝
Module: Mathlib.Algebra.Group.Pi.Units

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

Tactic:
;

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i)⁻¹ = ↑⋯.unit⁻¹
Module: Mathlib.Algebra.Group.Pi.Units

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

Tactic:
;

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ MulEquiv.piUnits hx.unit i = ⋯.unit
Module: Mathlib.Algebra.Group.Pi.Units

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

Tactic:
;

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i) = ↑⋯.unit
Module: Mathlib.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:
simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toPi κ), Pi.isUnit_iff]

Goal state after:
ι : Type u_1
κ : ι → Type u_5
inst✝ : (i : ι) → NonUnitalSemiring (κ i)
x : (i : ι) → κ i
⊢ (∀ (i : ι), IsUnit ((PreQuasiregular.toPi κ) (PreQuasiregular.equiv x) i)) ↔
    ∀ (i : ι), IsUnit (PreQuasiregular.equiv (x i))
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
x✝ : S
⊢ ((mapRingHom fR fS fT HS HT).comp includeLeftRingHom) x✝ = (includeLeftRingHom.comp fS) x✝

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
x✝ : S
⊢ ((mapRingHom fR fS fT HS HT).comp includeLeftRingHom) x✝ = (includeLeftRingHom.comp fS) x✝
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: case pos
ι : 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
r : R
r' : Rˣ
hr' : ↑r' = r
⊢ (∀ (hr : IsUnit ↑r'), ¬IsQuasiregular (-(⋯.unit⁻¹ • a))) ↔
    ∃ i, ∀ (hr : IsUnit ↑r'), ¬IsQuasiregular (-(⋯.unit⁻¹ • a i))

Tactic:
simp [isQuasiregular_pi_iff]

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

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
x✝ : T
⊢ ((mapRingHom fR fS fT HS HT).comp ↑includeRight) x✝ = ((↑includeRight).comp fT) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
x✝ : A
⊢ ((↑(map f g)).comp includeLeftRingHom) x✝ = (includeLeftRingHom.comp ↑f) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
x✝ : A
⊢ ((↑(map f g)).comp includeLeftRingHom) x✝ = (includeLeftRingHom.comp ↑f) x✝
Module: Mathlib.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:
refine DFunLike.ext φ ψ (fun x ↦ ?_)

Goal state after:
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
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)
x : Unitization R A
⊢ φ x = ψ x
Module: Mathlib.RingTheory.TensorProduct.Maps

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

Tactic:
;

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