awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FunLike F A R
inst_4 : AlgHomClass F R A R
inst_5 : Nontrivial R
φ : F
a : A
⊢ Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* R) (↑φ : A →+* R))
    (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) ((φ : (a : A) → R) a : R) : A) a)

Tactic:
have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
    simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
      Algebra.algebraMap_self, RingHom.id_apply, sub_self]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FunLike F A R
inst_4 : AlgHomClass F R A R
inst_5 : Nontrivial R
φ : F
a : A
h :
  Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* R) (↑φ : A →+* R))
    (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) ((φ : (a : A) → R) a : R) : A) a)
⊢ Membership.mem (α := R) (σ a) ((φ : (a : A) → R) a : R)

Tactic:
simp only [spectrum.mem_iff, ← mem_nonunits_iff,
    coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]

Premises used: mem_nonunits_iff, coe_subset_nonunits, RingHom.ker_ne_top, spectrum.mem_iff, RingHomClass.toRingHom
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : EquivLike F A B
inst_6 : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum.{u_2, u_4} R (A := B) ((f : (a : A) → B) a : B)

Tactic:
simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
      AlgHom.spectrum_apply_subset (AlgEquivClass.toAlgEquiv f : A ≃ₐ[R] B).symm (f a)

Premises used: AlgEquiv.symm, AlgEquivClass.toAlgEquiv, AlgEquiv.coe_coe_symm_apply_coe_apply, AlgEquiv.coe_algHom, AlgHom.spectrum_apply_subset, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
⊢ spectrum R ((↑u : A) * a * (↑u⁻¹ : A)) = spectrum R a

Tactic:
le_antisymm (this a u) ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
refine : spectrum R a ≤ spectrum R ((↑u : A) * a * (↑u⁻¹ : A))
⊢ spectrum R ((↑u : A) * a * (↑u⁻¹ : A)) = spectrum R a

Tactic:
refine le_antisymm (this a u) ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
apply : spectrum R a = spectrum R ((↑u⁻¹ : A) * ((↑u : A) * a * (↑u⁻¹ : A)) * (↑u⁻¹⁻¹ : A))
⊢ spectrum R a ≤ spectrum R ((↑u : A) * a * (↑u⁻¹ : A))

Tactic:
apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹

Premises used: Units.val, HMul.hMul, Inv.inv, le_of_eq_of_le
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
⊢ spectrum R a = spectrum R ((↑u⁻¹ : A) * ((↑u : A) * a * (↑u⁻¹ : A)) * (↑u⁻¹⁻¹ : A))

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
suffices : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
⊢ spectrum R ((↑u : A) * a * (↑u⁻¹ : A)) = spectrum R a

Tactic:
suffices ∀ (b : A) (v : Aˣ), spectrum R (v * b * v⁻¹) ⊆ spectrum R b by
    refine le_antisymm (this a u) ?_
    apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
    simp [mul_assoc]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a_1 : A
u_1 : Aˣ
a : A
u : Aˣ
μ : R
hμ : μ ∈ spectrum R ((↑u : A) * a * (↑u⁻¹ : A))
⊢ ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) ((↑u : A) * a * (↑u⁻¹ : A)))

Tactic:
rw [spectrum.mem_iff] at hμ ⊢

Premises used: spectrum.mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a_1 : A
u_1 : Aˣ
a : A
u : Aˣ
μ : R
hμ : ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) ((↑u : A) * a * (↑u⁻¹ : A)))
contrapose :
  ∀ (hμ : IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) a)),
    IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) ((↑u : A) * a * (↑u⁻¹ : A)))
⊢ ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) a)

Tactic:
contrapose hμ
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a_1 : A
u_1 : Aˣ
a : A
u : Aˣ
μ : R
hμ : IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) a)
⊢ IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) ((↑u : A) * a * (↑u⁻¹ : A)))

Tactic:
simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit

Premises used: mul_sub, Algebra.right_comm, IsUnit.mul, sub_mul, Inv.inv, Units.isUnit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
⊢ spectrum R ((↑u⁻¹ : A) * a * (↑u : A)) = spectrum R a

Tactic:
simpa using spectrum.units_conjugate (u := u⁻¹)

Premises used: spectrum.units_conjugate
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
κ : ι → Type u_5
inst : (i : ι) → NonUnitalSemiring (κ i)
x : (i : ι) → κ i
simp :
  (∀ (i : ι),
      IsUnit.{u_5} (M := PreQuasiregular (κ i))
        ((PreQuasiregular.toPi κ : (a : PreQuasiregular ((i : ι) → κ i)) → (i : ι) → PreQuasiregular (κ i))
            ((PreQuasiregular.equiv : (a : (i : ι) → κ i) → PreQuasiregular ((i : ι) → κ i)) x :
              PreQuasiregular ((i : ι) → κ i))
            i :
          PreQuasiregular (κ i))) ↔
    ∀ (i : ι),
      IsUnit (M := PreQuasiregular (κ i))
        ((PreQuasiregular.equiv : (a : κ i) → PreQuasiregular (κ i)) (x i) : PreQuasiregular (κ i))
⊢ IsQuasiregular x ↔ ∀ (i : ι), IsQuasiregular (x i)

Tactic:
simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toPi κ), Pi.isUnit_iff]

Premises used: isQuasiregular_iff', Pi.isUnit_iff, isUnit_map_iff, PreQuasiregular.toPi
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
κ : ι → Type u_5
inst : (i : ι) → NonUnitalSemiring (κ i)
x : (i : ι) → κ i
⊢ (∀ (i : ι),
      IsUnit.{u_5} (M := PreQuasiregular (κ i))
        ((PreQuasiregular.toPi κ : (a : PreQuasiregular ((i : ι) → κ i)) → (i : ι) → PreQuasiregular (κ i))
            ((PreQuasiregular.equiv : (a : (i : ι) → κ i) → PreQuasiregular ((i : ι) → κ i)) x :
              PreQuasiregular ((i : ι) → κ i))
            i :
          PreQuasiregular (κ i))) ↔
    ∀ (i : ι),
      IsUnit (M := PreQuasiregular (κ i))
        ((PreQuasiregular.equiv : (a : κ i) → PreQuasiregular (κ i)) (x i) : PreQuasiregular (κ i))

Tactic:
congr!
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
inst : NonUnitalSemiring A
inst_1 : NonUnitalSemiring B
a : A
b : B
simp :
  IsUnit.{u_2} (M := PreQuasiregular A)
        ((PreQuasiregular.toProd A B : (a : PreQuasiregular (A × B)) → PreQuasiregular A × PreQuasiregular B)
            ((PreQuasiregular.equiv : (a : A × B) → PreQuasiregular (A × B)) (a, b))).1 ∧
      IsUnit.{u_3} (M := PreQuasiregular B)
        ((PreQuasiregular.toProd A B : (a : PreQuasiregular (A × B)) → PreQuasiregular A × PreQuasiregular B)
            ((PreQuasiregular.equiv : (a : A × B) → PreQuasiregular (A × B)) (a, b))).2 ↔
    IsUnit (M := PreQuasiregular A) ((PreQuasiregular.equiv : (a : A) → PreQuasiregular A) a : PreQuasiregular A) ∧
      IsUnit (M := PreQuasiregular B) ((PreQuasiregular.equiv : (a : B) → PreQuasiregular B) b : PreQuasiregular B)
⊢ IsQuasiregular (a, b) ↔ IsQuasiregular a ∧ IsQuasiregular b

Tactic:
simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toProd A B), Prod.isUnit_iff]

Premises used: PreQuasiregular.toProd, Prod.isUnit_iff, isQuasiregular_iff', isUnit_map_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
inst : NonUnitalSemiring A
inst_1 : NonUnitalSemiring B
a : A
b : B
⊢ IsUnit.{u_2} (M := PreQuasiregular A)
        ((PreQuasiregular.toProd A B : (a : PreQuasiregular (A × B)) → PreQuasiregular A × PreQuasiregular B)
            ((PreQuasiregular.equiv : (a : A × B) → PreQuasiregular (A × B)) (a, b))).1 ∧
      IsUnit.{u_3} (M := PreQuasiregular B)
        ((PreQuasiregular.toProd A B : (a : PreQuasiregular (A × B)) → PreQuasiregular A × PreQuasiregular B)
            ((PreQuasiregular.equiv : (a : A × B) → PreQuasiregular (A × B)) (a, b))).2 ↔
    IsUnit (M := PreQuasiregular A) ((PreQuasiregular.equiv : (a : A) → PreQuasiregular A) a : PreQuasiregular A) ∧
      IsUnit (M := PreQuasiregular B) ((PreQuasiregular.equiv : (a : B) → PreQuasiregular B) b : PreQuasiregular B)

Tactic:
congr!
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
a : A
r : R
hr : IsUnit r
⊢ r ∈ quasispectrum R a ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • a))

Tactic:
⟨fun h => h hr, fun h _ => h⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Ring (κ i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
a₁ : (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
⊢ spectrum R a = ⋃ (i : ι), spectrum R (a i)

Tactic:
apply compl_injective

Premises used: compl_injective
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Ring (κ i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
a₁ : (resolventSet R a)ᶜᶜ = (⋃ (i : ι), (resolventSet R (a i))ᶜ)ᶜ
a₂ : (resolventSet R a)ᶜᶜ = ⋂ (i : ι), (resolventSet R (a i))ᶜᶜ
a₃ : resolventSet R a = ⋂ (i : ι), resolventSet R (a i)
a₄ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R |
      IsUnit
        (HSub.hSub (α := (i : ι) → κ i) ((algebraMap R ((i : ι) → κ i) : (a : R) → (i : ι) → κ i) r : (i : ι) → κ i) a)}
    (⋂ (i : ι), {r : R | IsUnit (HSub.hSub (α := κ i) ((algebraMap R (κ i) : (a : R) → κ i) r : κ i) (a i))})
a₅ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R |
      IsUnit
        (HSub.hSub (α := (i : ι) → κ i) ((algebraMap R ((i : ι) → κ i) : (a : R) → (i : ι) → κ i) r : (i : ι) → κ i) a)}
    {x : R | ∀ (i : ι), IsUnit (HSub.hSub (α := κ i) ((algebraMap R (κ i) : (a : R) → κ i) x : κ i) (a i))}
a₆ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R |
      ∀ (i : ι),
        IsUnit
          (HSub.hSub (α := (i : ι) → κ i) ((algebraMap R ((i : ι) → κ i) : (a : R) → (i : ι) → κ i) r : (i : ι) → κ i) a
            i)}
    {x : R | ∀ (i : ι), IsUnit (HSub.hSub (α := κ i) ((algebraMap R (κ i) : (a : R) → κ i) x : κ i) (a i))}
a₇ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R |
      ∀ (i : ι),
        IsUnit (HSub.hSub (α := κ i) ((algebraMap R ((i : ι) → κ i) : (a : R) → (i : ι) → κ i) r i : κ i) (a i))}
    {x : R | ∀ (i : ι), IsUnit (HSub.hSub (α := κ i) ((algebraMap R (κ i) : (a : R) → κ i) x : κ i) (a i))}
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ

Tactic:
simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]

Premises used: Pi.algebraMap_apply, compl_compl, spectrum, Pi.isUnit_iff, Set.compl_iUnion, Set.iInter_setOf, resolventSet, Pi.sub_apply
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
a : A
b : B
a₁ : (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
⊢ spectrum R (a, b) = spectrum R a ∪ spectrum R b

Tactic:
apply compl_injective

Premises used: compl_injective
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
a : A
b : B
a₁ : (resolventSet R (a, b))ᶜᶜ = ((resolventSet R a)ᶜ ∪ (resolventSet R b)ᶜ)ᶜ
a₂ : (resolventSet R (a, b))ᶜᶜ = (resolventSet R a)ᶜᶜ ∩ (resolventSet R b)ᶜᶜ
a₃ : resolventSet R (a, b) = resolventSet R a ∩ resolventSet R b
a₄ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R | IsUnit (HSub.hSub (α := A × B) ((algebraMap R (A × B) : (a : R) → A × B) r : A × B) (a, b))}
    ({r : R | IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) r : A) a)} ∩
      {r : R | IsUnit (HSub.hSub (α := B) ((algebraMap R B : (a : R) → B) r : B) b)})
a₅ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R | IsUnit (HSub.hSub (α := A × B) ((algebraMap R (A × B) : (a : R) → A × B) r : A × B) (a, b))}
    {a_1 : R |
      IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) a_1 : A) a) ∧
        IsUnit (HSub.hSub (α := B) ((algebraMap R B : (a : R) → B) a_1 : B) b)}
a₆ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R |
      IsUnit (HSub.hSub (α := A × B) ((algebraMap R (A × B) : (a : R) → A × B) r : A × B) (a, b)).1 ∧
        IsUnit (HSub.hSub (α := A × B) ((algebraMap R (A × B) : (a : R) → A × B) r : A × B) (a, b)).2}
    {a_1 : R |
      IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) a_1 : A) a) ∧
        IsUnit (HSub.hSub (α := B) ((algebraMap R B : (a : R) → B) a_1 : B) b)}
a₇ :
  Eq.{u_4 + 1} (α := Set R)
    {r : R |
      IsUnit
          (HSub.hSub (α := A × B) (((algebraMap R A : (a : R) → A) r, (algebraMap R B : (a : R) → B) r) : A × B)
              (a, b)).1 ∧
        IsUnit
          (HSub.hSub (α := A × B) (((algebraMap R A : (a : R) → A) r, (algebraMap R B : (a : R) → B) r) : A × B)
              (a, b)).2}
    {a_1 : R |
      IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) a_1 : A) a) ∧
        IsUnit (HSub.hSub (α := B) ((algebraMap R B : (a : R) → B) a_1 : B) b)}
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ

Tactic:
simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]

Premises used: Set.compl_union, Set.setOf_and, compl_compl, spectrum, Prod.isUnit_iff, Prod.mk_sub_mk, Prod.algebraMap_apply, resolventSet
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : Nonempty ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → NonUnitalRing (κ i)
inst_3 : (i : ι) → Module.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
h : ∀ (r : R), r ∈ quasispectrum R a ↔ Membership.mem (γ := Set R) (⋃ (i : ι), quasispectrum R (a i)) r
⊢ quasispectrum R a = ⋃ (i : ι), quasispectrum R (a i)

Tactic:
ext r
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : Nonempty ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → NonUnitalRing (κ i)
inst_3 : (i : ι) → Module.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
r : R
h :
  (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
⊢ r ∈ quasispectrum R a ↔ Membership.mem (γ := Set R) (⋃ (i : ι), quasispectrum R (a i)) r

Tactic:
simp only [quasispectrum, Set.mem_setOf_eq, Set.mem_iUnion]

Premises used: quasispectrum, Set.mem_iUnion, Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : Nonempty ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → NonUnitalRing (κ i)
inst_3 : (i : ι) → Module.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
r : R
pos :
  ∀ (hr : IsUnit r),
    (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
      ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
neg :
  ∀ (hr : ¬IsUnit r),
    (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
      ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))

Tactic:
by_cases hr : IsUnit r

Premises used: IsUnit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : Nonempty ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → NonUnitalRing (κ i)
inst_3 : (i : ι) → Module.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
r : R
hr : IsUnit r
⊢ IsUnit r

Tactic:
hr
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : Nonempty ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → NonUnitalRing (κ i)
inst_3 : (i : ι) → Module.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
r : R
hr : IsUnit r
pos :
  ∀ (r' : Rˣ) (hr' : (↑r' : R) = r),
    (∀ (hr : IsUnit (↑r' : R)), ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) a)) ↔
      ∃ (i : ι),
        ∀ (hr : IsUnit (↑r' : R)),
          ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) (a i))
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))

Tactic:
lift r to Rˣ using hr with r' hr'
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : Nonempty ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → NonUnitalRing (κ i)
inst_3 : (i : ι) → Module.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
r : R
r' : Rˣ
hr' : (↑r' : R) = r
⊢ (∀ (hr : IsUnit (↑r' : R)), ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) a)) ↔
    ∃ (i : ι),
      ∀ (hr : IsUnit (↑r' : R)),
        ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) (a i))

Tactic:
simp [isQuasiregular_pi_iff]

Premises used: isQuasiregular_pi_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : Nonempty ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → NonUnitalRing (κ i)
inst_3 : (i : ι) → Module.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
r : R
hr : ¬IsUnit r
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))

Tactic:
simp [hr]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
a₁ : (quasispectrum R (a, b))ᶜ = (quasispectrum R a ∪ quasispectrum R b)ᶜ
⊢ quasispectrum R (a, b) = quasispectrum R a ∪ quasispectrum R b

Tactic:
apply compl_injective

Premises used: compl_injective
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
a₁ : ∀ (r : R), r ∈ (quasispectrum R (a, b))ᶜ ↔ r ∈ (quasispectrum R a ∪ quasispectrum R b)ᶜ
⊢ (quasispectrum R (a, b))ᶜ = (quasispectrum R a ∪ quasispectrum R b)ᶜ

Tactic:
ext r
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
r : R
a₁ :
  (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
⊢ r ∈ (quasispectrum R (a, b))ᶜ ↔ r ∈ (quasispectrum R a ∪ quasispectrum R b)ᶜ

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

Premises used: Set.mem_union, Classical.not_not, quasispectrum, Set.mem_setOf_eq, Classical.not_forall, Set.mem_compl_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
r : R
pos :
  ∀ (hr : IsUnit r),
    (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
      ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
neg :
  ∀ (hr : ¬IsUnit r),
    (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
      ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
⊢ (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))

Tactic:
by_cases hr : IsUnit r

Premises used: IsUnit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
r : R
hr : IsUnit r
⊢ IsUnit r

Tactic:
hr
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
r : R
hr : IsUnit r
pos :
  ∀ (r' : Rˣ) (hr' : (↑r' : R) = r),
    (∃ (h : IsUnit (↑r' : R)), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
      ¬((∀ (hr : IsUnit (↑r' : R)),
            ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) a)) ∨
          ∀ (hr : IsUnit (↑r' : R)),
            ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) b))
⊢ (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))

Tactic:
lift r to Rˣ using hr with r' hr'
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
r : R
r' : Rˣ
hr' : (↑r' : R) = r
⊢ (∃ (h : IsUnit (↑r' : R)), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit (↑r' : R)),
          ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) a)) ∨
        ∀ (hr : IsUnit (↑r' : R)), ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) ⋯)⁻¹ : Rˣ) b))

Tactic:
simp [isQuasiregular_prod_iff]

Premises used: isQuasiregular_prod_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Pi
Goal:
A : Type u_2
B : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : NonUnitalRing B
inst_3 : Module R A
inst_4 : Module R B
a : A
b : B
r : R
hr : ¬IsUnit r
⊢ (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))

Tactic:
simp [hr]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
⊢ Eq.{u_1 + 1} (α := R) (val 1) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : PreQuasiregular R
⊢ (x * y).val = y.val + x.val + x.val * y.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y z : PreQuasiregular R
simp :
  z.val + (y.val + x.val + x.val * y.val) + (y.val * z.val + x.val * z.val + x.val * (y.val * z.val)) =
    z.val + y.val + y.val * z.val + x.val + (x.val * z.val + x.val * y.val + x.val * (y.val * z.val))
⊢ Eq (α := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (x * y * z) : R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (x * (y * z)) : R)

Tactic:
simp [mul_add, add_mul, mul_assoc]

Premises used: add_mul, mul_assoc, mul_add