mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝¹ : A
x✝ : B
y : A ⊗[S] B
⊢ ∀ (x : A) (y : B),
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ ⊗ₜ[S] x✝ * x ⊗ₜ[S] y) =
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ ⊗ₜ[S] x✝) *
        (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x ⊗ₜ[S] y)

Tactic:
by

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✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
⊢ IsQuasiregular ↑a ↔ IsQuasiregular a

Tactic:
by

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ 0 ∈ spectrum R ↑a

Tactic:
by

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
hr : ¬IsUnit r
h : r ∈ resolventSet R ↑a
⊢ IsUnit 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✝³³ : 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
x✝³ : A
x✝² : B
y x✝¹ x✝ : A ⊗[S] B
h :
  (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝³ ⊗ₜ[S] x✝² * x✝¹) =
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝³ ⊗ₜ[S] x✝²) *
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) x✝¹
h' :
  (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝³ ⊗ₜ[S] x✝² * x✝) =
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝³ ⊗ₜ[S] x✝²) *
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) x✝
⊢ (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝³ ⊗ₜ[S] x✝² * (x✝¹ + x✝)) =
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝³ ⊗ₜ[S] x✝²) *
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ + x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
⊢ quasispectrum R a = spectrum 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✝³³ : 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 x✝² x✝¹ : A ⊗[S] B
h :
  ∀ (y : A ⊗[S] B),
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝² * y) =
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) x✝² * (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) y
h' :
  ∀ (y : A ⊗[S] B),
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝¹ * y) =
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) x✝¹ * (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) y
x✝ : A ⊗[S] B
⊢ (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) ((x✝² + x✝¹) * x✝) =
    (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) (x✝² + x✝¹) *
      (_root_.TensorProduct.mapOfCompatibleSMul R S T A B) x✝

Tactic:
by

Goal state after:
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✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ quasispectrum R a = spectrum 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✝⁴³ : 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
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this✝ : IsAddTorsionFree (M ⊗[R] N)
this : q.den • (q • m) ⊗ₜ[R] n = q.den • m ⊗ₜ[R] (q • n)
⊢ (fun x ↦ q.den • x) ((q • m) ⊗ₜ[R] n) = (fun x ↦ q.den • x) (m ⊗ₜ[R] (q • n))

Tactic:
by

Goal state after:
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✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ quasispectrum R ↑a = quasispectrum R a

Tactic:
by

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) = quasispectrum R (b * a)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : Algebra 𝕜 A
⊢ NonnegSpectrumClass 𝕜 A ↔ ∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x

Tactic:
by

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

Goal state before:
pp: S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ (algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a

Tactic:
by

Goal state after:
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
h : QuasispectrumRestricts a f
⊢ f 0 = 0

Tactic:
by

Goal state after:
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)
s : S
hs : s ∈ quasispectrum S a
⊢ (algebraMap R S) (f s) = s

Tactic:
obtain ⟨r, rfl⟩ := h hs

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.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)
s : S
hs : s ∈ quasispectrum S a
⊢ (algebraMap R S) (f s) = s

Tactic:
by

Goal state after:
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
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass S A A
f : S → R
a b : A
⊢ QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f

Tactic:
by

Goal state after:
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
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a

Tactic:
by

Goal state after:
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
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ f '' quasispectrum S a = quasispectrum R a

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst✝¹³ : Semifield R₁
inst✝¹² : Field R₂
inst✝¹¹ : Field R₃
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R₁ A
inst✝⁸ : Module R₂ A
inst✝⁷ : Module R₃ A
inst✝⁶ : Algebra R₁ R₂
inst✝⁵ : Algebra R₂ R₃
inst✝⁴ : Algebra R₁ R₃
inst✝³ : IsScalarTower R₁ R₂ R₃
inst✝² : IsScalarTower R₂ R₃ A
inst✝¹ : IsScalarTower R₃ A A
inst✝ : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ Set.RightInvOn e (⇑(algebraMap R₁ R₃)) (quasispectrum 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✝⁴³ : 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
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
⊢ (q • m) ⊗ₜ[R] n = m ⊗ₜ[R] (q • n)

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
⊢ (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst✝¹³ : Semifield R₁
inst✝¹² : Field R₂
inst✝¹¹ : Field R₃
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R₁ A
inst✝⁸ : Module R₂ A
inst✝⁷ : Module R₃ A
inst✝⁶ : Algebra R₁ R₂
inst✝⁵ : Algebra R₂ R₃
inst✝⁴ : Algebra R₁ R₃
inst✝³ : IsScalarTower R₁ R₂ R₃
inst✝² : IsScalarTower R₂ R₃ A
inst✝¹ : IsScalarTower R₃ A A
inst✝ : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ Function.LeftInverse e ⇑(algebraMap R₁ 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✝²⁵ : 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 S T
inst✝² : Algebra T A
inst✝¹ : IsScalarTower R T A
inst✝ : IsScalarTower S T A
⊢ (AlgebraTensorModule.assoc R S T A C D) 1 = 1

Tactic:
by

Goal state after:
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✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx : x ∈ quasispectrum S a
⊢ (algebraMap R S) (f x) = x

Tactic:
by

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

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

Tactic:
obtain ⟨r, rfl⟩ := h hs

Goal state after:
case inr
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)
r : R
hs : (algebraMap R S) r ∈ spectrum S a
⊢ (algebraMap R S) (f ((algebraMap R S) r)) = (algebraMap R S) r
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✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)
s : S
hs : s ∈ quasispectrum S a
⊢ (algebraMap R S) (f s) = s

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 S T
inst✝² : Algebra T A
inst✝¹ : IsScalarTower R T A
inst✝ : IsScalarTower S T A
⊢ (LinearMap.mul T (A ⊗[S] C ⊗[R] D)).compr₂ ↑(AlgebraTensorModule.assoc R S T A C D) =
    (LinearMap.mul T (A ⊗[S] (C ⊗[R] D)) ∘ₗ ↑(AlgebraTensorModule.assoc R S T A C D)).compl₂
      ↑(AlgebraTensorModule.assoc R S T A C D)

Tactic:
by

Goal state after:
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✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S 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✝³¹ : 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
T : Type u_3
A : Type u_4
B : Type u_5
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring A
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra T A
inst✝⁴ : IsScalarTower R T A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Algebra S T
inst✝ : IsScalarTower S T A
⊢ (AlgebraTensorModule.cancelBaseChange R S T A B).symm 1 = 1

Tactic:
by

Goal state after:
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✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ ⇑(algebraMap R S) '' spectrum R a = spectrum S a

Tactic:
by

Goal state after:
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✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ f '' spectrum S a = spectrum R a

Tactic:
by

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

Goal state before:
pp: S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module R A
inst✝³ : Module S A
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f

Tactic:
by

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

Goal state before:
pp: R : Type u_3
S' : Type u_4
A : Type u_5
S : Type u_6
inst✝¹³ : Semifield R
inst✝¹² : Semifield S'
inst✝¹¹ : Field S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R A
inst✝⁸ : Module S' A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower S' S A
inst✝ : IsScalarTower R S A
a : A
f : S' → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f

Tactic:
by

Goal state after:
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✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts a f

Tactic:
by

Goal state after: