[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (r • ↑↑ₐ s - a)
⊢ (↑↑ₐ s - r⁻¹ • a) * r • ↑(IsUnit.unit h)⁻¹ = 1
[PROOFSTEP]
rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (r • ↑↑ₐ s - a)
⊢ r • ↑(IsUnit.unit h)⁻¹ * (↑↑ₐ s - r⁻¹ • a) = 1
[PROOFSTEP]
rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬r ∈ σ a ↔ IsUnit (↑↑ₐ r - a)
[PROOFSTEP]
apply not_iff_not.mp
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬¬r ∈ σ a ↔ ¬IsUnit (↑↑ₐ r - a)
[PROOFSTEP]
simp [Set.not_not_mem, mem_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ 0 ∈ σ a ↔ ¬IsUnit a
[PROOFSTEP]
rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ ¬0 ∈ σ a ↔ IsUnit a
[PROOFSTEP]
rw [zero_mem_iff, Classical.not_not]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a b c : A
h₁ : (↑↑ₐ r - a) * b = 1
h₂ : c * (↑↑ₐ r - a) = 1
⊢ b * (↑↑ₐ r - a) = 1
[PROOFSTEP]
rwa [← left_inv_eq_right_inv h₂ h₁]
[GOAL]
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ resolventSet R a = univ
[PROOFSTEP]
simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]
[GOAL]
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ σ a = ∅
[PROOFSTEP]
rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
by_cases h : s ∈ spectrum R a
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
rw [mem_iff] at h 
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (↑↑ₐ s - a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse ((r⁻¹ • s) • 1 - r⁻¹ • a)
[PROOFSTEP]
rw [smul_assoc, ← smul_sub]
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
[PROOFSTEP]
have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu => h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
hu : IsUnit (r⁻¹ • (s • 1 - a))
⊢ IsUnit (s • 1 - a)
[PROOFSTEP]
simpa only [smul_inv_smul] using IsUnit.smul r hu
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
h' : ¬IsUnit (r⁻¹ • (s • 1 - a))
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
[PROOFSTEP]
simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
simp only [resolvent]
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
[PROOFSTEP]
have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
  simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
[PROOFSTEP]
simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
[PROOFSTEP]
rw [← h'.subInvSMul_val, ← (not_mem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit, ←
  h'.subInvSMul.inv_eq_val_inv, h'.subInvSMul_inv]
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑(IsUnit.unit (_ : IsUnit (↑↑ₐ s - a)))⁻¹ = r • ↑(IsUnit.unit h')⁻¹
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : A
⊢ r • resolvent a ↑r = resolvent (r⁻¹ • a) 1
[PROOFSTEP]
simpa only [Units.smul_def, Algebra.id.smul_eq_mul, Units.inv_mul] using @units_smul_resolvent _ _ _ _ _ r r a
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : ↑r ∈ resolventSet R ↑a
⊢ ↑r⁻¹ ∈ resolventSet R ↑a⁻¹
[PROOFSTEP]
rw [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, ← Units.smul_def] at h ⊢
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r⁻¹ • 1 - ↑a⁻¹)
[PROOFSTEP]
rw [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv, IsUnit.sub_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
have h₁ : (a : A) * (r • (↑a⁻¹ : A) - 1) = r • (1 : A) - a := by rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
[PROOFSTEP]
rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
have h₂ : (r • (↑a⁻¹ : A) - 1) * a = r • (1 : A) - a := by rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
[PROOFSTEP]
rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
have hcomm : Commute (a : A) (r • (↑a⁻¹ : A) - 1) := by rwa [← h₂] at h₁ 
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ Commute (↑a) (r • ↑a⁻¹ - 1)
[PROOFSTEP]
rwa [← h₂] at h₁ 
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
hcomm : Commute (↑a) (r • ↑a⁻¹ - 1)
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
exact (hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
⊢ 0 ∈ resolventSet R ↑a
[PROOFSTEP]
simpa only [mem_resolventSet_iff, ← not_mem_iff, zero_not_mem_iff] using a.isUnit
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r + s ∈ σ a ↔ r ∈ σ (-↑↑ₐ s + a)
[PROOFSTEP]
simp only [mem_iff, sub_neg_eq_add, ← sub_sub, map_add]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r + s ∈ σ (↑↑ₐ s + a) ↔ r ∈ σ a
[PROOFSTEP]
rw [add_mem_iff, neg_add_cancel_left]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
s : R
r : Rˣ
⊢ r • s ∈ σ (r • a) ↔ s ∈ σ a
[PROOFSTEP]
simp only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub, isUnit_smul_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
⊢ σ (r • a) = r • σ a
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a
[PROOFSTEP]
have x_eq : x = r • r⁻¹ • x := by simp
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
⊢ x = r • r⁻¹ • x
[PROOFSTEP]
simp
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a
[PROOFSTEP]
nth_rw 1 [x_eq]
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a
[PROOFSTEP]
rw [smul_mem_smul_iff]
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a → x ∈ r • σ a
[PROOFSTEP]
exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
h : r⁻¹ • x ∈ σ a
⊢ r • r⁻¹ • x = x
[PROOFSTEP]
simp
[GOAL]
case h.mpr
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ r • σ a → r⁻¹ • x ∈ σ a
[PROOFSTEP]
rintro ⟨w, _, (x'_eq : r • w = x)⟩
[GOAL]
case h.mpr.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : 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
[PROOFSTEP]
simpa [← x'_eq]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
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]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
[PROOFSTEP]
refine' fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, _, _⟩, rfl⟩
[GOAL]
case refine'_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1
case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
[PROOFSTEP]
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]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1 - y * x + y * ((1 - x * y) * (IsUnit.unit h).inv) * x
[PROOFSTEP]
noncomm_ring
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((1 - x * y) * (IsUnit.unit h).inv) * x = 1
[PROOFSTEP]
simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
[GOAL]
case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
[PROOFSTEP]
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]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1 - y * x + y * ((IsUnit.unit h).inv * (1 - x * y)) * x
[PROOFSTEP]
noncomm_ring
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((IsUnit.unit h).inv * (1 - x * y)) * x = 1
[PROOFSTEP]
simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : 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)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
rw [mul_smul_comm r⁻¹ b a] at this 
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : 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 ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
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]
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : star r ∈ resolventSet R a
⊢ r ∈ resolventSet R (star a)
[PROOFSTEP]
simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul, star_star, star_one] using
  IsUnit.star h
[GOAL]
case refine'_2
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : r ∈ resolventSet R (star a)
⊢ star r ∈ resolventSet R a
[PROOFSTEP]
simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul, star_star, star_one] using
  IsUnit.star h
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
⊢ σ (star a) = star (σ a)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
x✝ : R
⊢ x✝ ∈ σ (star a) ↔ x✝ ∈ star (σ a)
[PROOFSTEP]
simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolventSet_iff.symm
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ x ∈ {r} + σ a ↔ x ∈ σ (↑↑ₐ r + a)
[PROOFSTEP]
rw [singleton_add, image_add_left, mem_preimage]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ (fun x x_1 => x + x_1) (-r) x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
[PROOFSTEP]
simp only
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ -r + x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
[PROOFSTEP]
rw [add_comm, add_mem_iff, map_neg, neg_neg]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ -σ a ↔ x ∈ σ (-a)
[PROOFSTEP]
simp only [mem_neg, mem_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ {r} - σ a = σ (↑↑ₐ r - a)
[PROOFSTEP]
rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ a - {r} = σ (a - ↑↑ₐ r)
[PROOFSTEP]
simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 = {0}
[PROOFSTEP]
refine' Set.Subset.antisymm _ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0} ⊆ σ 0
[PROOFSTEP]
simp [Algebra.algebraMap_eq_smul_one, mem_iff]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 ⊆ {0}
[PROOFSTEP]
rw [spectrum, Set.compl_subset_comm]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0}ᶜ ⊆ resolventSet 𝕜 0
[PROOFSTEP]
intro k hk
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ∈ {0}ᶜ
⊢ k ∈ resolventSet 𝕜 0
[PROOFSTEP]
rw [Set.mem_compl_singleton_iff] at hk 
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
⊢ k ∈ resolventSet 𝕜 0
[PROOFSTEP]
have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
this : IsUnit (Units.mk0 k hk • 1)
⊢ k ∈ resolventSet 𝕜 0
[PROOFSTEP]
simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
⊢ σ (↑↑ₐ k) = {k}
[PROOFSTEP]
rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ (↑↑ₐ 1)
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, one_smul]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : Set.Nonempty (σ a)
⊢ σ (k • a) = k • σ a
[PROOFSTEP]
rcases eq_or_ne k 0 with (rfl | h)
[GOAL]
case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : Set.Nonempty (σ a)
⊢ σ (0 • a) = 0 • σ a
[PROOFSTEP]
simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)
[GOAL]
case inr
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : Set.Nonempty (σ a)
h : k ≠ 0
⊢ σ (k • a) = k • σ a
[PROOFSTEP]
exact unit_smul_eq_smul a (Units.mk0 k h)
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}
[PROOFSTEP]
suffices h : ∀ x y : A, σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
h : ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}
[PROOFSTEP]
exact Set.eq_of_subset_of_subset (h a b) (h b a)
[GOAL]
case h
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
[PROOFSTEP]
rintro _ _ k ⟨k_mem, k_neq⟩
[GOAL]
case h.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_mem : k ∈ σ (x✝ * y✝)
k_neq : ¬k ∈ {0}
⊢ k ∈ σ (y✝ * x✝) \ {0}
[PROOFSTEP]
change ((Units.mk0 k k_neq) : 𝕜) ∈ _ at k_mem 
[GOAL]
case h.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_neq : ¬k ∈ {0}
k_mem : ↑(Units.mk0 k k_neq) ∈ σ (x✝ * y✝)
⊢ k ∈ σ (y✝ * x✝) \ {0}
[PROOFSTEP]
exact ⟨unit_mem_mul_iff_mem_swap_mul.mp k_mem, k_neq⟩
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
⊢ (σ ↑a)⁻¹ = σ ↑a⁻¹
[PROOFSTEP]
refine' Set.eq_of_subset_of_subset (fun k hk => _) fun k hk => _
[GOAL]
case refine'_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ (σ ↑a)⁻¹
⊢ k ∈ σ ↑a⁻¹
[PROOFSTEP]
rw [Set.mem_inv] at hk 
[GOAL]
case refine'_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
⊢ k ∈ σ ↑a⁻¹
[PROOFSTEP]
have : k ≠ 0 := by simpa only [inv_inv] using inv_ne_zero (ne_zero_of_mem_of_unit hk)
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
⊢ k ≠ 0
[PROOFSTEP]
simpa only [inv_inv] using inv_ne_zero (ne_zero_of_mem_of_unit hk)
[GOAL]
case refine'_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
this : k ≠ 0
⊢ k ∈ σ ↑a⁻¹
[PROOFSTEP]
lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr this
[GOAL]
case refine'_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : (↑k)⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val k] at hk 
[GOAL]
case refine'_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹
[PROOFSTEP]
exact inv_mem_iff.mp hk
[GOAL]
case refine'_2
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ σ ↑a⁻¹
⊢ k ∈ (σ ↑a)⁻¹
[PROOFSTEP]
lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr (ne_zero_of_mem_of_unit hk)
[GOAL]
case refine'_2.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k ∈ σ ↑a⁻¹
⊢ ↑k ∈ (σ ↑a)⁻¹
[PROOFSTEP]
simpa only [Units.val_inv_eq_inv_val] using inv_mem_iff.mp hk
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Ring B
inst✝¹ : Algebra R B
inst✝ : AlgHomClass F R A B
φ : F
a : A
r : R
h : r ∈ resolventSet R a
⊢ r ∈ resolventSet R (↑φ a)
[PROOFSTEP]
simpa only [map_sub, AlgHomClass.commutes] using h.map φ
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑φ a ∈ σ a
[PROOFSTEP]
have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
  simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply,
    sub_self]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑↑ₐ (↑φ a) - a ∈ RingHom.ker ↑φ
[PROOFSTEP]
simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply,
  sub_self]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
h : ↑↑ₐ (↑φ a) - a ∈ RingHom.ker ↑φ
⊢ ↑φ a ∈ σ a
[PROOFSTEP]
simp only [spectrum.mem_iff, ← mem_nonunits_iff, coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Ring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (↑f a)
[PROOFSTEP]
simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
  AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)
