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

Goal state before:
pp: case refine_3.refine_3
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
u v : A ⊗[R] B
a✝¹ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
a✝ : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz : (z * (u + v)) • m = z • (u + v) • m
⊢ (w * (u + v)) • m = w • (u + v) • m → ((z + w) * (u + v)) • m = (z + w) • (u + v) • m

Tactic:
hw

Goal state after:
case refine_3.refine_3
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
u v : A ⊗[R] B
a✝¹ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
a✝ : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz : (z * (u + v)) • m = z • (u + v) • m
hw : (w * (u + v)) • m = w • (u + v) • m
⊢ ((z + w) * (u + v)) • m = (z + w) • (u + v) • m
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:
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:
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
x✝³ x✝² : A
x✝¹ x✝ : B
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (AlgebraTensorModule.curry (LinearMap.mul' R (A ⊗[R] B) ∘ₗ ↑(tensorTensorTensorComm R A A B B))))
              x✝³)
            x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (map (LinearMap.mul' R A) (LinearMap.mul' R B)))) x✝³)
            x✝²))
        x✝¹)
      x✝

Tactic:
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:
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
a : A
b : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (mulLeft R (a ⊗ₜ[R] b))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (map (mulLeft R a) (mulLeft R b))) x✝¹) x✝

Tactic:
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
a : A
b : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (mulRight R (a ⊗ₜ[R] b))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (map (mulRight R a) (mulRight R b))) x✝¹) x✝

Tactic:
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:
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:
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:
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:
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✝
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:
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✝
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:
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✝
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:
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 : (PreQuasiregular A)ˣ
⊢ { val := 1 + ↑(PreQuasiregular.equiv.symm ↑x), inv := 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹), val_inv := ⋯,
      inv_val := ⋯ } ∈
    unitsFstOne R A

Tactic:
simp

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

Goal state before:
pp: case ha
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
x✝ : A
⊢ ((lift includeLeft includeRight ⋯).comp includeLeft) x✝ = ((AlgHom.id S (A ⊗[R] B)).comp includeLeft) x✝

Tactic:
simp

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

Goal state before:
pp: case hb
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
x✝ : B
⊢ ((AlgHom.restrictScalars R (lift includeLeft includeRight ⋯)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R (AlgHom.id S (A ⊗[R] B))).comp includeRight) x✝

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

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

Goal state before:
pp: case fst
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
fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }
x✝ : A
⊢ (↑((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩)
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯) fg))).1
      x✝ =
    (↑fg).1 x✝

Tactic:
simp

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

Goal state before:
pp: case snd
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
fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }
x✝ : B
⊢ (↑((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩)
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯) fg))).2
      x✝ =
    (↑fg).2 x✝

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv x * equiv y = 1

Tactic:
apply equiv.symm.injective
      assumption

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

Goal state before:
pp: case mpr.refine_2
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv y * equiv x = 1

Tactic:
apply equiv.symm.injective
      assumption

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

Goal state before:
pp: case ha
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
f' : A ⊗[R] B →ₐ[S] C
x✝ : A
⊢ (((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯)
            ((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩) f')).comp
        includeLeft)
      x✝ =
    (f'.comp includeLeft) x✝

Tactic:
simp

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

Goal state before:
pp: case hb
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
f' : A ⊗[R] B →ₐ[S] C
x✝ : B
⊢ ((AlgHom.restrictScalars R
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯)
              ((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩) f'))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R f').comp includeRight) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ 1 = 1 + 0

Tactic:
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 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:
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 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:
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
⊢ ∀ (a₁ a₂ : R) (b₁ b₂ : A), True

Tactic:
simp

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

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

Goal state after: