awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : NonUnitalRing A
inst_3 : NonUnitalRing B
inst_4 : Module R S
inst_5 : Module S A
inst_6 : Module R A
inst_7 : Module S B
inst_8 : Module R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : FunLike F A B
inst_12 : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
simp :
  ∀ (x_1 : IsUnit x) (h : IsQuasiregular (-(⋯.unit⁻¹ • a))),
    ∃ (h : IsUnit x), IsQuasiregular (-HSMul.hSMul (β := B) ⋯.unit⁻¹ ((φ : (a : A) → B) a : B))
⊢ x ∈ (quasispectrum R a)ᶜ → x ∈ (quasispectrum.{u_4, u_7} R (A := B) ((φ : (a : A) → B) a : B))ᶜ

Tactic:
simp only [quasispectrum, Set.mem_compl_iff, Set.mem_setOf_eq, not_forall, not_not,
    forall_exists_index]

Premises used: Classical.not_not, quasispectrum, forall_exists_index, Set.mem_setOf_eq, Classical.not_forall, Set.mem_compl_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : NonUnitalRing A
inst_3 : NonUnitalRing B
inst_4 : Module R S
inst_5 : Module S A
inst_6 : Module R A
inst_7 : Module S B
inst_8 : Module R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : FunLike F A B
inst_12 : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
⊢ ∀ (x_1 : IsUnit x) (h : IsQuasiregular (-(⋯.unit⁻¹ • a))),
    ∃ (h : IsUnit x), IsQuasiregular (-HSMul.hSMul (β := B) ⋯.unit⁻¹ ((φ : (a : A) → B) a : B))

Tactic:
fun hx this ↦ ⟨hx, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : NonUnitalRing A
inst_3 : NonUnitalRing B
inst_4 : Module R S
inst_5 : Module S A
inst_6 : Module R A
inst_7 : Module S B
inst_8 : Module R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : FunLike F A B
inst_12 : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
refine :
  ∀ (hx : IsUnit x) (this : IsQuasiregular (-(⋯.unit⁻¹ • a))),
    IsQuasiregular (-HSMul.hSMul (β := B) ⋯.unit⁻¹ ((φ : (a : A) → B) a : B))
⊢ ∀ (x_1 : IsUnit x) (h : IsQuasiregular (-(⋯.unit⁻¹ • a))),
    ∃ (h : IsUnit x), IsQuasiregular (-HSMul.hSMul (β := B) ⋯.unit⁻¹ ((φ : (a : A) → B) a : B))

Tactic:
refine fun hx this ↦ ⟨hx, ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : NonUnitalRing A
inst_3 : NonUnitalRing B
inst_4 : Module R S
inst_5 : Module S A
inst_6 : Module R A
inst_7 : Module S B
inst_8 : Module R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : FunLike F A B
inst_12 : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-(⋯.unit⁻¹ • a))
rw :
  ∀ (this : IsQuasiregular (-(HSMul.hSMul (β := S) (↑⋯.unit⁻¹ : R) 1 • a))),
    IsQuasiregular (-HSMul.hSMul (β := B) (HSMul.hSMul (β := S) (↑⋯.unit⁻¹ : R) 1) ((φ : (a : A) → B) a : B))
⊢ IsQuasiregular (-HSMul.hSMul (β := B) ⋯.unit⁻¹ ((φ : (a : A) → B) a : B))

Tactic:
rw [Units.smul_def, ← smul_one_smul S] at this ⊢

Premises used: smul_one_smul, Units.smul_def
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : NonUnitalRing A
inst_3 : NonUnitalRing B
inst_4 : Module R S
inst_5 : Module S A
inst_6 : Module R A
inst_7 : Module S B
inst_8 : Module R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : FunLike F A B
inst_12 : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-(HSMul.hSMul (β := S) (↑⋯.unit⁻¹ : R) 1 • a))
⊢ IsQuasiregular (-HSMul.hSMul (β := B) (HSMul.hSMul (β := S) (↑⋯.unit⁻¹ : R) 1) ((φ : (a : A) → B) a : B))

Tactic:
simpa [-smul_assoc] using this.map φ

Premises used: IsQuasiregular.map, smul_assoc
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
A : Type u_5
B : Type u_6
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
φ : F
a : A
⊢ quasispectrum.{u_4, u_6} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a

Tactic:
NonUnitalAlgHom.quasispectrum_apply_subset' R φ a

Premises used: NonUnitalAlgHom.quasispectrum_apply_subset'
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Nontrivial R
a : A
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
a : A
r : Rˣ
hr : ¬IsQuasiregular (-(r⁻¹ • a))
h : IsUnit (↑r : R)
⊢ ¬IsQuasiregular (-(h.unit⁻¹ • a))

Tactic:
simpa using hr
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : ∀ (r : R), r ∈ quasispectrum R a ↔ r ∈ spectrum R a ∪ {r : R | ¬IsUnit r}
⊢ quasispectrum R a = spectrum R a ∪ {r : R | ¬IsUnit r}

Tactic:
ext r
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
h :
  (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    IsUnit r → ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)
⊢ Membership.mem (γ := Set R) {r : R | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))} r ↔
    r ∈ spectrum R a ∪ {r : R | ¬IsUnit r}

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_union, ← imp_iff_or_not, spectrum.mem_iff]

Premises used: Set.mem_union, Set.mem_setOf_eq, spectrum.mem_iff, imp_iff_or_not
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
h :
  ∀ (hr : IsUnit r),
    ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    IsUnit r → ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)

Tactic:
congr! 1 with hr
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
hr : IsUnit r
h : IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (HSMul.hSMul (β := A) r 1 - a)
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)

Tactic:
rw [not_iff_not, isQuasiregular_iff_isUnit, ← sub_eq_add_neg, Algebra.algebraMap_eq_smul_one]

Premises used: not_iff_not, sub_eq_add_neg, isQuasiregular_iff_isUnit, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (HSMul.hSMul (β := A) r 1 - a)

Tactic:
(IsUnit.smul_sub_iff_sub_inv_smul hr.unit a).symm

Premises used: IsUnit.smul_sub_iff_sub_inv_smul, IsUnit.unit, Iff.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (HSMul.hSMul (β := A) r 1 - a)

Tactic:
exact (IsUnit.smul_sub_iff_sub_inv_smul hr.unit a).symm

Premises used: IsUnit.smul_sub_iff_sub_inv_smul, IsUnit.unit, Iff.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
⊢ spectrum R a ⊆ quasispectrum R a

Tactic:
quasispectrum_eq_spectrum_union R a ▸ Set.subset_union_left

Premises used: quasispectrum_eq_spectrum_union, Eq.rec, Set.subset_union_left, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
⊢ quasispectrum R a = spectrum R a ∪ {r : R | ¬IsUnit r}

Tactic:
quasispectrum_eq_spectrum_union R a

Premises used: quasispectrum_eq_spectrum_union
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : Eq (α := Set R) {0} {r : R | ¬IsUnit r}
⊢ quasispectrum R a = spectrum R a ∪ {0}

Tactic:
convert! quasispectrum_eq_spectrum_union R a

Premises used: quasispectrum_eq_spectrum_union
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
⊢ Eq (α := Set R) {0} {r : R | ¬IsUnit r}

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
x : R
⊢ x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a

Tactic:
simp [quasispectrum_eq_spectrum_union_zero]

Premises used: quasispectrum_eq_spectrum_union_zero
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
⊢ IsQuasiregular (R := Unitization R A) (↑a : Unitization R A) ↔ IsQuasiregular a

Tactic:
⟨fun ha ↦ ?_, IsQuasiregular.map (inrNonUnitalAlgHom R A)⟩

Premises used: IsQuasiregular.map, Unitization.inrNonUnitalAlgHom, Iff.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
refine : ∀ (ha : IsQuasiregular (R := Unitization R A) (↑a : Unitization R A)), IsQuasiregular a
⊢ IsQuasiregular (R := Unitization R A) (↑a : Unitization R A) ↔ IsQuasiregular a

Tactic:
refine ⟨fun ha ↦ ?_, IsQuasiregular.map (inrNonUnitalAlgHom R A)⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
ha : IsQuasiregular (R := Unitization R A) (↑a : Unitization R A)
rw :
  ∀
    (ha :
      ∃ (y : Unitization R A),
        y + (↑a : Unitization R A) + (↑a : Unitization R A) * y = 0 ∧
          (↑a : Unitization R A) + y + y * (↑a : Unitization R A) = 0),
    ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0
⊢ IsQuasiregular a

Tactic:
rw [isQuasiregular_iff] at ha ⊢

Premises used: isQuasiregular_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
ha :
  ∃ (y : Unitization R A),
    y + (↑a : Unitization R A) + (↑a : Unitization R A) * y = 0 ∧
      (↑a : Unitization R A) + y + y * (↑a : Unitization R A) = 0
obtain :
  ∀ (y : Unitization R A) (hy₁ : y + (↑a : Unitization R A) + (↑a : Unitization R A) * y = 0)
    (hy₂ : (↑a : Unitization R A) + y + y * (↑a : Unitization R A) = 0),
    ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0
⊢ ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := ha
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
y : Unitization R A
hy₁ : y + (↑a : Unitization R A) + (↑a : Unitization R A) * y = 0
hy₂ : (↑a : Unitization R A) + y + y * (↑a : Unitization R A) = 0
⊢ y.toProd.1 = 0

Tactic:
simpa using congr(fstHom R A $(hy₁))
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
y : Unitization R A
hy₁ : y + (↑a : Unitization R A) + (↑a : Unitization R A) * y = 0
hy₂ : (↑a : Unitization R A) + y + y * (↑a : Unitization R A) = 0
lift :
  ∀ (y : A)
    (hy₁ :
      HAdd.hAdd (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) +
          HMul.hMul (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) =
        0)
    (hy₂ :
      HAdd.hAdd (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) +
          HMul.hMul (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) =
        0),
    ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0
⊢ ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
lift y to A using by simpa using congr(fstHom R A $(hy₁))
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a y : A
hy₁ :
  HAdd.hAdd (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) =
    0
hy₂ :
  HAdd.hAdd (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) =
    0
⊢ ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
⟨y, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a y : A
hy₁ :
  HAdd.hAdd (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) =
    0
hy₂ :
  HAdd.hAdd (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) =
    0
refine_1 : y + a + a * y = 0
refine_2 : a + y + y * a = 0
⊢ ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
refine ⟨y, ?_, ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a y : A
hy₁ :
  HAdd.hAdd (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) =
    0
hy₂ :
  HAdd.hAdd (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) =
    0
⊢ Eq (α := Unitization R A) (↑(y + a + a * y) : Unitization R A) (↑0 : Unitization R A)

Tactic:
simpa
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a y : A
hy₁ :
  HAdd.hAdd (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) =
    0
hy₂ :
  HAdd.hAdd (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) =
    0
⊢ y + a + a * y = 0

Tactic:
exact inr_injective (R := R) <| by simpa

Premises used: Unitization.inr_injective
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a y : A
hy₁ :
  HAdd.hAdd (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) =
    0
hy₂ :
  HAdd.hAdd (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) =
    0
⊢ Eq (α := Unitization R A) (↑(a + y + y * a) : Unitization R A) (↑0 : Unitization R A)

Tactic:
simpa
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a y : A
hy₁ :
  HAdd.hAdd (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) =
    0
hy₂ :
  HAdd.hAdd (α := Unitization R A) (↑a : Unitization R A) (↑y : Unitization R A) +
      HMul.hMul (α := Unitization R A) (↑y : Unitization R A) (↑a : Unitization R A) =
    0
⊢ a + y + y * a = 0

Tactic:
exact inr_injective (R := R) <| by simpa

Premises used: Unitization.inr_injective
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : NonUnitalRing A
inst_4 : Algebra R S
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : Module R A
inst_9 : IsScalarTower R S A
a : A
rw : ¬IsUnit (M := Unitization S A) (↑a : Unitization S A)
⊢ 0 ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)

Tactic:
rw [spectrum.zero_mem_iff]

Premises used: spectrum.zero_mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : NonUnitalRing A
inst_4 : Algebra R S
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : Module R A
inst_9 : IsScalarTower R S A
a : A
u : (Unitization S A)ˣ
hu : (↑u : Unitization S A) = (↑a : Unitization S A)
⊢ False

Tactic:
simpa [-Units.mul_inv, hu] using congr($(u.mul_inv).fst)

Premises used: Units.mul_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
r : R
hr : ¬IsUnit r
h : r ∈ resolventSet R (A := Unitization R A) (↑a : Unitization R A)
⊢ IsUnit r

Tactic:
simpa [map_sub] using h.map (fstHom R A)

Premises used: map_sub, Unitization.fstHom, IsUnit.map
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
h : ∀ (r : R), r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization R A) (↑a : Unitization R A)
⊢ quasispectrum R a = spectrum R (A := Unitization R A) (↑a : Unitization R A)

Tactic:
ext r
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
r : R
⊢ {r : R | ¬IsUnit r} ⊆ spectrum R (A := Unitization R A) (↑a : Unitization R A)

Tactic:
have : { r | ¬ IsUnit r} ⊆ spectrum R _ := mem_spectrum_inr_of_not_isUnit a
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
r : R
this : {r : R | ¬IsUnit r} ⊆ spectrum R (A := Unitization R A) (↑a : Unitization R A)
h : r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization R A) (↑a : Unitization R A)
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization R A) (↑a : Unitization R A)

Tactic:
rw [← Set.union_eq_left.mpr this, ← quasispectrum_eq_spectrum_union]

Premises used: Iff.mpr, quasispectrum_eq_spectrum_union, Set.union_eq_left
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
r : R
this : {r : R | ¬IsUnit r} ⊆ spectrum R (A := Unitization R A) (↑a : Unitization R A)
apply :
  ∀ (hr : IsUnit r),
    ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
      ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization R A) (↑a : Unitization R A)

Tactic:
apply forall_congr' fun hr ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
r : R
this : {r : R | ¬IsUnit r} ⊆ spectrum R (A := Unitization R A) (↑a : Unitization R A)
hr : IsUnit r
rw :
  IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
rw₁ :
  IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
rw₂ :
  IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization R A) (↑hr.unit⁻¹ : R) (↑a : Unitization R A))
rw₃ :
  IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (R := Unitization R A) (-(↑((↑hr.unit⁻¹ : R) • a) : Unitization R A))
rw₄ :
  IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (R := Unitization R A) (↑(-((↑hr.unit⁻¹ : R) • a)) : Unitization R A)
rw₅ rw₆ : IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔ IsQuasiregular (-((↑hr.unit⁻¹ : R) • a))
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))

Tactic:
rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

Premises used: Unitization.inr_neg, not_iff_not, Unitization.isQuasiregular_inr_iff, Unitization.inr_smul, Units.smul_def
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
h : ∀ (r : R), r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)
⊢ quasispectrum R a = spectrum R (A := Unitization S A) (↑a : Unitization S A)

Tactic:
ext r
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
r : R
⊢ {0} ⊆ spectrum R (A := Unitization S A) (↑a : Unitization S A)

Tactic:
have := Set.singleton_subset_iff.mpr (zero_mem_spectrum_inr R S a)
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
r : R
this : {0} ⊆ spectrum R (A := Unitization S A) (↑a : Unitization S A)
h : r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization S A) (↑a : Unitization S A)
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)

Tactic:
rw [← Set.union_eq_self_of_subset_right this, ← quasispectrum_eq_spectrum_union_zero]

Premises used: Set.union_eq_self_of_subset_right, quasispectrum_eq_spectrum_union_zero