awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ quasispectrum.{u_4, u_7} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
have refine : ∀ x ∈ (quasispectrum R a)ᶜ, x ∈ (quasispectrum.{u_4, u_7} R (A := B) ((φ : (a : A) → B) a : B))ᶜ
Tactic: refine Set.compl_subset_compl.mp fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 ∈ (quasispectrum R a)ᶜ → x ∈ (quasispectrum.{u_4, u_7} R (A := B) ((φ : (a : A) → B) a : B))ᶜ
have simp : ∀ (x_1 : IsUnit x) (h : IsQuasiregular (-(sorry.unit⁻¹ • a))),
  ∃ (h : IsUnit x), IsQuasiregular (-HSMul.hSMul (β := B) sorry.unit⁻¹ ((φ : (a : A) → B) a : B))
Tactic: simp only [quasispectrum, Set.mem_compl_iff, Set.mem_setOf_eq, not_forall, not_not,
    forall_exists_index]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
have refine : ∀ (hx : IsUnit x) (this : IsQuasiregular (-(sorry.unit⁻¹ • a))),
  IsQuasiregular (-HSMul.hSMul (β := B) sorry.unit⁻¹ ((φ : (a : A) → B) a : B))
Tactic: refine fun hx this ↦ ⟨hx, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ IsQuasiregular (-HSMul.hSMul (β := B) ⋯.unit⁻¹ ((φ : (a : A) → B) a : B))
have rw : ∀ (this : IsQuasiregular (-(HSMul.hSMul (β := S) (↑sorry.unit⁻¹ : R) 1 • a))),
  IsQuasiregular (-HSMul.hSMul (β := B) (HSMul.hSMul (β := S) (↑sorry.unit⁻¹ : R) 1) ((φ : (a : A) → B) a : B))
Tactic: rw [Units.smul_def, ← smul_one_smul S] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
⊢ quasispectrum R a = spectrum R a ∪ {r : R | ¬IsUnit r}
have h : ∀ (r : R), r ∈ quasispectrum R a ↔ r ∈ spectrum R a ∪ {r : R | ¬IsUnit r}
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ Membership.mem (γ := Set R) {r : R | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))} r ↔
    r ∈ spectrum R a ∪ {r : R | ¬IsUnit r}
have h : (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
  IsUnit r → ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)
Tactic: simp only [Set.mem_setOf_eq, Set.mem_union, ← imp_iff_or_not, spectrum.mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    IsUnit r → ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)
have h : ∀ (hr : IsUnit r),
  ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)
Tactic: congr! 1 with hr
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)
have h : IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (HSMul.hSMul (β := A) r 1 - a)
Tactic: rw [not_iff_not, isQuasiregular_iff_isUnit, ← sub_eq_add_neg, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 ∪ {0}
have h : Eq (α := Set R) {0} {r : R | ¬IsUnit r}
Tactic: convert! quasispectrum_eq_spectrum_union R a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
have refine : ∀ (ha : IsQuasiregular (R := Unitization R A) (↑a : Unitization R A)), IsQuasiregular a
Tactic: refine ⟨fun ha ↦ ?_, IsQuasiregular.map (inrNonUnitalAlgHom R A)⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ IsQuasiregular a
have 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
Tactic: rw [isQuasiregular_iff] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0
have 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
Tactic: obtain ⟨y, hy₁, hy₂⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 : A), y + a + a * y = 0 ∧ a + y + y * a = 0
have 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
Tactic: lift y to A using by simpa using congr(fstHom R A $(hy₁))
Cleared hypotheses: y, hy₁, hy₂
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
have refine_1 : y + a + a * y = 0
Tactic: refine ⟨y, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ ∃ (y : A), y + a + a * y = 0 ∧ a + y + y * a = 0
have refine_2 : a + y + y * a = 0
Tactic: refine ⟨y, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ 0 ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)
have rw : ¬IsUnit (M := Unitization S A) (↑a : Unitization S A)
Tactic: rw [spectrum.zero_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ quasispectrum R a = spectrum R (A := Unitization R A) (↑a : Unitization R A)
have h : ∀ (r : R), r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization R A) (↑a : Unitization R A)
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
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 ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization R A) (↑a : Unitization R A)
have this : {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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization R A) (↑a : Unitization R A)
have h : r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization R A) (↑a : Unitization R A)
Tactic: rw [← Set.union_eq_left.mpr this, ← quasispectrum_eq_spectrum_union]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization R A) (↑a : Unitization R A)
have apply : ∀ (hr : IsUnit r),
  ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
Tactic: apply forall_congr' fun hr ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
have rw : 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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
have rw₁ : IsQuasiregular (-((↑hr.unit⁻¹ : R) • 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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
have rw₂ : IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔
  IsQuasiregular (-HSMul.hSMul (β := Unitization R A) (↑hr.unit⁻¹ : R) (↑a : Unitization R A))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
have rw₃ : IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔
  IsQuasiregular (R := Unitization R A) (-(↑((↑hr.unit⁻¹ : R) • a) : Unitization R A))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
have rw₄ : IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔
  IsQuasiregular (R := Unitization R A) (↑(-((↑hr.unit⁻¹ : R) • a)) : Unitization R A)
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization R A) hr.unit⁻¹ (↑a : Unitization R A))
have rw₅ : IsQuasiregular (-((↑hr.unit⁻¹ : R) • a)) ↔ IsQuasiregular (-((↑hr.unit⁻¹ : R) • a))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ quasispectrum R a = spectrum R (A := Unitization S A) (↑a : Unitization S A)
have h : ∀ (r : R), r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
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
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)
have this : {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)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)
have h : r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization S A) (↑a : Unitization S A)
Tactic: rw [← Set.union_eq_self_of_subset_right this, ← quasispectrum_eq_spectrum_union_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization S A) (↑a : Unitization S A)
have apply : ∀ (x : IsUnit r),
  ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
Tactic: apply forall_congr' fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
x : IsUnit r
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
have rw : IsQuasiregular (-(x.unit⁻¹ • a)) ↔ IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
x : IsUnit r
rw :
  IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
have rw₁ : IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
  IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
x : IsUnit r
rw :
  IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
rw₁ :
  IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
have rw₂ : IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
  IsQuasiregular (-HSMul.hSMul (β := Unitization S A) (↑x.unit⁻¹ : R) (↑a : Unitization S A))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]