awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a → x ∈ r • σ a

Tactic:
exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
w : R
left : w ∈ σ a
x'_eq : r • w = x
⊢ r⁻¹ • x ∈ σ a

Tactic:
simpa [← x'_eq]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)

Tactic:
fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩

Premises used: HMul.hMul, HSub.hSub, IsUnit, HAdd.hAdd, Units.mk, Exists.intro, IsUnit.unit, Units.inv, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
refine_1 : ∀ (x y : A) (h : IsUnit (1 - x * y)), (1 - y * x) * (1 + y * h.unit.inv * x) = 1
refine_2 : ∀ (x y : A) (h : IsUnit (1 - x * y)), (1 + y * h.unit.inv * x) * (1 - y * x) = 1
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)

Tactic:
refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * h.unit.inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x

Tactic:
noncomm_ring
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x = 1

Tactic:
simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]

Premises used: IsUnit.mul_val_inv, Units.inv_eq_val_inv, mul_one, sub_add_cancel
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
y₁ : (1 - y * x) * (1 + y * h.unit.inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x
y₂ : 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x = 1
⊢ (1 - y * x) * (1 + y * h.unit.inv * x) = 1

Tactic:
calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd, IsUnit.unit, Units.inv, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
noncomm_ring noncomm_ring₁ noncomm_ring₂ noncomm_ring₃ :
  1 + y * (⋯.unit.inv * x) + -(y * x + y * (⋯.unit.inv * (x * (y * x)))) =
    1 + -(y * x) + (y * (⋯.unit.inv * x) + -(y * (⋯.unit.inv * (x * (y * x)))))
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x

Tactic:
noncomm_ring
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x = 1

Tactic:
simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]

Premises used: Units.inv_eq_val_inv, mul_one, IsUnit.val_inv_mul, sub_add_cancel
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
y₁ : (1 + y * h.unit.inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x
y₂ : 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x = 1
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1

Tactic:
calc
        (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd, IsUnit.unit, Units.inv, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)

Tactic:
have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) := by
    refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
    · calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
    · calc
        (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
⊢ IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)

Tactic:
have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))

Tactic:
rw [mul_smul_comm r⁻¹ b a] at this

Premises used: Inv.inv, mul_smul_comm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
⊢ (↑r : R) ∈ σ (a * b) ↔ (↑r : R) ∈ σ (b * a)

Tactic:
simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def,
    IsUnit.smul_sub_iff_sub_inv_smul, smul_mul_assoc]

Premises used: not_iff_not, IsUnit.smul_sub_iff_sub_inv_smul, smul_mul_assoc, Algebra.algebraMap_eq_smul_one, spectrum.mem_iff, Units.smul_def
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
⊢ Eq (α := Set Rˣ) (Units.val ⁻¹' σ (a * b)) (Units.val ⁻¹' σ (b * a))

Tactic:
Set.ext fun _ => unit_mem_mul_comm

Premises used: Set.ext, spectrum.unit_mem_mul_comm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
h : ∀ (r : R), r ∈ {r : R | IsUnit r} ∩ σ (a * b) ↔ r ∈ {r : R | IsUnit r} ∩ σ (b * a)
⊢ {r : R | IsUnit r} ∩ σ (a * b) = {r : R | IsUnit r} ∩ σ (b * a)

Tactic:
ext r
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : R
⊢ r ∈ {r : R | IsUnit r} ∩ σ (a * b) ↔ r ∈ {r : R | IsUnit r} ∩ σ (b * a)

Tactic:
simpa using fun hr : IsUnit r ↦ unit_mem_mul_comm (r := hr.unit)

Premises used: spectrum.unit_mem_mul_comm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

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

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
r : R
a : A
refine_1 : ∀ (h : star r ∈ resolventSet R a), r ∈ resolventSet R (star a)
refine_2 : ∀ (h : r ∈ resolventSet R (star a)), star r ∈ resolventSet R a
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
r : R
a : A
h : star r ∈ resolventSet R a
⊢ r ∈ resolventSet R (star a)

Tactic:
simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul,
      star_star, star_one] using IsUnit.star h

Premises used: IsUnit.star, star_star, StarModule.star_smul, spectrum.mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
r : R
a : A
h : r ∈ resolventSet R (star a)
⊢ star r ∈ resolventSet R a

Tactic:
simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul,
      star_star, star_one] using IsUnit.star h

Premises used: IsUnit.star, star_star, StarModule.star_smul, spectrum.mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
a : A
h : ∀ (x : R), x ∈ σ (star a) ↔ x ∈ star (σ a)
⊢ σ (star a) = star (σ a)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
a : A
x : R
⊢ x ∈ σ (star a) ↔ x ∈ star (σ a)

Tactic:
simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolventSet_iff.symm

Premises used: not_iff_not, spectrum.star_mem_resolventSet_iff, spectrum.mem_iff, Set.mem_star, Iff.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : SubringClass S A
inst_5 : SMulMemClass S R A
s : S
a : ↥s
⊢ σ (↑a : A) ⊆ σ a

Tactic:
Set.compl_subset_compl.mpr fun _ ↦ IsUnit.map (SubalgebraClass.val s)

Premises used: Iff.mpr, spectrum, Set.compl_subset_compl, IsUnit.map, SubalgebraClass.val
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
rw :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ -r + x) ⁻¹' σ a) x ↔
    x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₂ : -r + x ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₃ : x + -r ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₄ :
  x ∈ σ (HAdd.hAdd (α := A) (-(↑ₐ : (a : R) → A) (-r) : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₅ :
  x ∈ σ (HAdd.hAdd (α := A) (- -(↑ₐ : (a : R) → A) r : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₆ rw₇ :
  x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)

Tactic:
rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]

Premises used: neg_neg, map_neg, add_comm, Set.image_add_left, Set.singleton_add, spectrum.add_mem_iff, Set.mem_preimage
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
⊢ σ a + {r} = σ (HAdd.hAdd (β := A) a ((↑ₐ : (a : R) → A) r : A))

Tactic:
add_comm {r} (σ a) ▸ add_comm (algebraMap R A r) a ▸ singleton_add_eq a r

Premises used: Algebra.algebraMap, spectrum, Eq.rec, add_comm, spectrum.singleton_add_eq, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
⊢ r +ᵥ σ a = σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)

Tactic:
singleton_add.symm.trans <| singleton_add_eq a r

Premises used: spectrum.singleton_add_eq, Set.singleton_add, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
x : R
⊢ x ∈ resolventSet R (-a) ↔ x ∈ -resolventSet R a

Tactic:
simp only [mem_neg, mem_resolventSet_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]

Premises used: Set.mem_neg, map_neg, IsUnit.neg_iff, spectrum.mem_resolventSet_iff, neg_add', sub_neg_eq_add
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
rw : -(resolventSet R a)ᶜ = σ (-a)
rw₁ : (-resolventSet R a)ᶜ = σ (-a)
rw₂ : (-resolventSet R a)ᶜ = (resolventSet R (-a))ᶜ
rw₃ rw₄ : (-resolventSet R a)ᶜ = (-resolventSet R a)ᶜ
⊢ -σ a = σ (-a)

Tactic:
rw [spectrum, Set.compl_neg, spectrum, resolventSet_neg]

Premises used: spectrum, Set.compl_neg, resolventSet_neg
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
rw : {r} + -σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ : {r} + σ (-a) = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₂ : σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) (-a)) = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₃ rw₄ :
  σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) (-a)) = σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) (-a))
⊢ {r} - σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)

Tactic:
rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]

Premises used: sub_eq_add_neg, spectrum.singleton_add_eq, spectrum.neg_eq
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
⊢ σ a - {r} = σ (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) r : A))

Tactic:
simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)

Premises used: neg_sub, congr_arg, spectrum.singleton_sub_eq, spectrum.neg_eq, Neg.neg
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : Aˣ
inl : 0⁻¹ ∈ spectrum R (↑a : A) ↔ 0 ∈ spectrum R (↑a⁻¹ : A)
inr : ∀ (hr : r ≠ 0), r⁻¹ ∈ spectrum R (↑a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)
⊢ r⁻¹ ∈ spectrum R (↑a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)

Tactic:
obtain (rfl | hr) := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
a : Aˣ
⊢ 0⁻¹ ∈ spectrum R (↑a : A) ↔ 0 ∈ spectrum R (↑a⁻¹ : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : Aˣ
hr : r ≠ 0
⊢ IsUnit r

Tactic:
hr.isUnit

Premises used: Ne.isUnit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : Aˣ
hr : r ≠ 0
inr : ∀ (r : Rˣ) (hr : (↑r : R) ≠ 0), (↑r : R)⁻¹ ∈ spectrum R (↑a : A) ↔ (↑r : R) ∈ spectrum R (↑a⁻¹ : A)
⊢ r⁻¹ ∈ spectrum R (↑a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)

Tactic:
lift r to Rˣ using hr.isUnit

Premises used: Ne.isUnit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
a : Aˣ
r : Rˣ
hr : (↑r : R) ≠ 0
⊢ (↑r : R)⁻¹ ∈ spectrum R (↑a : A) ↔ (↑r : R) ∈ spectrum R (↑a⁻¹ : A)

Tactic:
simp [inv_mem_iff]

Premises used: spectrum.inv_mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : Aˣ
⊢ r⁻¹ ∈ spectrum R (↑a⁻¹ : A) ↔ r ∈ spectrum R (↑a : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
⊢ {0} ⊆ spectrum.{u, v} 𝕜 (A := A) 0

Tactic:
simp [Algebra.algebraMap_eq_smul_one, mem_iff]

Premises used: Algebra.algebraMap_eq_smul_one, spectrum.mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
refine : spectrum.{u, v} 𝕜 (A := A) 0 ⊆ {0}
⊢ spectrum.{u, v} 𝕜 (A := A) 0 = {0}

Tactic:
refine Set.Subset.antisymm ?_ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
rw : {0}ᶜ ⊆ resolventSet.{u, v} 𝕜 (A := A) 0
⊢ spectrum.{u, v} 𝕜 (A := A) 0 ⊆ {0}

Tactic:
rw [spectrum, Set.compl_subset_comm]

Premises used: spectrum, Set.compl_subset_comm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
hk : Membership.mem (γ := Set 𝕜) {0}ᶜ k
⊢ k ≠ 0

Tactic:
rw [Set.mem_compl_singleton_iff] at hk

Premises used: Set.mem_compl_singleton_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
hk : k ≠ 0
⊢ IsUnit (HSMul.hSMul (α := 𝕜ˣ) (β := A) (Units.mk0 k hk) 1)

Tactic:
have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
hk : k ≠ 0
this : IsUnit (HSMul.hSMul (α := 𝕜ˣ) (β := A) (Units.mk0 k hk) 1)
⊢ k ∈ resolventSet.{u, v} 𝕜 (A := A) 0

Tactic:
simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]

Premises used: spectrum.mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
rw : σ (HAdd.hAdd (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) (0 : A)) = {k}
rw₁ : {k} + spectrum.{u, v} 𝕜 (A := A) 0 = {k}
rw₂ : HAdd.hAdd (α := Set 𝕜) {k} {0} = {k}
rw₃ : Eq (α := Set 𝕜) {k + 0} {k}
rw₄ rw₅ : Eq (α := Set 𝕜) {k} {k}
⊢ spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) k : A) = {k}

Tactic:
rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]

Premises used: Set.singleton_add_singleton, spectrum.singleton_add_eq, add_zero, spectrum.zero_eq
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
rw : spectrum.{u, v} 𝕜 (A := A) 1 = σ (HSMul.hSMul.{u, v, v} (α := 𝕜) (β := A) 1 1)
rw₁ rw₂ : spectrum.{u, v} 𝕜 (A := A) 1 = spectrum.{u, v} 𝕜 (A := A) 1
⊢ spectrum.{u, v} 𝕜 (A := A) 1 = spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) 1 : A)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, one_smul]

Premises used: one_smul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
inl : σ (HSMul.hSMul.{u, v, v} (α := 𝕜) 0 a) = HSMul.hSMul (α := 𝕜) 0 (σ a)
inr : ∀ (h : k ≠ 0), σ (k • a) = k • σ a
⊢ σ (k • a) = k • σ a

Tactic:
rcases eq_or_ne k 0 with (rfl | h)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
a : A
ha : (σ a).Nonempty
⊢ σ (HSMul.hSMul.{u, v, v} (α := 𝕜) 0 a) = HSMul.hSMul (α := 𝕜) 0 (σ a)

Tactic:
simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)

Premises used: Set.zero_smul_set, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
h : k ≠ 0
⊢ σ (k • a) = k • σ a

Tactic:
unit_smul_eq_smul a (Units.mk0 k h)

Premises used: Units.mk0, spectrum.unit_smul_eq_smul
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
h : k ≠ 0
⊢ σ (k • a) = k • σ a

Tactic:
exact unit_smul_eq_smul a (Units.mk0 k h)

Premises used: Units.mk0, spectrum.unit_smul_eq_smul
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a b : A
suffices : ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}

Tactic:
suffices h : ∀ x y : A, σ (x * y) \ {0} ⊆ σ (y * x) \ {0} from
    Set.eq_of_subset_of_subset (h a b) (h b a)
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a b x y : A
k : 𝕜
k_mem : k ∈ σ (x * y)
k_ne : k ∉ {0}
⊢ (↑(Units.mk0 k k_ne) : 𝕜) ∈ σ (x * y)

Tactic:
change ((Units.mk0 k k_ne) : 𝕜) ∈ _ at k_mem

Premises used: Units.val, Units.mk0
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a b x y : A
k : 𝕜
k_ne : k ∉ {0}
k_mem : (↑(Units.mk0 k k_ne) : 𝕜) ∈ σ (x * y)
⊢ k ∈ σ (y * x) \ {0}

Tactic:
⟨unit_mem_mul_comm.mp k_mem, k_ne⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro, Iff.mp, spectrum.unit_mem_mul_comm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a b x y : A
k : 𝕜
k_ne : k ∉ {0}
k_mem : (↑(Units.mk0 k k_ne) : 𝕜) ∈ σ (x * y)
⊢ k ∈ σ (y * x) \ {0}

Tactic:
exact ⟨unit_mem_mul_comm.mp k_mem, k_ne⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : Aˣ
h : ∀ (x : 𝕜), x ∈ (σ (↑a : A))⁻¹ ↔ x ∈ σ (↑a⁻¹ : A)
⊢ (σ (↑a : A))⁻¹ = σ (↑a⁻¹ : A)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : Aˣ
x : 𝕜
⊢ x ∈ (σ (↑a : A))⁻¹ ↔ x ∈ σ (↑a⁻¹ : A)

Tactic:
simp
-- 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 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ : F
a : A
r : R
h : r ∈ resolventSet R a
⊢ r ∈ resolventSet.{u_2, u_4} R (A := B) ((φ : (a : A) → B) a : B)

Tactic:
simpa only [map_sub, AlgHomClass.commutes] using h.map φ

Premises used: map_sub, AlgHomClass.commutes, IsUnit.map
-- 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 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ : F
a : A
⊢ spectrum.{u_2, u_4} R (A := B) ((φ : (a : A) → B) a : B) ⊆ σ a

Tactic:
fun _ =>
  mt (mem_resolventSet_apply φ)

Premises used: spectrum, Set.Mem, setOf, mt, Set.Subset, Not, AlgHom.mem_resolventSet_apply
-- 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:
simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
      Algebra.algebraMap_self, RingHom.id_apply, sub_self]

Premises used: map_sub, RingHom.id_apply, sub_self, Algebra.algebraMap_self, RingHom.coe_coe, RingHom.mem_ker, AlgHomClass.commutes