mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * c * star a = b * (c * star a)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * c * star a = b * (c * star a)
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
s : Set R
h : ∀ a ∈ s, star a ∈ s
ha : a ∈ s.centralizer
y : R
hy : y ∈ s
⊢ y * star a = star a * y

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
s : Set R
h : ∀ a ∈ s, star a ∈ s
ha : a ∈ s.centralizer
y : R
hy : y ∈ s
⊢ y * star a = star a * y
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
inst✝ : Subsingleton A
a : A
⊢ (resolventSet R a)ᶜ = ∅

Tactic:
resolventSet_of_subsingleton,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ univᶜ = ∅
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 b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑ₐ r - b - ↑(IsUnit.unit ha) = a - b

Tactic:
ha.unit_spec

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑ₐ r - b - (↑ₐ r - a) = a - b
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
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
hu : IsUnit (r⁻¹ • (s • 1 - a))
⊢ IsUnit (s • 1 - a)

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
hu : IsUnit (r⁻¹ • (s • 1 - a))
⊢ IsUnit (s • 1 - 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
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ IsUnit (r • ↑ₐ (r⁻¹ • s) - a)

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ IsUnit (s • 1 - 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
r : Rˣ
a : A
⊢ r • resolvent a ↑r = resolvent (r⁻¹ • a) 1

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : A
⊢ ↑r • resolvent a ↑r = resolvent (↑r⁻¹ • a) 1
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case tmul
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
x : A
y : B
⊢ f (x ⊗ₜ[R] y) = g (x ⊗ₜ[R] y)

Tactic:
simpa using

Goal state after:
case tmul
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
x : A
y : B
⊢ f (x ⊗ₜ[R] y) = g (x ⊗ₜ[R] y)
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ˣ
⊢ 0 ∈ resolventSet R ↑a

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
⊢ IsUnit ↑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 b : A
r : R
⊢ r ∈ {r | IsUnit r} ∩ σ (a * b) ↔ r ∈ {r | IsUnit r} ∩ σ (b * a)

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
⊢ IsUnit r → (r ∈ σ (a * b) ↔ r ∈ σ (b * a))
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : star r ∈ resolventSet R a
⊢ r ∈ resolventSet R (star a)

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : star r ∈ resolventSet R a
⊢ IsUnit (r • 1 - star a)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : r ∈ resolventSet R (star a)
⊢ star r ∈ resolventSet R a

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : r ∈ resolventSet R (star a)
⊢ IsUnit (star r • 1 - a)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ a - {r} = σ (a - ↑ₐ r)

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ a - {r} = σ (a - ↑ₐ r)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : (σ a).Nonempty
⊢ σ (0 • a) = 0 • σ a

Tactic:
simpa using

Goal state after:
case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : (σ a).Nonempty
⊢ {0} = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : EquivLike F A B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (f a)

Tactic:
simpa using

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : EquivLike F A B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (f a)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : IsUnit ((algebraMap R A) μ - a)
⊢ IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : IsUnit ((algebraMap R A) μ - a)
⊢ IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)
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 x✝¹ x✝ : A ⊗[R] B
h₁ : a • b • x✝¹ = b • a • x✝¹
h₂ : a • b • x✝ = b • a • x✝
⊢ a • b • (x✝¹ + x✝) = b • a • (x✝¹ + x✝)

Tactic:
simpa using

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✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
a : A
b : B
x x✝¹ x✝ : A ⊗[R] B
h₁ : a • b • x✝¹ = b • a • x✝¹
h₂ : a • b • x✝ = b • a • x✝
⊢ a • b • x✝¹ + a • b • x✝ = b • a • x✝¹ + b • a • x✝
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a
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
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)
h_one : f (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1
x✝⁵ : A
x✝⁴ : B
x✝³ : C
x✝² : A
x✝¹ : B
x✝ : C
⊢ (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              ((((AlgebraTensorModule.curry (AlgebraTensorModule.curry ((LinearMap.mul R (A ⊗[R] B ⊗[R] C)).compr₂ ↑f)))
                    x✝⁵)
                  x✝⁴)
                x✝³)))
          x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              ((((AlgebraTensorModule.curry (AlgebraTensorModule.curry ((LinearMap.mul R D ∘ₗ ↑f).compl₂ ↑f))) x✝⁵) x✝⁴)
                x✝³)))
          x✝²)
        x✝¹)
      x✝

Tactic:
simpa using

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
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)
h_one : f (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1
x✝⁵ : A
x✝⁴ : B
x✝³ : C
x✝² : A
x✝¹ : B
x✝ : C
⊢ f ((x✝⁵ * x✝²) ⊗ₜ[R] (x✝⁴ * x✝¹) ⊗ₜ[R] (x✝³ * x✝)) = f (x✝⁵ ⊗ₜ[R] x✝⁴ ⊗ₜ[R] x✝³) * f (x✝² ⊗ₜ[R] x✝¹ ⊗ₜ[R] x✝)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0
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 : (Unitization R A)ˣ
hx : (↑x).toProd.1 = 1
⊢ x⁻¹ ∈ {x | (↑x).toProd.1 = 1}

Tactic:
simpa using

Goal state after:
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 : (Unitization R A)ˣ
hx : (↑x).toProd.1 = 1
⊢ (↑x⁻¹).toProd.1 = 1
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 : ↥(unitsFstOne R A)
⊢ PreQuasiregular.equiv.symm (PreQuasiregular.equiv (↑↑x).toProd.2 * PreQuasiregular.equiv (↑↑x⁻¹).toProd.2) =
    PreQuasiregular.equiv.symm 1

Tactic:
simpa using

Goal state after:
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 : ↥(unitsFstOne R A)
⊢ (↑(↑x)⁻¹).toProd.2 + (↑↑x).toProd.2 + (↑↑x).toProd.2 * (↑(↑x)⁻¹).toProd.2 = 0
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 : ↥(unitsFstOne R A)
⊢ PreQuasiregular.equiv.symm (PreQuasiregular.equiv (↑↑x⁻¹).toProd.2 * PreQuasiregular.equiv (↑↑x).toProd.2) =
    PreQuasiregular.equiv.symm 1

Tactic:
simpa using

Goal state after:
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 : ↥(unitsFstOne R A)
⊢ (↑↑x).toProd.2 + (↑(↑x)⁻¹).toProd.2 + (↑(↑x)⁻¹).toProd.2 * (↑↑x).toProd.2 = 0
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 : ↥(unitsFstOne R A)
⊢ ↑↑((fun x ↦
            ⟨{ val := 1 + ↑(PreQuasiregular.equiv.symm ↑x), inv := 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹), val_inv := ⋯,
                inv_val := ⋯ },
              ⋯⟩)
          ((fun x ↦
              { val := PreQuasiregular.equiv (↑↑x).toProd.2, inv := PreQuasiregular.equiv (↑↑x⁻¹).toProd.2,
                val_inv := ⋯, inv_val := ⋯ })
            x)) =
    ↑↑x

Tactic:
simpa using

Goal state after:
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 : ↥(unitsFstOne R A)
⊢ 1 + ↑(↑↑x).toProd.2 = ↑↑x
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x ↔ IsUnit (equiv x)

Tactic:
by
  simp only [IsQuasiregular, IsUnit, Equiv.apply_symm_apply,
    ← PreQuasiregular.equiv (R := R).injective.eq_iff]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ f y + f x + f x * f y = 0 ∧ f x + f y + f y * f x = 0

Tactic:
simpa using

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ f y + f x + f x * f y = 0 ∧ f x + f y + f y * f x = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • a))
⊢ IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • φ a))

Tactic:
simpa using

Goal state after:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • a))
⊢ IsQuasiregular (-((↑⋯.unit⁻¹ • 1) • φ a))
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
a : A
r : Rˣ
hr : ¬IsQuasiregular (-(r⁻¹ • a))
x✝ : IsUnit ↑r
⊢ ¬IsQuasiregular (-(x✝.unit⁻¹ • a))

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : NonUnitalRing A
inst✝ : Module R A
a : A
r : Rˣ
hr : ¬IsQuasiregular (-(r⁻¹ • a))
x✝ : IsUnit ↑r
⊢ ¬IsQuasiregular (-(r⁻¹ • a))
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ quasispectrum R a = spectrum R a ∪ {r | ¬IsUnit r}

Tactic:
by
  ext r
  rw [quasispectrum]
  simp only [Set.mem_ofPred_eq, Set.mem_union, ← imp_iff_or_not, spectrum.mem_iff]
  congr! 1 with hr
  rw [not_iff_not, isQuasiregular_iff_isUnit, ← sub_eq_add_neg, Algebra.algebraMap_eq_smul_one]
  exact (IsUnit.smul_sub_iff_sub_inv_smul hr.unit a).symm

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
y : Unitization R A
hy₁ : y + ↑a + ↑a * y = 0
hy₂ : ↑a + y + y * ↑a = 0
⊢ y.toProd.1 = 0

Tactic:
simpa using

Goal state after:
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
y : Unitization R A
hy₁ : y + ↑a + ↑a * y = 0
hy₂ : ↑a + y + y * ↑a = 0
⊢ y.toProd.1 = 0
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
u : (Unitization S A)ˣ
hu : ↑u = ↑a
⊢ False

Tactic:
simpa using

Goal state after:
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
u : (Unitization S A)ˣ
hu : ↑u = ↑a
⊢ False
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:
simpa using

Goal state after:
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
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
⊢ spectrum R ↑a ∪ {0} = spectrum R ↑a

Tactic:
simpa using

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✝⁵ : 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
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case e'_3
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) ∩ {r | IsUnit r} = quasispectrum R (b * a) ∩ {r | IsUnit r}

Tactic:
simpa using

Goal state after:
case e'_3
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
⊢ {r | IsUnit r} ∩ spectrum R (↑a * ↑b) = {r | IsUnit r} ∩ spectrum R (↑b * ↑a)
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:
rw [← Set.inter_union_compl (quasispectrum R (a * b)) {r | IsUnit r},
    ← Set.inter_union_compl (quasispectrum R (b * a)) {r | IsUnit r}]
  congr! 1
  · simpa [Set.inter_comm _ {r | IsUnit r}, Unitization.quasispectrum_eq_spectrum_inr,
      Unitization.inr_mul] using spectrum.setOfPred_isUnit_inter_mul_comm _ _
  · rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]
    all_goals exact fun _ ↦ quasispectrum.not_isUnit_mem _

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

Goal state before:
pp: case refine_1
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:
simpa using

Goal state after:
case refine_1
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
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case inl
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)
hx : 0 ∈ quasispectrum S a
⊢ (algebraMap R S) (f 0) = 0

Tactic:
simpa using

Goal state after:
case inl
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)
hx : 0 ∈ quasispectrum S a
⊢ f 0 = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case inl
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)
⊢ (algebraMap R S) (f 0) = 0

Tactic:
simpa using

Goal state after:
case inl
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)
⊢ f 0 = 0