awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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))ᶜᶜ
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
have a₃ : resolventSet R a = ⋂ (i : ι), resolventSet R (a i)
Tactic: simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
have 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))})
Tactic: simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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))})
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
have 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))}
Tactic: simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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))}
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
have 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))}
Tactic: simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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))}
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
have 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))}
Tactic: simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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
⊢ spectrum R (a, b) = spectrum R a ∪ spectrum R b
have a₁ : (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
Tactic: apply compl_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
have a₁ : (resolventSet R (a, b))ᶜᶜ = ((resolventSet R a)ᶜ ∪ (resolventSet R b)ᶜ)ᶜ
Tactic: simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)ᶜ)ᶜ
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
have a₂ : (resolventSet R (a, b))ᶜᶜ = (resolventSet R a)ᶜᶜ ∩ (resolventSet R b)ᶜᶜ
Tactic: simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)ᶜᶜ
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
have a₃ : resolventSet R (a, b) = resolventSet R a ∩ resolventSet R b
Tactic: simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
have 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)})
Tactic: simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)})
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
have 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)}
Tactic: simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)}
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
have 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)}
Tactic: simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)}
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ
have 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)}
Tactic: simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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
⊢ quasispectrum R a = ⋃ (i : ι), quasispectrum R (a i)
have h : ∀ (r : R), r ∈ quasispectrum R a ↔ Membership.mem (γ := Set R) (⋃ (i : ι), quasispectrum R (a i)) r
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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 ∈ quasispectrum R a ↔ Membership.mem (γ := Set R) (⋃ (i : ι), quasispectrum R (a i)) r
have h : (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
  ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
Tactic: simp only [quasispectrum, Set.mem_setOf_eq, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
have pos : ∀ (hr : IsUnit r),
  (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
Tactic: by_cases hr : IsUnit r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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))
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
have neg : ∀ (hr : ¬IsUnit r),
  (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔
    ∃ (i : ι), ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
Tactic: by_cases hr : IsUnit r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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))
have pos : ∀ (r' : Rˣ) (hr' : (↑r' : R) = r),
  (∀ (hr : IsUnit (↑r' : R)), ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) sorry)⁻¹ : Rˣ) a)) ↔
    ∃ (i : ι),
      ∀ (hr : IsUnit (↑r' : R)),
        ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) sorry)⁻¹ : Rˣ) (a i))
Tactic: lift r to Rˣ using hr with r' hr'
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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
⊢ quasispectrum R (a, b) = quasispectrum R a ∪ quasispectrum R b
have a₁ : (quasispectrum R (a, b))ᶜ = (quasispectrum R a ∪ quasispectrum R b)ᶜ
Tactic: apply compl_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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
⊢ (quasispectrum R (a, b))ᶜ = (quasispectrum R a ∪ quasispectrum R b)ᶜ
have a₁ : ∀ (r : R), r ∈ (quasispectrum R (a, b))ᶜ ↔ r ∈ (quasispectrum R a ∪ quasispectrum R b)ᶜ
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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 ∈ (quasispectrum R (a, b))ᶜ ↔ r ∈ (quasispectrum R a ∪ quasispectrum R b)ᶜ
have a₁ : (∃ (h : IsUnit r), IsQuasiregular (-(sorry.unit⁻¹ • (a, b)))) ↔
  ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
Tactic: simp only [quasispectrum, Set.mem_compl_iff, Set.mem_setOf_eq, not_forall, not_not, Set.mem_union]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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
⊢ (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
have pos : ∀ (hr : IsUnit r),
  (∃ (h : IsUnit r), IsQuasiregular (-(sorry.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
Tactic: by_cases hr : IsUnit r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)))
⊢ (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
have neg : ∀ (hr : ¬IsUnit r),
  (∃ (h : IsUnit r), IsQuasiregular (-(sorry.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))
Tactic: by_cases hr : IsUnit r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
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)))
have pos : ∀ (r' : Rˣ) (hr' : (↑r' : R) = r),
  (∃ (h : IsUnit (↑r' : R)), IsQuasiregular (-(sorry.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit (↑r' : R)),
          ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) sorry)⁻¹ : Rˣ) a)) ∨
        ∀ (hr : IsUnit (↑r' : R)), ¬IsQuasiregular (-HSMul.hSMul (α := Rˣ) ((IsUnit.unit (a := (↑r' : R)) sorry)⁻¹ : Rˣ) b))
Tactic: lift r to Rˣ using hr with r' hr'
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y z : PreQuasiregular R
⊢ Eq (α := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (x * y * z) : R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (x * (y * z)) : R)
have 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))
Tactic: simp [mul_add, add_mul, mul_assoc]
-- 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 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) *
      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) =
    1
have h : HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
      ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
          Unitization R A) :
        Unitization R A) *
    HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
      ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
          Unitization R A) :
        Unitization R A) =
  HAdd.hAdd (α := Unitization R A) 1
    (↑((↑x⁻¹ : PreQuasiregular A).val + (↑x : PreQuasiregular A).val +
          (↑x : PreQuasiregular A).val * (↑x⁻¹ : PreQuasiregular A).val) :
      Unitization R A)
Tactic: convert! congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A)) using 1