mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
g : C ≃ₐ[A] D
x y : B
⊢ (fieldEquivOfAlgEquiv FA FB FD (f.trans g)) ((algebraMap B FB) x / (algebraMap B FB) y) =
    ((fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g))
      ((algebraMap B FB) x / (algebraMap B FB) y)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
⊢ f = g

Tactic:
ext b

Goal state after:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
b : B
⊢ f b = g b
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (⨆ x, J ↑x).subtype) ((rTensor M (inclusion ⋯)) (y x)) = (rTensor M (J x).subtype) (y x)

Tactic:
rw [← comp_apply, ← rTensor_comp]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M ((⨆ x, J ↑x).subtype ∘ₗ inclusion ⋯)) (y x) = (rTensor M (J x).subtype) (y x)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : Finite ↑s
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
x : ↥I ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (inclusion ⋯)) ((rTensor M (inclusion ⋯)) (y x)) = (rTensor M (inclusion ⋯)) (y x)

Tactic:
rw [← comp_apply, ← rTensor_comp]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : Finite ↑s
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
x : ↥I ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (inclusion ⋯ ∘ₗ inclusion ⋯)) (y x) = (rTensor M (inclusion ⋯)) (y x)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ (↑y * x) y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)

Tactic:
exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

Goal state after:
Module: Mathlib.RingTheory.Localization.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
S : Type u_4
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
M : Submonoid R
inst✝⁶ : IsLocalization M S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f✝ : A →ₐ[R] B
f : S →ₐ[R] B := f✝.comp (IsScalarTower.toAlgHom R S A)
g : S →ₐ[R] B := IsScalarTower.toAlgHom R S B
⊢ f.comp (algebraMap R S) = g.comp (algebraMap R S)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Algebra.IsEpi R A
a : A
⊢ (lift (LinearMap.mul R A)) (1 ⊗ₜ[R] a) = (lift (LinearMap.mul R A)) (a ⊗ₜ[R] 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
⊢ 0 = 0 ⊗ₜ[R] 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A
⊢ u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A
⊢ u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 = (u * v) ⊗ₜ[R] 1

Tactic:
simp

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

Goal state before:

Tactic:
u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := ⋯
h✝ : Nontrivial (A ⧸ R')
x y : A
⊢ x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y = x ⊗ₜ[R] y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
                    (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
simp

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

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
x✝ : S
⊢ ((Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
            ((↑(Algebra.TensorProduct.comm R T' S)).comp
              ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T)))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

Tactic:
simp

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

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
              ((↑(Algebra.TensorProduct.comm R T' S)).comp
                ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T))))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x : A
⊢ ∀ (m_1 : R) (x_1 : A), x ⊗ₜ[R] ((m_1 • x_1) • m) = (RingHom.id R) m_1 • x ⊗ₜ[R] (x_1 • m)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (AlgebraTensorModule.lift (LinearMap.restrictScalarsₗ R A M M A ∘ₗ LinearMap.lsmul A M)) (1 ⊗ₜ[R] m) = m

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (lid' R A M) ((lid' R A M).symm m) = (lid' R A M) (1 ⊗ₜ[R] m)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
p q : R
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hqp : q * p = p
⊢ p * q = p

Tactic:
simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
y : M
⊢ (liftBaseChange A l) (1 ⊗ₜ[R] y) = l y

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module A N
inst✝⁴ : IsScalarTower R A N
P : Type u_1
inst✝³ : AddCommMonoid P
inst✝² : Module A P
inst✝¹ : Module R P
inst✝ : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
x✝ : M
⊢ ((AlgebraTensorModule.curry (l' ∘ₗ liftBaseChange A l)) 1) x✝ =
    ((AlgebraTensorModule.curry (liftBaseChange A (↑R l' ∘ₗ l))) 1) x✝

Tactic:
simp

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

Goal state before:
pp: case a.zero
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ (liftBaseChange A l) 0 ∈ Submodule.span A ↑l.range

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x : M
⊢ (liftBaseChange A l) (1 ⊗ₜ[R] x) = l x

Tactic:
simp

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
⊢ ↑0 ⊗ₜ[R] 1 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (x y : A),
    (↑((AlgebraTensorModule.mk R R A B).flip 1).toAddMonoidHom).toFun (x * y) =
      (↑((AlgebraTensorModule.mk R R A B).flip 1).toAddMonoidHom).toFun x *
        (↑((AlgebraTensorModule.mk R R A B).flip 1).toAddMonoidHom).toFun y

Tactic:
simp

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Semiring C
inst✝³ : Algebra R C
inst✝² : CommSemiring S
inst✝¹ : Algebra S A
inst✝ : SMulCommClass R S A
⊢ ∀ (r : S), (↑↑includeLeftRingHom).toFun ((algebraMap S A) r) = (algebraMap S (A ⊗[R] B)) r

Tactic:
simp

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : CommSemiring S
inst✝ : Algebra S A
⊢ ∀ (x y : B),
    (↑((AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun (x * y) =
      (↑((AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun x *
        (↑((AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun y

Tactic:
simp

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✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : R
⊢ (includeLeftRingHom.comp (algebraMap R A)) x✝ = (includeRight.comp (algebraMap R B)) x✝

Tactic:
simp

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

Goal state before:
pp: case zero
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
C : Type u_3
inst✝ : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom
⊢ f 0 = g 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
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
⊢ 0 * y = y * 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
⊢ x = r • r⁻¹ • x

Tactic:
simp

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a

Tactic:
smul_mem_smul_iff

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
h : r⁻¹ • x ∈ σ a
⊢ r • r⁻¹ • x = x

Tactic:
simp

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

Goal state before:
pp: case refine_2.refine_1
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
a₁ : A
b₁ : B
⊢ a₁ ⊗ₜ[R] b₁ * 0 = 0 * a₁ ⊗ₜ[R] b₁

Tactic:
simp

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

Goal state before:
pp: case refine_2.refine_2
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
a₁ : A
b₁ : B
⊢ ∀ (x : A) (y : B), a₁ ⊗ₜ[R] b₁ * x ⊗ₜ[R] y = x ⊗ₜ[R] y * a₁ ⊗ₜ[R] b₁

Tactic:
intro a₂ b₂
        simp [mul_comm]

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

Goal state before:
pp: case inl
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
⊢ 0⁻¹ ∈ spectrum R ↑a ↔ 0 ∈ spectrum R ↑a⁻¹

Tactic:
simp

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : Aˣ
⊢ r⁻¹ ∈ spectrum R ↑a⁻¹ ↔ r ∈ spectrum R ↑a

Tactic:
simp

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ˣ
x✝ : 𝕜
⊢ x✝ ∈ (σ ↑a)⁻¹ ↔ x✝ ∈ σ ↑a⁻¹

Tactic:
simp

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
a : A
b : B
x : A ⊗[R] B
⊢ a • b • 0 = b • a • 0

Tactic:
simp

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

Goal state before:
pp: case e'_5
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
x : A
y : B
⊢ x ⊗ₜ[R] y = includeLeftRingHom x * includeRight y

Tactic:
simp

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
m : M
⊢ (LinearMap.liftBaseChange S LinearMap.id) (((TensorProduct.mk R S M) 1) m) = m

Tactic:
simp

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 i : B
⊢ ((AlgebraTensorModule.curry (LinearMap.baseChange A ((lmul R B) f))) 1) i =
    ((AlgebraTensorModule.curry ((lmul A (A ⊗[R] B)) (1 ⊗ₜ[R] f))) 1) i

Tactic:
simp

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:
ext i
  simp

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

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

Tactic:
hw

Goal state after:
case refine_2.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
z w : A ⊗[R] B
hz : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * z) • m = x ⊗ₜ[R] y • z • m
hw : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * w) • m = x ⊗ₜ[R] y • w • m
⊢ ∀ (x : A) (y : B), (x ⊗ₜ[R] y * (z + w)) • m = x ⊗ₜ[R] y • (z + w) • m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_2
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
a : A
b : B
z w : A ⊗[R] B
hz : (z * a ⊗ₜ[R] b) • m = z • a ⊗ₜ[R] b • m
⊢ (w * a ⊗ₜ[R] b) • m = w • a ⊗ₜ[R] b • m → ((z + w) * a ⊗ₜ[R] b) • m = (z + w) • a ⊗ₜ[R] b • m

Tactic:
hw

Goal state after:
case refine_3.refine_2
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
a : A
b : B
z w : A ⊗[R] B
hz : (z * a ⊗ₜ[R] b) • m = z • a ⊗ₜ[R] b • m
hw : (w * a ⊗ₜ[R] b) • m = w • a ⊗ₜ[R] b • m
⊢ ((z + w) * a ⊗ₜ[R] b) • m = (z + w) • a ⊗ₜ[R] b • m